Preconditions

regression/cbmc-cover/branch3/test.desc

@@ -3,6 +3,7 @@ main.c
 --cover branch --unwind 6
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* .* of .* covered \(100.0%\)$
+^\*\* .* of .* covered \(.*\)$
 --
 ^warning: ignoring
+^\[main.coverage.*\] file main.c line .* function main block .* branch .*: FAILED$

regression/cbmc-cover/built-ins1/main.c

@@ -1,9 +1,11 @@
+#include <string.h>
+
 int main()
 {
   char a[10];
   __CPROVER_input("a[3]", a[3]);
 
-  int len = strlen(a);
+  int len=strlen(a);
 
   if(len==3)
   {
@@ -13,5 +15,6 @@ int main()
   {
     return -1;
   }
+
   return 1;
 }

regression/cbmc-cover/built-ins1/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover location --unwind 1
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 4 of 7 covered
+^\*\* 5 of 8 covered
 --
 ^warning: ignoring
 ^\[.*<builtin-library-

regression/cbmc-cover/built-ins3/main.c

@@ -5,6 +5,8 @@ int main()
   const char *s="test";
   int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable)
 
+  __CPROVER_input("return value puts", ret);
+
   if(ret<0)
   {
     return 1;

regression/cbmc-cover/built-ins3/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover location --unwind 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 4 of 4 covered
+^\*\* 5 of .* covered
 --
 ^warning: ignoring
 ^\[.*<builtin-library-

regression/cbmc-cover/built-ins4/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/built-ins5/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/built-ins6/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/built-ins7/main.c

@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];

regression/cbmc-cover/inlining1/main.c

@@ -1,3 +1,5 @@
+// Discussion point: is the branch below one goal or two?
+
 inline void my_func(int x)
 {
   if(x)

regression/cbmc-cover/inlining1/test.desc

@@ -3,9 +3,9 @@ main.c
 --cover branch
 ^EXIT=0$
 ^SIGNAL=0$
-^\[my_func.coverage.1\] file main.c line 3 function my_func block 1 branch false: SATISFIED$
-^\[my_func.coverage.2\] file main.c line 3 function my_func block 1 branch true: FAILED$
-^\[my_func.coverage.3\] file main.c line 3 function my_func block 2 branch false: FAILED$
-^\[my_func.coverage.4\] file main.c line 3 function my_func block 2 branch true: SATISFIED$
+^\[main.coverage.1\] file main.c line 15 function main entry point: SATISFIED$
+^\[my_func.coverage.1\] file main.c line 5 function my_func entry point: SATISFIED$
+^\[my_func.coverage.2\] file main.c line 5 function my_func block 1 branch false: SATISFIED$
+^\[my_func.coverage.3\] file main.c line 5 function my_func block 1 branch true: SATISFIED$
 --
 ^warning: ignoring

regression/cbmc/Free2/test.desc

@@ -1,8 +1,10 @@
 CORE
 main.c
---pointer-check
+
 ^EXIT=10$
 ^SIGNAL=0$
+^.*free argument must be dynamic object: FAILURE$
+^.*free argument has offset zero: SUCCESS$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

src/ansi-c/ansi_c_internal_additions.cpp

@@ -112,6 +112,8 @@ void ansi_c_internal_additions(std::string &code)
     "void __VERIFIER_assume(__CPROVER_bool assumption);\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     "void __CPROVER_assert(__CPROVER_bool assertion, const char *description);\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    "void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);\n"
     "__CPROVER_bool __CPROVER_equal();\n"
     "__CPROVER_bool __CPROVER_same_object(const void *, const void *);\n"
     "__CPROVER_bool __CPROVER_invalid_pointer(const void *);\n"

src/ansi-c/library/cprover.h

@@ -19,6 +19,7 @@ extern const void *__CPROVER_memory_leak;
 
 void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
+void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
 
 __CPROVER_bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);

src/ansi-c/library/stdlib.c

@@ -145,14 +145,13 @@ inline void free(void *ptr)
 {
   __CPROVER_HIDE:;
   // If ptr is NULL, no operation is performed.
+  __CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
+                         "free argument must be dynamic object");
+  __CPROVER_precondition(ptr==0 || __CPROVER_POINTER_OFFSET(ptr)==0,
+                         "free argument has offset zero");
+
   if(ptr!=0)
   {
-    // is it dynamic?
-    __CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr),
-                     "free argument is dynamic object");
-    __CPROVER_assert(__CPROVER_POINTER_OFFSET(ptr)==0,
-                     "free argument has offset zero");
-
     // catch double free
     if(__CPROVER_deallocated==ptr)
       __CPROVER_assert(0, "double free");

src/cbmc/bmc_cover.cpp

@@ -204,8 +204,6 @@ bool bmc_covert::operator()()
   // This maps property IDs to 'goalt'
   forall_goto_functions(f_it, goto_functions)
   {
-    // Functions are already inlined.
-    if(f_it->second.is_inlined()) continue;
     forall_goto_program_instructions(i_it, f_it->second.body)
     {
       if(i_it->is_assert())

src/cbmc/cbmc_parse_options.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/convert_nondet.h>
 #include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/link_to_library.h>
@@ -780,9 +781,8 @@ bool cbmc_parse_optionst::process_goto_program(
 
     mm_io(goto_model);
 
-    // do partial inlining
-    status() << "Partial Inlining" << eom;
-    goto_partial_inline(goto_model, get_message_handler());
+    // instrument library preconditions
+    instrument_preconditions(goto_model);
 
     // remove returns, gcc vectors, complex
     remove_returns(goto_model);

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -259,7 +259,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-value-sets"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
 
       // recalculate numbers, etc.
       goto_model.goto_functions.update();
@@ -275,7 +274,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-global-may-alias"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
       do_remove_returns();
       parameter_assignments(goto_model);
 
@@ -292,7 +290,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-local-bitvector-analysis"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
       parameter_assignments(goto_model);
 
       // recalculate numbers, etc.
@@ -316,7 +313,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-custom-bitvector-analysis"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
       do_remove_returns();
       parameter_assignments(goto_model);
 
@@ -341,7 +337,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-escape-analysis"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
       do_remove_returns();
       parameter_assignments(goto_model);
 
@@ -358,7 +353,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("custom-bitvector-analysis"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
       do_remove_returns();
       parameter_assignments(goto_model);
 
@@ -388,7 +382,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-points-to"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
 
       // recalculate numbers, etc.
       goto_model.goto_functions.update();
@@ -405,7 +398,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-intervals"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
 
       // recalculate numbers, etc.
       goto_model.goto_functions.update();
@@ -434,7 +426,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("list-calls-args"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
 
       list_calls_and_arguments(goto_model);
 
@@ -448,7 +439,6 @@ int goto_instrument_parse_optionst::doit()
       if(!cmdline.isset("inline"))
       {
         do_indirect_call_and_rtti_removal();
-        do_partial_inlining();
 
         // recalculate numbers, etc.
         goto_model.goto_functions.update();
@@ -977,8 +967,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("show-custom-bitvector-analysis") ||
      cmdline.isset("custom-bitvector-analysis"))
   {
-    do_partial_inlining();
-
     status() << "Propagating Constants" << eom;
     constant_propagator_ait constant_propagator_ai(goto_model);
     remove_skip(goto_model);
@@ -987,7 +975,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("escape-analysis"))
   {
     do_indirect_call_and_rtti_removal();
-    do_partial_inlining();
     do_remove_returns();
     parameter_assignments(goto_model);
 
@@ -1082,9 +1069,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("partial-inline"))
   {
     do_indirect_call_and_rtti_removal();
-
-    status() << "Partial inlining" << eom;
-    goto_partial_inline(goto_model, get_message_handler(), true);
+    do_partial_inlining();
 
     goto_model.goto_functions.update();
     goto_model.goto_functions.compute_loop_numbers();
@@ -1172,7 +1157,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
      cmdline.isset("concurrency"))
   {
     do_indirect_call_and_rtti_removal();
-    do_partial_inlining();
 
     status() << "Pointer Analysis" << eom;
     value_set_analysist value_set_analysis(ns);

src/goto-programs/Makefile

@@ -23,6 +23,7 @@ SRC = basic_blocks.cpp \
       goto_program_template.cpp \
       goto_trace.cpp \
       graphml_witness.cpp \
+      instrument_preconditions.cpp \
       interpreter.cpp \
       interpreter_evaluate.cpp \
       json_goto_trace.cpp \

src/goto-programs/builtin_functions.cpp

@@ -1113,7 +1113,8 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
   }
-  else if(identifier==CPROVER_PREFIX "assert")
+  else if(identifier==CPROVER_PREFIX "assert" ||
+          identifier==CPROVER_PREFIX "precondition")
   {
     if(arguments.size()!=2)
     {
@@ -1123,16 +1124,28 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
+    bool is_precondition=
+      identifier==CPROVER_PREFIX "precondition";
+
     const irep_idt description=
       get_string_constant(arguments[1]);
 
     goto_programt::targett t=dest.add_instruction(ASSERT);
     t->guard=arguments[0];
     t->source_location=function.source_location();
-    t->source_location.set(
-      "user-provided",
-      !function.source_location().is_built_in());
-    t->source_location.set_property_class(ID_assertion);
+
+    if(is_precondition)
+    {
+      t->source_location.set_property_class(ID_precondition);
+    }
+    else
+    {
+      t->source_location.set(
+        "user-provided",
+        !function.source_location().is_built_in());
+      t->source_location.set_property_class(ID_assertion);
+    }
+
     t->source_location.set_comment(description);
 
     // let's double-check the type of the argument