Merge pull request #6234 from feliperodri/clean-up-contracts

Refactoring code contracts implementation

Author: martin-cs

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

regression/contracts/assigns_replace_06/test.desc

@@ -1,9 +1,9 @@
 CORE
 main.c
 --replace-all-calls-with-contracts
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 --
 --
 Checks whether the values outside the array range specified by the assigns

regression/contracts/assigns_type_checking_valid_cases/main.c

@@ -3,10 +3,15 @@
 int *x;
 int y;
 
+struct blob
+{
+  int allocated;
+};
 struct buf
 {
   int *data;
   size_t len;
+  struct blob aux;
 };
 
 void foo1(int a) __CPROVER_assigns(a)
@@ -76,9 +81,10 @@ void foo9(int array[]) __CPROVER_assigns(array)
 }
 
 void foo10(struct buf *buffer) __CPROVER_requires(buffer != NULL)
-  __CPROVER_assigns(*buffer)
+  __CPROVER_assigns(buffer->len, buffer->aux.allocated)
 {
   buffer->len = 0;
+  buffer->aux.allocated = 0;
 }
 
 int main()

src/ansi-c/ansi_c_convert_type.cpp

@@ -257,7 +257,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     {
       if(
         operand.id() != ID_symbol && operand.id() != ID_ptrmember &&
-        operand.id() != ID_dereference)
+        operand.id() != ID_member && operand.id() != ID_dereference)
       {
         error().source_location = source_location;
         error() << "illegal target in assigns clause" << eom;

src/goto-instrument/Makefile

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