Merge pull request #2636 from polgreen/fix_function_map

if function is not in the function map, treat as if it has no body

Author: Daniel Kroening

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);
+}

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

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)

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);