Collection of patches for SV-COMP'17

regression/cbmc-concurrency/thread_chain_posix2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 -D_ENABLE_CHAIN_ --unwind 2
 ^EXIT=0$

regression/cbmc-concurrency/thread_chain_posix3/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 -D_ENABLE_CHAIN_ -D_SANITY_CHECK_ --unwind 2
 ^EXIT=10$

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_malloc(1);
+  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_malloc(1*sizeof(unsigned char));
+  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_malloc(sizeof(unsigned char)*1);
+  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_malloc(size);
+  unsigned char* buffer=__CPROVER_allocate(size, 0);
   assert(buffer!=0);
 
   buffer[0]=0;

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

@@ -22,7 +22,7 @@ int main()
 {
     // Create node
     struct node *nd;
-    nd = (struct node *)__CPROVER_malloc(sizeof(struct node));
+    nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);
 
     // Link node
     struct list_head *hd = &(nd->linkage);

regression/cbmc/Calloc1/main.c

@@ -0,0 +1,9 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main()
+{
+  int *x=calloc(sizeof(int), 1);
+  assert(*x==0);
+  return 0;
+}

regression/cbmc/Calloc1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Local_out_of_scope3/main.c

@@ -0,0 +1,15 @@
+int main()
+{
+  int *p=0;
+
+  for(int i=0; i<3; ++i)
+  {
+    {
+      int x=42;
+      p=&x;
+      *p=1;
+    }
+  }
+
+  return 0;
+}

regression/cbmc/Local_out_of_scope3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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_malloc(1);
+  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_malloc(1*sizeof(unsigned char));
+  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_malloc(sizeof(unsigned char)*1);
+  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_malloc(buffer_size);
+  unsigned char* buffer=__CPROVER_allocate(buffer_size, 0);
   __CPROVER_assert(buffer!=0, "malloc did not return NULL");
 
   buffer[0]=10;

regression/cbmc/Malloc19/main.c

@@ -22,7 +22,7 @@ int main()
 {
     // Create node
     struct node *nd;
-    nd = (struct node *)__CPROVER_malloc(sizeof(struct node));
+    nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);
 
     // Link node
     struct list_head *hd = &(nd->linkage);

regression/cbmc/realloc3/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$

src/analyses/constant_propagator.cpp

@@ -296,7 +296,7 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
     return false;
 
   if(expr.id()==ID_side_effect &&
-     to_side_effect_expr(expr).get_statement()==ID_malloc)
+     to_side_effect_expr(expr).get_statement()==ID_allocate)
     return false;
 
   if(expr.id()==ID_symbol)

src/analyses/goto_check.cpp

@@ -1654,6 +1654,34 @@ void goto_checkt::goto_check(
         }
       }
     }
+    else if(i.is_decl())
+    {
+      if(enable_pointer_check)
+      {
+        assert(i.code.operands().size()==1);
+        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

@@ -234,7 +234,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_malloc)
+    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_malloc)
+    if(statement==ID_allocate)
     {
       dest.insert(objects.number(exprt(ID_dynamic_object)));
     }

src/ansi-c/ansi_c_internal_additions.cpp

@@ -158,7 +158,7 @@ void ansi_c_internal_additions(std::string &code)
     "void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);\n"
 
     // malloc
-    "void *__CPROVER_malloc(__CPROVER_size_t size);\n"
+    "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"
     "const void *__CPROVER_deallocated=0;\n"
     "const void *__CPROVER_dead_object=0;\n"
     "const void *__CPROVER_malloc_object=0;\n"
@@ -197,6 +197,18 @@ void ansi_c_internal_additions(std::string &code)
     "long double __CPROVER_infl(void);\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"
+    "int __CPROVER_isgreaterequald(double f, double g);\n"
+    "int __CPROVER_islessf(float f, float g);\n"
+    "int __CPROVER_islessd(double f, double g);\n"
+    "int __CPROVER_islessequalf(float f, float g);\n"
+    "int __CPROVER_islessequald(double f, double g);\n"
+    "int __CPROVER_islessgreaterf(float f, float g);\n"
+    "int __CPROVER_islessgreaterd(double f, double g);\n"
+    "int __CPROVER_isunorderedf(float f, float g);\n"
+    "int __CPROVER_isunorderedd(double f, double g);\n"
 
     // absolute value
     "int __CPROVER_abs(int x);\n"

src/ansi-c/c_typecheck_expr.cpp

@@ -2258,16 +2258,16 @@ exprt c_typecheck_baset::do_special_functions(
 
     return abs_expr;
   }
-  else if(identifier==CPROVER_PREFIX "malloc")
+  else if(identifier==CPROVER_PREFIX "allocate")
   {
-    if(expr.arguments().size()!=1)
+    if(expr.arguments().size()!=2)
     {
       err_location(f_op);
-      error() << "malloc expects one operand" << eom;
+      error() << "allocate expects two operands" << eom;
       throw 0;
     }
 
-    exprt malloc_expr=side_effect_exprt(ID_malloc);
+    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

@@ -679,6 +679,7 @@ std::string expr2ct::convert_struct_type(
   if(tag!="")
     dest+=" "+id2string(tag);
 
+#if 0
   if(inc_struct_body)
   {
     dest+=" {";
@@ -702,6 +703,7 @@ std::string expr2ct::convert_struct_type(
 
     dest+=" }";
   }
+#endif
 
   dest+=declarator;
 
@@ -1095,17 +1097,20 @@ std::string expr2ct::convert_pointer_object_has_type(
   return dest;
 }
 
-std::string expr2ct::convert_malloc(
+std::string expr2ct::convert_allocate(
   const exprt &src,
   unsigned &precedence)
 {
-  if(src.operands().size()!=1)
+  if(src.operands().size()!=2)
     return convert_norep(src, precedence);
 
   unsigned p0;
   std::string op0=convert_with_precedence(src.op0(), p0);
 
-  std::string dest="MALLOC";
+  unsigned p1;
+  std::string op1=convert_with_precedence(src.op0(), p1);
+
+  std::string dest="ALLOCATE";
   dest+='(';
 
   if(src.type().id()==ID_pointer &&
@@ -1115,7 +1120,7 @@ std::string expr2ct::convert_malloc(
     dest+=", ";
   }
 
-  dest+=op0;
+  dest+=op0+", "+op1;
   dest+=')';
 
   return dest;
@@ -3629,8 +3634,8 @@ std::string expr2ct::convert_with_precedence(
       return
         convert_side_effect_expr_function_call(
           to_side_effect_expr_function_call(src), precedence);
-    else if(statement==ID_malloc)
-      return convert_malloc(src, precedence=15);
+    else if(statement==ID_allocate)
+      return convert_allocate(src, precedence=15);
     else if(statement==ID_printf)
       return convert_function(src, "printf", precedence=16);
     else if(statement==ID_nondet)

src/ansi-c/expr2c_class.h

@@ -214,7 +214,7 @@ class expr2ct
   std::string convert_function_application(const function_application_exprt &src, unsigned &precedence);
   // NOLINTNEXTLINE(whitespace/line_length)
   std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence);
-  std::string convert_malloc(const exprt &src, unsigned &precedence);
+  std::string convert_allocate(const exprt &src, unsigned &precedence);
   std::string convert_nondet(const exprt &src, unsigned &precedence);
   std::string convert_prob_coin(const exprt &src, unsigned &precedence);
   std::string convert_prob_uniform(const exprt &src, unsigned &precedence);

src/ansi-c/library/cprover.h

@@ -10,7 +10,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ANSI_C_LIBRARY_CPROVER_H
 
 typedef __typeof__(sizeof(int)) __CPROVER_size_t;
-void *__CPROVER_malloc(__CPROVER_size_t size);
+void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 extern const void *__CPROVER_deallocated;
 extern const void *__CPROVER_malloc_object;
 extern __CPROVER_size_t __CPROVER_malloc_size;
@@ -92,6 +92,7 @@ double __CPROVER_inf(void);
 float __CPROVER_inff(void);
 long double __CPROVER_infl(void);
 //extern int __CPROVER_thread_local __CPROVER_rounding_mode;
+int __CPROVER_isgreaterd(double f, double g);
 
 // absolute value
 int __CPROVER_abs(int);