File tree Expand file tree Collapse file tree 4 files changed +11
-5
lines changed Expand file tree Collapse file tree 4 files changed +11
-5
lines changed Original file line number Diff line number Diff line change @@ -192,11 +192,17 @@ class function_indicest
192192// / was set when this call-graph was constructed the edge will be annotated
193193// / with the call-site set.
194194// / \return grapht representation of this call_grapht
195- call_grapht::directed_grapht call_grapht::get_directed_graph () const
195+ call_grapht::directed_grapht
196+ call_grapht::get_directed_graph (const goto_modelt &goto_model) const
196197{
197198 call_grapht::directed_grapht ret;
198199 function_indicest function_indices (ret);
199200
201+ // To make sure we include unreachable functions we first create indices
202+ // for all functions in the function map
203+ for (const auto &f : goto_model.goto_functions .function_map )
204+ function_indices[f.first ];
205+
200206 for (const auto &edge : graph)
201207 {
202208 auto a_index=function_indices[edge.first ];
Original file line number Diff line number Diff line change @@ -135,7 +135,7 @@ class call_grapht
135135 }
136136 };
137137
138- directed_grapht get_directed_graph () const ;
138+ directed_grapht get_directed_graph (const goto_modelt &goto_model ) const ;
139139
140140protected:
141141 void add (const irep_idt &function,
Original file line number Diff line number Diff line change @@ -39,7 +39,7 @@ void slice_global_inits(goto_modelt &goto_model)
3939 // the entry point:
4040 call_grapht call_graph =
4141 call_grapht::create_from_root_function (goto_model, entry_point, false );
42- const auto directed_graph = call_graph.get_directed_graph ();
42+ const auto directed_graph = call_graph.get_directed_graph (goto_model );
4343 INVARIANT (
4444 !directed_graph.empty (), " At least __CPROVER_start should be reachable" );
4545
Original file line number Diff line number Diff line change @@ -176,7 +176,7 @@ SCENARIO("call_graph",
176176 WHEN (" The call graph is exported as a grapht" )
177177 {
178178 call_grapht::directed_grapht exported=
179- call_graph_from_goto_functions.get_directed_graph ();
179+ call_graph_from_goto_functions.get_directed_graph (goto_model );
180180
181181 typedef call_grapht::directed_grapht::node_indext node_indext;
182182 std::map<irep_idt, node_indext> nodes_by_name;
@@ -234,7 +234,7 @@ SCENARIO("call_graph",
234234 {
235235 call_grapht call_graph_from_goto_functions (goto_model, true );
236236 call_grapht::directed_grapht exported=
237- call_graph_from_goto_functions.get_directed_graph ();
237+ call_graph_from_goto_functions.get_directed_graph (goto_model );
238238
239239 typedef call_grapht::directed_grapht::node_indext node_indext;
240240 std::map<irep_idt, node_indext> nodes_by_name;
You can’t perform that action at this time.
0 commit comments