Skip to content

Commit f404979

Browse files
polgreenmmuesly
authored andcommitted
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 diffblue#2631
1 parent da86bdb commit f404979

File tree

4 files changed

+38
-6
lines changed

4 files changed

+38
-6
lines changed
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
void* thr(void * arg) {
2+
#ifdef __GNUC__
3+
__asm__ __volatile__ ("mfence": : :"memory");
4+
#elif defined(_MSC_VER)
5+
__asm mfence;
6+
#endif
7+
}
8+
9+
int main()
10+
{
11+
thr(0);
12+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--reachable-call-graph
4+
main -> thr
5+
__CPROVER__start -> __CPROVER_initialize
6+
__CPROVER__start -> main
7+
thr -> __asm_mfence
8+
^EXIT=0$
9+
^SIGNAL=0$
10+
--
11+
^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)