Merge pull request #6108 from feliperodri/error-msg-contracts

feliperodri · web-flow · commit 185cc4cb5ad4 · 2021-05-26T16:57:50.000-04:00
Add source location and comments to assertions generated from function contracts
diff --git a/regression/contracts/assigns_enforce_scoping_01/test.desc b/regression/contracts/assigns_enforce_scoping_01/test.desc
@@ -3,8 +3,9 @@ main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-assertion: SUCCESS$
-assertion: FAILURE$
+^\[f1.\d+\] line \d+ Check that b is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that \*b is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/assigns_enforce_scoping_02/test.desc b/regression/contracts/assigns_enforce_scoping_02/test.desc
@@ -3,8 +3,8 @@ main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-assertion: SUCCESS$
-assertion: FAILURE$
+^\[f1.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that \*b is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/quantifiers-exists-both-enforce/test.desc b/regression/contracts/quantifiers-exists-both-enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-exists-both-replace/test.desc b/regression/contracts/quantifiers-exists-both-replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-all-calls-with-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-exists-requires-enforce/test.desc b/regression/contracts/quantifiers-exists-requires-enforce/test.desc
@@ -3,7 +3,11 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[f1.\d+\] line \d+ Check that found\_four is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that found\_four is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-exists-requires-replace/test.desc b/regression/contracts/quantifiers-exists-requires-replace/test.desc
@@ -3,8 +3,8 @@ main.c
 --replace-all-calls-with-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
-^\[2\] assertion: FAILURE$
+^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
+^\[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-both-enforce/test.desc b/regression/contracts/quantifiers-forall-both-enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-both-replace/test.desc b/regression/contracts/quantifiers-forall-both-replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-all-calls-with-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc
@@ -3,7 +3,10 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that arr\[\(.*\)i\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-requires-enforce/test.desc b/regression/contracts/quantifiers-forall-requires-enforce/test.desc
@@ -3,7 +3,11 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[f1.\d+\] line \d+ Check that is\_identity is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that is\_identity is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-requires-replace/test.desc b/regression/contracts/quantifiers-forall-requires-replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-all-calls-with-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
@@ -441,6 +441,11 @@ bool code_contractst::apply_function_contract(
       code_assertt(requires),
       assertion,
       symbol_table.lookup_ref(function).mode);
+    assertion.instructions.front().source_location = requires.source_location();
+    assertion.instructions.back().source_location.set_comment(
+      "Check requires clause");
+    assertion.instructions.front().source_location.set_property_class(
+      ID_precondition);
     auto lines_to_iterate = assertion.instructions.size();
     goto_program.insert_before_swap(target, assertion);
     std::advance(target, lines_to_iterate);
@@ -563,7 +568,8 @@ void code_contractst::instrument_assign_statement(
   alias_assertion.add(goto_programt::make_assertion(
     assigns_clause.alias_expression(lhs),
     instruction_iterator->source_location));
-
+  alias_assertion.instructions.back().source_location.set_comment(
+    "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable");
   int lines_to_iterate = alias_assertion.instructions.size();
   program.insert_before_swap(instruction_iterator, alias_assertion);
   std::advance(instruction_iterator, lines_to_iterate);
@@ -626,6 +632,9 @@ void code_contractst::instrument_call_statement(
     goto_programt alias_assertion;
     alias_assertion.add(goto_programt::make_assertion(
       alias_expr, instruction_iterator->source_location));
+    alias_assertion.instructions.back().source_location.set_comment(
+      "Check that " + from_expr(ns, alias_expr.id(), alias_expr) +
+      " is assignable");
     program.insert_before_swap(instruction_iterator, alias_assertion);
     ++instruction_iterator;
   }
@@ -661,6 +670,8 @@ void code_contractst::instrument_call_statement(
     goto_programt alias_assertion;
     alias_assertion.add(goto_programt::make_assertion(
       compatible, instruction_iterator->source_location));
+    alias_assertion.instructions.back().source_location.set_comment(
+      "Check compatibility of assigns clause with the called function");
     program.insert_before_swap(instruction_iterator, alias_assertion);
     ++instruction_iterator;
   }
@@ -1003,8 +1014,13 @@ void code_contractst::add_contract_check(
 
     // get all the relevant instructions related to history variables
     auto assertion = code_assertt(ensures);
+    assertion.add_source_location() = ensures.source_location();
     ensures_pair = create_ensures_instruction(
       assertion, ensures.source_location(), wrapper_fun, function_symbol.mode);
+    ensures_pair.first.instructions.back().source_location.set_comment(
+      "Check ensures clause");
+    ensures_pair.first.instructions.front().source_location.set_property_class(
+      ID_postcondition);
 
     // add all the history variable initializations
     check.destructive_append(ensures_pair.second);
diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h
@@ -23,6 +23,8 @@ Date: February 2016
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
+#include <langapi/language_util.h>
+
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
