Skip to content

Commit 5606ce5

Browse files
author
martin
committed
Use is_bottom() to catch unreachable functions.
1 parent 3178f1b commit 5606ce5

File tree

1 file changed

+8
-3
lines changed

1 file changed

+8
-3
lines changed

src/analyses/ai.cpp

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ xmlt ai_domain_baset::output_xml(
3737
{
3838
std::ostringstream out;
3939
output(out, ai, ns);
40-
xmlt xml("domain");
40+
xmlt xml("abstract_state");
4141
xml.data=out.str();
4242
return xml;
4343
}
@@ -166,7 +166,7 @@ jsont ai_baset::output_json(
166166
json_numbert(std::to_string(i_it->location_number));
167167
location["sourceLocation"]=
168168
json_stringt(i_it->source_location.as_string());
169-
location["domain"]=find_state(i_it).output_json(*this, ns);
169+
location["abstractState"]=find_state(i_it).output_json(*this, ns);
170170

171171
// Ideally we need output_instruction_json
172172
std::ostringstream out;
@@ -427,7 +427,12 @@ bool ai_baset::do_function_call(
427427
assert(l_end->is_end_function());
428428

429429
// do edge from end of function to instruction after call
430-
std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_end)));
430+
const statet &end_state=get_state(l_end);
431+
432+
if(end_state.is_bottom())
433+
return false; // function exit point not reachable
434+
435+
std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
431436
tmp_state->transform(l_end, l_return, *this, ns);
432437

433438
// Propagate those

0 commit comments

Comments
 (0)