Skip to content

Commit 8aaa411

Browse files
author
Daniel Kroening
committed
properly set function id on instructions added by remove_asm
fixes issue #2653
1 parent 2ad41e3 commit 8aaa411

File tree

4 files changed

+20
-3
lines changed

4 files changed

+20
-3
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
void func()
2+
{
3+
asm("mfence");
4+
}
5+
6+
int main(void)
7+
{
8+
func();
9+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--full-slice
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

src/analyses/flow_insensitive_analysis.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -240,8 +240,8 @@ bool flow_insensitive_analysis_baset::do_function_call(
240240
// get the state at the beginning of the function
241241
locationt l_begin=goto_function.body.instructions.begin();
242242

243-
DATA_INVARIANT(l_begin->function == f_it->first,
244-
"function names have to match");
243+
DATA_INVARIANT(
244+
l_begin->function == f_it->first, "function names have to match");
245245

246246
// do the edge from the call site to the beginning of the function
247247
new_data=state.transform(ns, l_call, l_begin);

src/goto-programs/remove_asm.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -467,7 +467,7 @@ void remove_asmt::process_function(
467467
it->make_skip();
468468
did_something = true;
469469

470-
for(auto & instruction : tmp_dest.instructions)
470+
for(auto &instruction : tmp_dest.instructions)
471471
instruction.function = it->function;
472472

473473
goto_programt::targett next=it;

0 commit comments

Comments
 (0)