properly set function id on instructions added by remove_asm

fixes issue #2653
This commit is contained in:
Daniel Kroening 2018-08-15 10:51:37 +01:00
parent 05993f467b
commit ef4bb3cd1a
4 changed files with 23 additions and 0 deletions

View File

@ -0,0 +1,9 @@
void func()
{
asm("mfence");
}
int main(void)
{
func();
}

View File

@ -0,0 +1,8 @@
CORE
main.c
--full-slice
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring

View File

@ -240,6 +240,9 @@ bool flow_insensitive_analysis_baset::do_function_call(
// get the state at the beginning of the function
locationt l_begin=goto_function.body.instructions.begin();
DATA_INVARIANT(
l_begin->function == f_it->first, "function names have to match");
// do the edge from the call site to the beginning of the function
new_data=state.transform(ns, l_call, l_begin);

View File

@ -467,6 +467,9 @@ void remove_asmt::process_function(
it->make_skip();
did_something = true;
for(auto &instruction : tmp_dest.instructions)
instruction.function = it->function;
goto_programt::targett next=it;
next++;