Skip to content

Commit 8a44f9a

Browse files
tautschnigDaniel Kroening
authored and
Daniel Kroening
committed
Justify use of source_locationt::get_function in WMM instrumentation
This user-level heuristics is no more or less reliable than the file-name test that's also used here.
1 parent 9f7ed63 commit 8a44f9a

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/goto-instrument/wmm/goto2graph.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -535,6 +535,9 @@ void inline instrumentert::cfg_visitort::visit_cfg_duplicate(
535535
}
536536
}
537537

538+
// The code below uses heuristics to limit false positives: no cycles across
539+
// inlined functions, which we would detect when file names or
540+
// (user-provided) function names change _within a single goto_program_.
538541
if(!found_pos
539542
|| new_targ->source_location.get_function()
540543
!=targ->source_location.get_function()

0 commit comments

Comments
 (0)