diff --git a/regression/goto-instrument/assembly_call_graph_test/main.c b/regression/goto-instrument/assembly_call_graph_test/main.c new file mode 100644 index 00000000000..afc2bbc5c3c --- /dev/null +++ b/regression/goto-instrument/assembly_call_graph_test/main.c @@ -0,0 +1,20 @@ +// This is a hack to make the test pass on windows. The way CBMC on +// windows handles assembly code needs to be fixed. +// CBMC doesn't recognise __asm mfence as a function. + +#ifndef __GNUC__ +void __asm_mfence(); +#endif + +void* thr(void * arg) { +#ifdef __GNUC__ +__asm__ __volatile__ ("mfence": : :"memory"); +#else +__asm_mfence(); +#endif +} + +int main() +{ + thr(0); +} diff --git a/regression/goto-instrument/assembly_call_graph_test/test.desc b/regression/goto-instrument/assembly_call_graph_test/test.desc new file mode 100644 index 00000000000..655514fbb22 --- /dev/null +++ b/regression/goto-instrument/assembly_call_graph_test/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--reachable-call-graph +main -> thr +__CPROVER__start -> __CPROVER_initialize +__CPROVER__start -> main +thr -> __asm_mfence +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp index 881348279f2..6354ec41485 100644 --- a/src/analyses/call_graph.cpp +++ b/src/analyses/call_graph.cpp @@ -84,11 +84,16 @@ call_grapht::call_grapht( { irep_idt function=pending_stack.top(); pending_stack.pop(); - const goto_programt &goto_program= - goto_functions.function_map.at(function).body; nodes.insert(function); + // if function is not in function_map, assume function has no body + const auto &it = goto_functions.function_map.find(function); + if(it == goto_functions.function_map.end()) + continue; + + const goto_programt &goto_program = it->second.body; + forall_callsites( goto_program, [&](goto_programt::const_targett i_it, const irep_idt &callee) diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index 0c51b77fca8..ed50376570c 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -52,13 +52,17 @@ void slice_global_inits(goto_modelt &goto_model) const irep_idt &id = directed_graph[node_idx].function; if(id == INITIALIZE_FUNCTION) continue; - const goto_functionst::goto_functiont &goto_function - =goto_functions.function_map.at(id); - const goto_programt &goto_program=goto_function.body; + + // assume function has no body if it is not in the function map + const auto &it = goto_functions.function_map.find(id); + if(it == goto_functions.function_map.end()) + continue; + + const goto_programt &goto_program = it->second.body; forall_goto_program_instructions(i_it, goto_program) { - const codet &code=i_it->code; + const codet &code = i_it->code; find_symbols(code, symbols, true, false); const exprt &expr = i_it->guard; find_symbols(expr, symbols, true, false);