Add a __CPROVER_postcondition builtin

The added builtin function, is transformed into an assert (like __CPROVER_precondition)
by the goto-cc pass. The reason why it was added, is to allow an analysis on the AST
to extract the postconditions from function bodies, to extend their function contracts.

Author: angelhof

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);
 
 // NOLINTNEXTLINE(build/deprecated)
 void __CPROVER_input(const char *description, ...);

src/goto-programs/builtin_functions.cpp

@@ -736,7 +736,8 @@ void goto_convertt::do_function_call_symbol(
     }
   }
   else if(identifier==CPROVER_PREFIX "assert" ||
-          identifier==CPROVER_PREFIX "precondition")
+          identifier==CPROVER_PREFIX "precondition" ||
+          identifier==CPROVER_PREFIX "postcondition")
   {
     if(arguments.size()!=2)
     {
@@ -747,6 +748,8 @@ 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)