Merge pull request #4921 from angelhof/cprover-postcondition

Add a __CPROVER_postcondition builtin

Author: karkhaz

doc/cprover-manual/cbmc-assertions.md

@@ -59,6 +59,34 @@ for(i=0; i<100; i++)
   assert(a[i]==0);
 ```
 
+CPROVER also supports writing function pre and postconditions, using
+the built-in functions `__CPROVER_precondition` and
+`__CPROVER_postcondition`. They can be used to express intent, and at
+the moment they are just transformed to assertions in the goto
+program. As such, they can be used as simple assertions in
+code. However, it is advised to use `__CPROVER_precondition` at the
+beginning of a function's body, and `__CPROVER_postcondition` before
+the exit points in a function (either the return statements, or the
+end of the body if the function returns void). The following is an
+example usage:
+
+```C
+int foo(int a, int b) {
+  __CPROVER_precondition(a >= 0);
+  __CPROVER_precondition(b > 0);
+
+  int rval = a / b;
+
+  __CPROVER_postcondition(rval >= 0);
+  return rval;
+}
+```
+
+A future release of CPROVER will support using these pre and
+postconditions to create a function contract, which can be used for
+modular verification.
+
+
 Future CPROVER releases will support explicit quantifiers with a syntax
 that resembles Spec\#:
 

regression/cbmc/cprover_postcondition/main.c

@@ -0,0 +1,14 @@
+int func(int a)
+{
+  __CPROVER_precondition(a > 10, "Argument should be larger than 10");
+  int rval = a - 10;
+  __CPROVER_postcondition(rval > 1, "Return value should be positive");
+  return rval;
+}
+
+int main()
+{
+  int a = 11;
+  int rval = func(a);
+  return 0;
+}

regression/cbmc/cprover_postcondition/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

regression/cbmc/cprover_precondition/main.c

@@ -0,0 +1,13 @@
+void func(int a)
+{
+  __CPROVER_precondition(a > 10, "Argument should be larger than 10.");
+}
+
+int main()
+{
+  int a = 10;
+
+  func(a);
+
+  return 0;
+}

regression/cbmc/cprover_precondition/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

src/ansi-c/cprover_builtin_headers.h

@@ -2,6 +2,7 @@ void __CPROVER_assume(__CPROVER_bool assumption);
 void __VERIFIER_assume(__CPROVER_bool assumption);
 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
 void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);
+void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
 void __CPROVER_havoc_object(void *);
 __CPROVER_bool __CPROVER_equal();
 __CPROVER_bool __CPROVER_same_object(const void *, const void *);

src/ansi-c/library/cprover.h

@@ -20,6 +20,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);
+void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
 
 __CPROVER_bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);

src/cpp/library/cprover.h

@@ -21,6 +21,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);
+void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
 
 void __CPROVER_input(const char *description, ...);
 void __CPROVER_output(const char *description, ...);

src/goto-programs/builtin_functions.cpp

@@ -735,8 +735,10 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
   }
-  else if(identifier==CPROVER_PREFIX "assert" ||
-          identifier==CPROVER_PREFIX "precondition")
+  else if(
+    identifier == CPROVER_PREFIX "assert" ||
+    identifier == CPROVER_PREFIX "precondition" ||
+    identifier == CPROVER_PREFIX "postcondition")
   {
     if(arguments.size()!=2)
     {
@@ -747,6 +749,7 @@ void goto_convertt::do_function_call_symbol(
 
     bool is_precondition=
       identifier==CPROVER_PREFIX "precondition";
+    bool is_postcondition = identifier == CPROVER_PREFIX "postcondition";
 
     const irep_idt description=
       get_string_constant(arguments[1]);
@@ -760,6 +763,10 @@ void goto_convertt::do_function_call_symbol(
     {
       t->source_location.set_property_class(ID_precondition);
     }
+    else if(is_postcondition)
+    {
+      t->source_location.set_property_class(ID_postcondition);
+    }
     else
     {
       t->source_location.set(

src/util/irep_ids.def

@@ -89,6 +89,7 @@ IREP_ID_ONE(assume)
 IREP_ID_ONE(assert)
 IREP_ID_ONE(assertion)
 IREP_ID_ONE(precondition)
+IREP_ID_ONE(postcondition)
 IREP_ID_ONE(precondition_instance)
 IREP_ID_ONE(goto)
 IREP_ID_ONE(gcc_computed_goto)