Simplifier 20160305

regression/cbmc/null3/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct S
+{
+  int a;
+  int b;
+};
+
+int main()
+{
+  struct S s;
+  int* b_ptr=&(s.b);
+
+  if((size_t)((struct S*)0)!=0)
+    return 1;
+
+  struct S* s_ptr=(struct S*)((char*)b_ptr - ((size_t) &((struct S*)0)->b));
+  assert(s_ptr==&s);
+
+  return 0;
+}
+

regression/cbmc/null3/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+\(Starting CEGAR Loop\|^Generated 0 VCC(s), 0 remaining after simplification$\)
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-symex/symex_builtin_functions.cpp

@@ -234,6 +234,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
 
   exprt tmp=code.op0();
   state.rename(tmp, ns); // to allow constant propagation
+  do_simplify(tmp);
   irep_idt id=get_symbol(tmp);
 
   exprt rhs=gen_zero(lhs.type());
@@ -346,6 +347,7 @@ void goto_symext::symex_printf(
 
   exprt tmp_rhs=rhs;
   state.rename(tmp_rhs, ns);
+  do_simplify(tmp_rhs);
 
   const exprt::operandst &operands=tmp_rhs.operands();
   std::list<exprt> args;
@@ -391,6 +393,7 @@ void goto_symext::symex_input(
   {
     args.push_back(code.operands()[i]);
     state.rename(args.back(), ns);
+    do_simplify(args.back());
   }
 
   const irep_idt input_id=get_string_argument(id_arg, ns);
@@ -427,6 +430,7 @@ void goto_symext::symex_output(
   {
     args.push_back(code.operands()[i]);
     state.rename(args.back(), ns);
+    do_simplify(args.back());
   }
 
   const irep_idt output_id=get_string_argument(id_arg, ns);