Merge pull request #3727 from diffblue/uf-test

fix for uninterpreted functions

Author: Daniel Kroening

regression/cbmc/uninterpreted_function/uf1.c

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

regression/cbmc/uninterpreted_function/uf1.desc

@@ -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.

regression/cbmc/uninterpreted_function/uf2.c

@@ -0,0 +1,12 @@
+int __CPROVER_uninterpreted_f(int, int);
+
+main()
+{
+  int a, b;
+
+  int inst1 = __CPROVER_uninterpreted_f(1, a);
+  int inst2 = __CPROVER_uninterpreted_f(1, b);
+
+  if(a == b)
+    __CPROVER_assert(inst1 == inst2, "functional consistency");
+}

regression/cbmc/uninterpreted_function/uf2.desc

@@ -0,0 +1,10 @@
+CORE
+uf2.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Basic test for an uninterpreted function.

scripts/delete_failing_smt2_solver_tests

@@ -74,6 +74,8 @@ 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 uninterpreted_function/uf2.desc
 rm union12/test.desc
 rm union6/test.desc
 rm union7/test.desc

src/goto-symex/build_goto_trace.cpp

@@ -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