added __CPROVER_precondtion(c, d)

smowton · Sep 16, 2017 · 54e80da · 54e80da
1 parent 1d81035
commit 54e80da
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 5 deletions.
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/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"

diff --git a/src/ansi-c/library/cprover.h b/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 *);

diff --git a/src/goto-programs/builtin_functions.cpp b/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

diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
@@ -90,6 +90,7 @@ IREP_ID_ONE(assign_bitor)
 IREP_ID_ONE(assume)
 IREP_ID_ONE(assert)
 IREP_ID_ONE(assertion)
+IREP_ID_ONE(precondition)
 IREP_ID_ONE(goto)
 IREP_ID_ONE(gcc_computed_goto)
 IREP_ID_ONE(ifthenelse)