Adds a code contract module to goto-instrument

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

src/ansi-c/c_typecheck_base.h

@@ -144,6 +144,7 @@ class c_typecheck_baset:
   virtual void typecheck_while(code_whilet &code);
   virtual void typecheck_dowhile(code_dowhilet &code);
   virtual void typecheck_start_thread(codet &code);
+  virtual void typecheck_spec_assigns(codet &code);
   virtual void typecheck_spec_loop_invariant(codet &code);
   virtual void typecheck_spec_decreases(codet &code);
 

src/ansi-c/c_typecheck_code.cpp

@@ -484,6 +484,7 @@ void c_typecheck_baset::typecheck_for(codet &code)
     typecheck_code(code); // recursive call
   }
 
+  typecheck_spec_assigns(code);
   typecheck_spec_loop_invariant(code);
   typecheck_spec_decreases(code);
 }
@@ -773,6 +774,7 @@ void c_typecheck_baset::typecheck_while(code_whilet &code)
   break_is_allowed=old_break_is_allowed;
   continue_is_allowed=old_continue_is_allowed;
 
+  typecheck_spec_assigns(code);
   typecheck_spec_loop_invariant(code);
   typecheck_spec_decreases(code);
 }
@@ -807,10 +809,29 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
   break_is_allowed=old_break_is_allowed;
   continue_is_allowed=old_continue_is_allowed;
 
+  typecheck_spec_assigns(code);
   typecheck_spec_loop_invariant(code);
   typecheck_spec_decreases(code);
 }
 
+void c_typecheck_baset::typecheck_spec_assigns(codet &code)
+{
+  if(code.find(ID_C_spec_assigns).is_not_nil())
+  {
+    for(const exprt &operand : static_cast<exprt &>(code.add(ID_C_spec_assigns)).operands())
+    {
+      if(
+        operand.id() != ID_symbol && operand.id() != ID_ptrmember &&
+        operand.id() != ID_member && operand.id() != ID_dereference)
+      {
+        error().source_location = code.source_location();
+        error() << "illegal target in assigns clause" << eom;
+        throw 0;
+      }
+    }
+  }
+}
+
 void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
 {
   if(code.find(ID_C_spec_loop_invariant).is_not_nil())

src/ansi-c/parser.y

@@ -2453,6 +2453,9 @@ iteration_statement:
           statement($$, ID_while);
           parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($8)));
 
+          if(!parser_stack($4).is_not_nil())
+            parser_stack($$).add(ID_C_spec_assigns).swap(parser_stack($4)); 
+
           if(!parser_stack($6).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands());
 
@@ -2468,6 +2471,9 @@ iteration_statement:
           statement($$, ID_dowhile);
           parser_stack($$).add_to_operands(std::move(parser_stack($5)), std::move(parser_stack($2)));
 
+          if(!parser_stack($7).is_not_nil())
+            parser_stack($$).add(ID_C_spec_assigns).swap(parser_stack($7));
+
           if(!parser_stack($8).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands());
 
@@ -2499,6 +2505,9 @@ iteration_statement:
           mto($$, $7);
           mto($$, $12);
 
+          if(!parser_stack($9).is_not_nil())
+            parser_stack($$).add(ID_C_spec_assigns).swap(parser_stack($9));
+
           if(!parser_stack($10).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($10).operands());
 
@@ -3305,6 +3314,13 @@ cprover_contract_assigns:
         ;
 
 cprover_contract_assigns_opt:
+        /* nothing */
+        { init($$); parser_stack($$).make_nil(); }
+        | TOK_CPROVER_ASSIGNS '(' argument_expression_list ')'
+        { $$=$3; }
+        ;
+
+cprover_contract_assigns_opt_old:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
         | cprover_contract_assigns

src/goto-instrument/contracts/assigns.cpp

@@ -238,6 +238,11 @@ goto_programt assigns_clauset::havoc_code(
   return havoc_statements;
 }
 
+std::vector<assigns_clause_targett *> assigns_clauset::getTargets()
+{
+    return targets;
+}
+
 exprt assigns_clauset::alias_expression(const exprt &lhs)
 {
   if(targets.empty())

src/goto-instrument/contracts/assigns.h

@@ -73,6 +73,7 @@ class assigns_clauset
     irep_idt function_name,
     irep_idt language_mode);
   exprt alias_expression(const exprt &lhs);
+  std::vector<assigns_clause_targett *> getTargets();
 
   exprt compatible_expression(const assigns_clauset &called_assigns);
 

src/goto-instrument/contracts/contracts.cpp

@@ -12,7 +12,10 @@ Date: February 2016
 /// Verify and use annotated invariants and pre/post-conditions
 
 #include "contracts.h"
+<<<<<<< HEAD:src/goto-instrument/contracts/contracts.cpp
 
+=======
+>>>>>>> b3b2ee77d... Adds a code contract module to goto-instrument:src/goto-instrument/contracts.cpp
 #include "assigns.h"
 #include "memory_predicates.h"