From 54e80da8391068a3353dde1731fde744891f9a1e Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Fri, 1 Sep 2017 11:31:33 +0100
Subject: [PATCH] added __CPROVER_precondtion(c, d)

---
 src/ansi-c/ansi_c_internal_additions.cpp |  2 ++
 src/ansi-c/library/cprover.h             |  1 +
 src/goto-programs/builtin_functions.cpp  | 23 ++++++++++++++++++-----
 src/util/irep_ids.def                    |  1 +
 4 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index aa1d82e0102..6cfe07b0e2c 100644
--- 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
index 251bb828b6f..94da717f33d 100644
--- 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
index f1a103e2428..fbf77309efe 100644
--- 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
index 92457c747f3..92afdfd3e4a 100644
--- 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)