Set a property id for recursion unwinding assertions

Previously we displayed an empty id.
This commit is contained in:
Michael Tautschnig 2019-01-19 16:25:58 +00:00
parent e48870578f
commit e53a82b00d
3 changed files with 23 additions and 0 deletions

View File

@ -0,0 +1,9 @@
void foo()
{
foo();
}
int main()
{
foo();
}

View File

@ -0,0 +1,8 @@
CORE
main.c
--unwind 3 --unwinding-assertions
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
^\[foo.recursion\]
--

View File

@ -988,6 +988,12 @@ irep_idt symex_target_equationt::SSA_stept::get_property_id() const
property_id = id2string(source.pc->source_location.get_function()) +
".unwind." + std::to_string(source.pc->loop_number);
}
else if(source.pc->is_function_call())
{
// this is likely a recursion unwinding assertion
property_id =
id2string(source.pc->source_location.get_function()) + ".recursion";
}
else
{
// return empty