SV-COMP 2018: Rebase of Tautschnig's branch/PR sv-comp-2017 on cbmc/develop

regression/cbmc-with-incr/Malloc17/main.c

@@ -4,7 +4,7 @@ unsigned char* init1()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(1, 0);
+  unsigned char *buffer = __CPROVER_allocate(1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
+  unsigned char *buffer = __CPROVER_allocate(1 * sizeof(unsigned char), 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
+  unsigned char *buffer = __CPROVER_allocate(sizeof(unsigned char) * 1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;

regression/cbmc-with-incr/Malloc18/main.c

@@ -4,7 +4,7 @@ unsigned char* init()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(size, 0);
+  unsigned char *buffer = __CPROVER_allocate(size, 0);
   assert(buffer!=0);
 
   buffer[0]=0;

regression/cbmc/Calloc1/main.c

@@ -3,7 +3,7 @@
 
 int main()
 {
-  int *x=calloc(sizeof(int), 1);
-  assert(*x==0);
+  int *x = calloc(sizeof(int), 1);
+  assert(*x == 0);
   return 0;
 }

regression/cbmc/Malloc17/main.c

@@ -4,7 +4,7 @@ unsigned char* init1()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(1, 0);
+  unsigned char *buffer = __CPROVER_allocate(1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
+  unsigned char *buffer = __CPROVER_allocate(1 * sizeof(unsigned char), 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
+  unsigned char *buffer = __CPROVER_allocate(sizeof(unsigned char) * 1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;

regression/cbmc/Malloc18/main.c

@@ -3,7 +3,7 @@ unsigned char* init()
   unsigned long buffer_size;
   if(buffer_size!=1) return 0;
 
-  unsigned char* buffer=__CPROVER_allocate(buffer_size, 0);
+  unsigned char *buffer = __CPROVER_allocate(buffer_size, 0);
   __CPROVER_assert(buffer!=0, "malloc did not return NULL");
 
   buffer[0]=10;

regression/cbmc/Malloc24/main.c

@@ -2,8 +2,8 @@
 
 struct node
 {
-    int value;
-    struct node *next;
+  int value;
+  struct node *next;
 };
 
 struct list
@@ -12,7 +12,7 @@ struct list
   struct node *head;
 };
 
-void removeLast(struct list * l)
+void removeLast(struct list *l)
 {
   int index = l->size - 1;
   struct node **current;
@@ -22,16 +22,17 @@ void removeLast(struct list * l)
   l->size--;
 }
 
-int main () {
+int main()
+{
   //build a 2-nodes list
   struct node *n0 = malloc(sizeof(struct node));
   struct node *n1 = malloc(sizeof(struct node));
   struct list *l = malloc(sizeof(struct list));
   l->size = 2;
   l->head = n0;
 
-  n0->next=n1;
-  n1->next=NULL;
+  n0->next = n1;
+  n1->next = NULL;
 
   //remove last node from list
 
@@ -43,5 +44,5 @@ int main () {
   //this doesn't
   removeLast(l);
 
-  __CPROVER_assert(n0->next == NULL , "not NULL");
+  __CPROVER_assert(n0->next == NULL, "not NULL");
 }

regression/cbmc/address_space_size_limit1/test.desc

@@ -1,5 +1,7 @@
 CORE
 test.c
 --no-simplify --unwind 300 --object-bits 8
+^EXIT=6$
+^SIGNAL=0$
 too many addressed objects
---
+--

regression/cbmc/realloc3/test.desc

@@ -1,8 +1,12 @@
 CORE
 main.c
 
-^EXIT=0$
+^EXIT=6$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+pointer handling for concurrency is unsound
 --
 ^warning: ignoring
+--
+The test uses "__CPROVER_ASYNC_1:" and the async-called function foo
+does pointer operations over allocated memory - which is not handled sound
+way in CBMC.

regression/strings-smoke-tests/java_format/test.desc

@@ -5,5 +5,4 @@ test.class
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
 ^\[.*assertion.2\].* line 7.* FAILURE$
---
-^ignoring
+--

src/analyses/constant_propagator.cpp

@@ -276,9 +276,12 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
      to_side_effect_expr(expr).get_statement()==ID_nondet)
     return false;
 
-  if(expr.id()==ID_side_effect &&
-     to_side_effect_expr(expr).get_statement()==ID_allocate)
+  if(
+    expr.id() == ID_side_effect &&
+    to_side_effect_expr(expr).get_statement() == ID_allocate)
+  {
     return false;
+  }
 
   if(expr.id()==ID_symbol)
     if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())==

src/analyses/goto_check.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_predicates.h>
 #include <util/cprover_prefix.h>
 #include <util/options.h>
+#include <util/invariant.h>
 
 #include "local_bitvector_analysis.h"
 
@@ -1658,30 +1659,56 @@ void goto_checkt::goto_check(
     {
       if(enable_pointer_check)
       {
-        assert(i.code.operands().size()==1);
+        INVARIANT(i.code.operands().size() == 1, "The num-operands must be 1.");
         const symbol_exprt &variable=to_symbol_expr(i.code.op0());
 
         // is it dirty?
         if(local_bitvector_analysis->dirty(variable))
         {
           // need to mark the dead variable as dead
           goto_programt::targett t=new_code.add_instruction(ASSIGN);
-          exprt address_of_expr=address_of_exprt(variable);
+          address_of_exprt address_of_expr = address_of_exprt(variable);
           exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
           if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
             address_of_expr.make_typecast(lhs.type());
-          exprt rhs=
-            if_exprt(
-              side_effect_expr_nondett(bool_typet()),
-              address_of_expr,
-              lhs,
-              lhs.type());
+          if_exprt rhs = if_exprt(
+            side_effect_expr_nondett(bool_typet()),
+            address_of_expr,
+            lhs,
+            lhs.type());
           t->source_location=i.source_location;
           t->code=code_assignt(lhs, rhs);
           t->code.add_source_location()=i.source_location;
         }
       }
     }
+    else if(i.is_decl())
+    {
+      if(enable_pointer_check)
+      {
+        INVARIANT(i.code.operands().size() == 1, "There must be 1 operand.");
+        const symbol_exprt &variable = to_symbol_expr(i.code.op0());
+
+        // is it dirty?
+        if(local_bitvector_analysis->dirty(variable))
+        {
+          // reset the dead marker
+          goto_programt::targett t = new_code.add_instruction(ASSIGN);
+          exprt address_of_expr = address_of_exprt(variable);
+          exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+          if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
+            address_of_expr.make_typecast(lhs.type());
+          exprt rhs = if_exprt(
+            equal_exprt(lhs, address_of_expr),
+            null_pointer_exprt(to_pointer_type(address_of_expr.type())),
+            lhs,
+            lhs.type());
+          t->source_location = i.source_location;
+          t->code = code_assignt(lhs, rhs);
+          t->code.add_source_location() = i.source_location;
+        }
+      }
+    }
     else if(i.is_end_function())
     {
       if(i.function==goto_functionst::entry_point() &&

src/analyses/local_bitvector_analysis.cpp

@@ -232,7 +232,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
     const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
     const irep_idt &statement=side_effect_expr.get_statement();
 
-    if(statement==ID_allocate)
+    if(statement == ID_allocate)
       return flagst::mk_dynamic_heap();
     else
       return flagst::mk_unknown();

src/analyses/local_may_alias.cpp

@@ -298,7 +298,7 @@ void local_may_aliast::get_rec(
     const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
     const irep_idt &statement=side_effect_expr.get_statement();
 
-    if(statement==ID_allocate)
+    if(statement == ID_allocate)
     {
       dest.insert(objects.number(exprt(ID_dynamic_object)));
     }

src/ansi-c/ansi_c_internal_additions.cpp

@@ -105,15 +105,17 @@ static std::string architecture_string(int value, const char *s)
 
 void ansi_c_internal_additions(std::string &code)
 {
-  code+=
+  code +=
     "# 1 \"<built-in-additions>\"\n"
     "typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n"
     "void __CPROVER_assume(__CPROVER_bool assumption);\n"
     "void __VERIFIER_assume(__CPROVER_bool assumption);\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "void __CPROVER_assert(__CPROVER_bool assertion, const char *description);\n"
+    "void __CPROVER_assert(__CPROVER_bool assertion, const char "
+    "*description);\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);\n"
+    "void __CPROVER_precondition(__CPROVER_bool precondition, const char "
+    "*description);\n"
     "void __CPROVER_havoc_object(void *);\n"
     "__CPROVER_bool __CPROVER_equal();\n"
     "__CPROVER_bool __CPROVER_same_object(const void *, const void *);\n"
@@ -145,7 +147,8 @@ void ansi_c_internal_additions(std::string &code)
     "void __CPROVER_fence(const char *kind, ...);\n"
     "__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
+    "__CPROVER_bool "
+    "__CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
     "unsigned long __CPROVER_next_thread_id=0;\n"
 
     // traces
@@ -157,7 +160,8 @@ void ansi_c_internal_additions(std::string &code)
     "__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);\n"
     "extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);\n"
+    "void __CPROVER_allocated_memory(__CPROVER_size_t address, "
+    "__CPROVER_size_t extent);\n"
 
     // malloc
     "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"
@@ -170,13 +174,16 @@ void ansi_c_internal_additions(std::string &code)
 
     // this is ANSI-C
     // NOLINTNEXTLINE(whitespace/line_length)
-    "extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];\n"
+    "extern __CPROVER_thread_local const char "
+    "__func__[__CPROVER_constant_infinity_uint];\n"
 
     // this is GCC
     // NOLINTNEXTLINE(whitespace/line_length)
-    "extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];\n"
+    "extern __CPROVER_thread_local const char "
+    "__FUNCTION__[__CPROVER_constant_infinity_uint];\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
+    "extern __CPROVER_thread_local const char "
+    "__PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
 
     // float stuff
     "__CPROVER_bool __CPROVER_isnanf(float f);\n"
@@ -197,8 +204,9 @@ void ansi_c_internal_additions(std::string &code)
     "double __CPROVER_inf(void);\n"
     "float __CPROVER_inff(void);\n"
     "long double __CPROVER_infl(void);\n"
-    "int __CPROVER_thread_local __CPROVER_rounding_mode="+
-      std::to_string(config.ansi_c.rounding_mode)+";\n"
+    "int __CPROVER_thread_local __CPROVER_rounding_mode=" +
+    std::to_string(config.ansi_c.rounding_mode) +
+    ";\n"
     "int __CPROVER_isgreaterf(float f, float g);\n"
     "int __CPROVER_isgreaterd(double f, double g);\n"
     "int __CPROVER_isgreaterequalf(float f, float g);\n"
@@ -222,7 +230,8 @@ void ansi_c_internal_additions(std::string &code)
 
     // arrays
     // NOLINTNEXTLINE(whitespace/line_length)
-    "__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);\n"
+    "__CPROVER_bool __CPROVER_array_equal(const void *array1, "
+    "const void *array2);\n"
     // overwrite all of *dest (possibly using nondet values), even
     // if *src is smaller
     "void __CPROVER_array_copy(const void *dest, const void *src);\n"
@@ -232,7 +241,7 @@ void ansi_c_internal_additions(std::string &code)
 
     // k-induction
     "void __CPROVER_k_induction_hint(unsigned min, unsigned max, "
-      "unsigned step, unsigned loop_free);\n"
+    "unsigned step, unsigned loop_free);\n"
 
     // format string-related
     "int __CPROVER_scanf(const char *, ...);\n"
@@ -245,7 +254,8 @@ void ansi_c_internal_additions(std::string &code)
     "  short next_unread;\n"
     "};\n"
     // NOLINTNEXTLINE(whitespace/line_length)
-    "extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
+    "extern struct __CPROVER_pipet "
+    "__CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
     // offset to make sure we don't collide with other fds
     "extern const int __CPROVER_pipe_offset;\n"
     "unsigned __CPROVER_pipe_count=0;\n"

src/ansi-c/c_typecheck_expr.cpp

@@ -2271,16 +2271,16 @@ exprt c_typecheck_baset::do_special_functions(
 
     return abs_expr;
   }
-  else if(identifier==CPROVER_PREFIX "allocate")
+  else if(identifier == CPROVER_PREFIX "allocate")
   {
-    if(expr.arguments().size()!=2)
+    if(expr.arguments().size() != 2)
     {
       err_location(f_op);
       error() << "allocate expects two operands" << eom;
       throw 0;
     }
 
-    exprt malloc_expr=side_effect_exprt(ID_allocate);
+    exprt malloc_expr = side_effect_exprt(ID_allocate);
     malloc_expr.type()=expr.type();
     malloc_expr.add_source_location()=source_location;
     malloc_expr.operands()=expr.arguments();

src/ansi-c/expr2c.cpp

@@ -1124,7 +1124,7 @@ std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence)
   std::string op0 = convert_with_precedence(src.op0(), p0);
 
   unsigned p1;
-  std::string op1 = convert_with_precedence(src.op1(), p1);
+  const std::string op1 = convert_with_precedence(src.op1(), p1);
 
   std::string dest = "ALLOCATE";
   dest += '(';