replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

fix for uninterpreted functions 

CBMC supports uninterpreted functions; this feature had no test, and thus
got broken with 5081310093.

Fixes #3561.
This commit is contained in:
Daniel Kroening 2019-01-08 16:16:24 +00:00
parent 8408181b11
commit e53d2b4d45
4 changed files with 27 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
regression/cbmc/uninterpreted_function/uf1.c Normal file
View File

@ -0,0 +1,7 @@
_Bool __CPROVER_uninterpreted_f();
main()
{
_Bool a = __CPROVER_uninterpreted_f();
assert(0);
}

10
regression/cbmc/uninterpreted_function/uf1.desc Normal file
View File

@ -0,0 +1,10 @@
CORE
uf1.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^warning: ignoring
--
Basic test for an uninterpreted function; based on issue #3561.

1
scripts/delete_failing_smt2_solver_tests
View File

@ -74,6 +74,7 @@ rm struct6/test.desc
rm struct7/test.desc
rm trace-values/trace-values.desc
rm trace_show_function_calls/test.desc
rm uninterpreted_function/uf1.desc
rm union12/test.desc
rm union6/test.desc
rm union7/test.desc

15
src/goto-symex/build_goto_trace.cpp
View File

@ -111,13 +111,16 @@ void set_internal_dynamic_object(
{
if(expr.id()==ID_symbol)
{
const irep_idt &id=to_ssa_expr(expr).get_original_name();
const symbolt *symbol;
if(!ns.lookup(id, symbol))
if(expr.type().id() != ID_code)
{
bool result = symbol->type.get_bool(ID_C_dynamic);
if(result)
goto_trace_step.internal=true;
const irep_idt &id = to_ssa_expr(expr).get_original_name();
const symbolt *symbol;
if(!ns.lookup(id, symbol))
{
bool result = symbol->type.get_bool(ID_C_dynamic);
if(result)
goto_trace_step.internal = true;
}
}
}
else