Skip to content

Commit a73b9d8

Browse files
committed
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
1 parent 0c0e288 commit a73b9d8

File tree

4 files changed

+41
-6
lines changed

4 files changed

+41
-6
lines changed
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
void* thr1(void * arg) {
2+
__asm__ __volatile__ ("mfence": : :"memory");
3+
}
4+
5+
void* thr2(void * arg) {
6+
__asm__ __volatile__ ("mfence": : :"memory");
7+
}
8+
9+
int main()
10+
{
11+
thr1(0);
12+
thr2(0);
13+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--reachable-call-graph
4+
main -> thr1
5+
main -> thr2
6+
__CPROVER__start -> __CPROVER_initialize
7+
__CPROVER__start -> main
8+
thr1 -> __asm_mfence
9+
thr2 -> __asm_mfence
10+
^EXIT=0$
11+
^SIGNAL=0$
12+
--
13+
^warning: ignoring

src/analyses/call_graph.cpp

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -84,11 +84,16 @@ call_grapht::call_grapht(
8484
{
8585
irep_idt function=pending_stack.top();
8686
pending_stack.pop();
87-
const goto_programt &goto_program=
88-
goto_functions.function_map.at(function).body;
8987

9088
nodes.insert(function);
9189

90+
// if function is not in function_map, assume function has no body
91+
const auto &it = goto_functions.function_map.find(function);
92+
if(it == goto_functions.function_map.end())
93+
continue;
94+
95+
const goto_programt &goto_program = it->second.body;
96+
9297
forall_callsites(
9398
goto_program,
9499
[&](goto_programt::const_targett i_it, const irep_idt &callee)

src/goto-programs/slice_global_inits.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -52,13 +52,17 @@ void slice_global_inits(goto_modelt &goto_model)
5252
const irep_idt &id = directed_graph[node_idx].function;
5353
if(id == INITIALIZE_FUNCTION)
5454
continue;
55-
const goto_functionst::goto_functiont &goto_function
56-
=goto_functions.function_map.at(id);
57-
const goto_programt &goto_program=goto_function.body;
55+
56+
// assume function has no body if it is not in the function map
57+
const auto &it = goto_functions.function_map.find(id);
58+
if(it == goto_functions.function_map.end())
59+
continue;
60+
61+
const goto_programt &goto_program = it->second.body;
5862

5963
forall_goto_program_instructions(i_it, goto_program)
6064
{
61-
const codet &code=i_it->code;
65+
const codet &code = i_it->code;
6266
find_symbols(code, symbols, true, false);
6367
const exprt &expr = i_it->guard;
6468
find_symbols(expr, symbols, true, false);

0 commit comments

Comments
 (0)