postcondition messages now include condition

Author: kroening

regression/cprover/contracts/check_postcondition4.c

@@ -0,0 +1,10 @@
+int x, y;
+
+void my_function()
+  __CPROVER_ensures(x == 10) // passes
+  __CPROVER_ensures(y == 20) // fails
+  __CPROVER_assigns(x, y)
+{
+  x = 10;
+  y = 10;
+}

regression/cprover/contracts/check_postcondition4.desc

@@ -0,0 +1,8 @@
+CORE
+check_postcondition4.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[my_function\.postcondition\.2\] line \d+ postcondition x == 10: SUCCESS$
+^\[my_function\.postcondition\.1\] line \d+ postcondition y == 20: REFUTED$
+--

src/cprover/instrument_contracts.cpp

@@ -229,10 +229,14 @@ void instrument_contract_checks(
 
     for(auto &assertion : contract.ensures())
     {
+      std::string comment = "postcondition";
+      if(contract.ensures().size() >= 2)
+        comment += " " + expr2text(assertion, ns);
+
       auto location = assertion.source_location();
       location.set_function(f.first); // seems to be missing
       location.set_property_class(ID_postcondition);
-      location.set_comment("postcondition");
+      location.set_comment(comment);
 
       auto replaced_assertion = replace_old(assertion, f.first, old_exprs);