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

For the call graph, we add the function to the call graph but do not try to look for function calls in the body.
For slicing global inits, we do not try to look in the function body for symbols.
This fixes issue #2631

Author: polgreen

regression/goto-instrument/assembly_call_graph_test/main.c

@@ -0,0 +1,37 @@
+#ifdef SATABS
+#define assert(e) __CPROVER_assert(e,"error")
+#endif
+
+volatile int turn; // integer variable to hold the ID of the thread whose turn is it
+int x; // variable to test mutual exclusion
+volatile int flag1 = 0, flag2 = 0; // boolean flags
+
+void* thr1(void * arg) { // frontend produces 12 transitions from this thread. It would be better if it would produce only 8!
+  flag1 = 1;
+  turn = 1;
+  __asm__ __volatile__ ("mfence": : :"memory");
+  __CPROVER_assume(! (flag2==1 && turn==1) );
+  // begin: critical section
+  x = 0;
+  assert(x<=0);
+  // end: critical section
+  flag1 = 0;
+}
+
+void* thr2(void * arg) {
+  flag2 = 1;
+  turn = 0;
+  __asm__ __volatile__ ("mfence": : :"memory");
+  __CPROVER_assume(! (flag1==1 && turn==0) );
+  // begin: critical section
+  x = 1;
+  assert (x>=1);
+  // end: critical section
+  flag2 = 0;
+}
+
+int main()
+{
+  __CPROVER_ASYNC_1: thr1(0);
+  thr2(0);
+}

regression/goto-instrument/assembly_call_graph_test/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--reachable-call-graph
+main -> thr1
+main -> thr2
+__CPROVER__start -> __CPROVER_initialize
+__CPROVER__start -> main
+thr1 -> __asm_mfence
+thr2 -> __asm_mfenc
+^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);