precondition messages now include condition

Author: kroening

regression/cprover/contracts/check_precondition1.desc

@@ -3,6 +3,6 @@ check_precondition1.c
 
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.precondition\.1\] line \d+ precondition my_function: REFUTED$
-^\[main\.precondition\.2\] line \d+ precondition my_function: SUCCESS$
+^\[main\.precondition\.1\] line \d+ my_function precondition .*: REFUTED$
+^\[main\.precondition\.2\] line \d+ my_function precondition .*: SUCCESS$
 --

regression/cprover/contracts/check_precondition2.desc

@@ -3,5 +3,5 @@ check_precondition2.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[caller\.precondition\.1\] line \d+ precondition callee: SUCCESS$
+^\[caller\.precondition\.1\] line \d+ callee precondition parameter >= 10: SUCCESS$
 --

regression/cprover/contracts/nested1.desc

@@ -4,5 +4,5 @@ nested1.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[caller\.assertion\.1\] line \d+ property 1: SUCCESS$
-^\[caller\.precondition\.1\] line \d+ precondition callee: SUCCESS$
+^\[caller\.precondition\.1\] line \d+ callee precondition .*: SUCCESS$
 --

regression/cprover/contracts/recursive_function1.desc

@@ -3,5 +3,5 @@ recursive_function1.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^\[recursive_function\.precondition\.1] line \d+ precondition recursive_function: SUCCESS$
+^\[recursive_function\.precondition\.1] line \d+ recursive_function precondition.*: SUCCESS$
 --

src/cprover/instrument_contracts.cpp

@@ -19,8 +19,21 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_model.h>
 
+#include <ansi-c/expr2c.h>
+
 #include <iostream>
 
+#define MAX_TEXT 20
+
+static std::string expr2text(const exprt &src, const namespacet &ns)
+{
+  auto text = expr2c(src, ns);
+  if(text.size() >= MAX_TEXT)
+    return std::string(text, 0, MAX_TEXT - 3) + "...";
+  else
+    return text;
+}
+
 static exprt make_address(exprt src)
 {
   if(src.id() == ID_dereference)
@@ -328,7 +341,8 @@ void replace_function_calls_by_contracts(
           auto location = it->source_location();
           location.set_property_class(ID_precondition);
           location.set_comment(
-            "precondition " + id2string(symbol.display_name()));
+            id2string(symbol.display_name()) + " precondition " +
+            expr2text(precondition, ns));
 
           auto replaced_precondition = precondition;
           replace_symbol(replaced_precondition);