Skip to content

Commit

Permalink
Fix undefined-function property rewrite
Browse files Browse the repository at this point in the history
  • Loading branch information
tautschnig committed Jun 11, 2024
1 parent bf7a41e commit 23f68ea
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions kani-driver/src/cbmc_property_renderer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,7 @@ enum CoverageStatus {
const UNSUPPORTED_CONSTRUCT_DESC: &str = "is not currently supported by Kani";
const UNWINDING_ASSERT_DESC: &str = "unwinding assertion loop";
const UNWINDING_ASSERT_REC_DESC: &str = "recursion unwinding assertion";
const DEFAULT_ASSERTION: &str = "assertion";
const UNDEFINED_FUNCTION_DESC: &str = "undefined function should be unreachable";

impl ParserItem {
/// Determines if an item must be skipped or not.
Expand Down Expand Up @@ -618,8 +618,7 @@ fn modify_undefined_function_checks(mut properties: Vec<Property>) -> (Vec<Prope
let mut has_unknown_location_checks = false;
for prop in &mut properties {
if let Some(function) = &prop.source_location.function
&& prop.description == DEFAULT_ASSERTION
&& prop.source_location.file.is_none()
&& prop.description == UNDEFINED_FUNCTION_DESC
{
// Missing functions come with mangled names.
// `demangle` produces the demangled version if it's a mangled name.
Expand Down

0 comments on commit 23f68ea

Please sign in to comment.