Adds a code contract module to goto-instrument

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

Author: feliperodri

CODEOWNERS

@@ -45,8 +45,8 @@
 /src/goto-analyzer/ @martin-cs @chrisr-diffblue @peterschrammel
 /src/goto-harness/ @martin-cs @chrisr-diffblue @peterschrammel
 /src/goto-instrument/ @martin-cs @chrisr-diffblue @peterschrammel
-/src/goto-instrument/code_contracts.* @tautschnig @feliperodri @SaswatPadhi
-doc/cprover-manual/contracts* @tautschnig @feliperodri @SaswatPadhi
+/src/goto-instrument/contracts/ @tautschnig @feliperodri @SaswatPadhi
+/doc/cprover-manual/contracts* @tautschnig @feliperodri @SaswatPadhi
 /src/goto-diff/ @tautschnig @peterschrammel
 /src/jsil/ @kroening @tautschnig
 /src/memory-analyzer/ @tautschnig @chrisr-diffblue

src/goto-instrument/Makefile

@@ -16,9 +16,9 @@ SRC = accelerate/accelerate.cpp \
       alignment_checks.cpp \
       branch.cpp \
       call_sequences.cpp \
-      contracts_assigns.cpp \
-      contracts_memory_predicates.cpp \
-      contracts.cpp \
+      contracts/assigns.cpp \
+      contracts/memory_predicates.cpp \
+      contracts/contracts.cpp \
       concurrency.cpp \
       count_eloc.cpp \
       cover.cpp \

src/goto-instrument/contracts_assigns.cpp renamed to src/goto-instrument/contracts/assigns.cpp

@@ -11,7 +11,7 @@ Date: July 2021
 /// \file
 /// Specify write set in function contracts
 
-#include "contracts_assigns.h"
+#include "assigns.h"
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
@@ -328,4 +328,4 @@ exprt assigns_clauset::compatible_expression(
   }
 
   return result;
-}
+}

src/goto-instrument/contracts_assigns.h renamed to src/goto-instrument/contracts/assigns.h

@@ -87,4 +87,4 @@ class assigns_clauset
   messaget log;
 };
 
-#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
+#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H

src/goto-instrument/contracts.cpp renamed to src/goto-instrument/contracts/contracts.cpp

@@ -11,8 +11,9 @@ Date: February 2016
 /// \file
 /// Verify and use annotated invariants and pre/post-conditions
 
-#include "contracts_assigns.h"
-#include "contracts_memory_predicates.h"
+#include "contracts.h"
+#include "assigns.h"
+#include "memory_predicates.h"
 
 #include <algorithm>
 #include <map>
@@ -21,8 +22,6 @@ Date: February 2016
 
 #include <ansi-c/c_expr.h>
 
-#include <goto-instrument/contracts_memory_predicates.h>
-
 #include <goto-programs/remove_skip.h>
 
 #include <util/c_types.h>
@@ -162,8 +161,8 @@ void code_contractst::check_apply_loop_contracts(
 
     // Generate: an assignment to store the decreases clause's value before the
     // loop
-    code_assignt old_decreases_assignment{
-      old_decreases_symbol, decreases_clause};
+    code_assignt old_decreases_assignment{old_decreases_symbol,
+                                          decreases_clause};
     old_decreases_assignment.add_source_location() = loop_head->source_location;
     converter.goto_convert(old_decreases_assignment, havoc_code, mode);
   }
@@ -200,8 +199,8 @@ void code_contractst::check_apply_loop_contracts(
 
     // Generate: an assignment to store the decreases clause's value after one
     // iteration of the loop
-    code_assignt new_decreases_assignment{
-      new_decreases_symbol, decreases_clause};
+    code_assignt new_decreases_assignment{new_decreases_symbol,
+                                          decreases_clause};
     new_decreases_assignment.add_source_location() = loop_head->source_location;
     converter.goto_convert(new_decreases_assignment, havoc_code, mode);
 
@@ -1261,4 +1260,4 @@ bool code_contractst::enforce_contracts(
       fail = enforce_contract(fun);
   }
   return fail;
-}
+}

src/goto-instrument/contracts.h renamed to src/goto-instrument/contracts/contracts.h

@@ -19,6 +19,8 @@ Date: February 2016
 #include <string>
 #include <unordered_set>
 
+#include <goto-instrument/loop_utils.h>
+
 #include <goto-programs/goto_convert_class.h>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
@@ -29,8 +31,6 @@ Date: February 2016
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 
-#include "loop_utils.h"
-
 #define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
 #define HELP_LOOP_CONTRACTS                                                    \
   " --apply-loop-contracts\n"                                                  \

src/goto-instrument/contracts_memory_predicates.cpp renamed to src/goto-instrument/contracts/memory_predicates.cpp

@@ -11,7 +11,7 @@ Date: July 2021
 /// \file
 /// Predicates to specify memory footprint in function contracts
 
-#include "contracts_memory_predicates.h"
+#include "memory_predicates.h"
 
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/expr2c.h>

src/goto-instrument/contracts_memory_predicates.h renamed to src/goto-instrument/contracts/memory_predicates.h

@@ -156,4 +156,4 @@ class function_binding_visitort : const_expr_visitort
   }
 };
 
-#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
+#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H

src/goto-instrument/contracts/module_dependencies.txt

@@ -0,0 +1,8 @@
+analyses
+ansi-c
+goto-instrument/contracts
+goto-instrument
+goto-programs
+langapi
+linking
+util

src/goto-instrument/goto_instrument_parse_options.h

@@ -29,7 +29,7 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/goto_check.h>
 
 #include "aggressive_slicer.h"
-#include "contracts.h"
+#include "contracts/contracts.h"
 #include "generate_function_bodies.h"
 #include "insert_final_assert_false.h"
 #include "nondet_volatile.h"

src/goto-instrument/module_dependencies.txt

@@ -2,6 +2,7 @@ accelerate
 analyses
 ansi-c
 assembler
+contracts
 cpp
 goto-instrument
 goto-programs