---

yaml
---
r: 83303
b: refs/heads/variant-submodule
c: 2c32f86
h: refs/heads/develop
i:
  83301: f384b98
  83299: 5ada16b
  83295: 6b5139e

Author: feliperodri

[refs]

@@ -131,7 +131,7 @@ refs/heads/unwind-counters4: 57aedaa3fe3995b30ba69c96c9f04df79f8e8ff8
 refs/heads/value-set-make-member: 0f8404cb460f55d43bc253e12f1bde7fd7ed4d37
 refs/heads/value-set-member-fix: 2c87bd4c0d9e1954e2de6af0118fa1ef296ae548
 "refs/heads/value_set_fi_hacks": 3d243543adb4ff450596e7994e2fa1d590ec1e1b
-refs/heads/variant-submodule: a0646ecf24dfe0686ad5b2eedde0144d839185b2
+refs/heads/variant-submodule: 2c32f86edeb62a6fbb39268e605f2299bcbedd87
 refs/heads/windows-console-streambuf: b984ac7bd772da956bb5656f0072d85b3fdbbf34
 refs/tags/cbmc-5.10: 097cf712f57d59cff9c53a9fb7b9b81be1245f93
 refs/tags/cbmc-5.11: 90d0de91b0918c9e5d5ed250cae62241ae38392a

branches/variant-submodule/doc/cprover-manual/contracts-assigns.md

@@ -6,7 +6,7 @@
 __CPROVER_assigns(*identifier*, ...)
 ```
 
-An _assigns_ clause allows the user to specify that a memory location may be written by a function. The set of locations writable by a function is the union of the locations specified by the assigns clauses, or the empty set of no _assigns_ clause is specified. While, in general, an _assigns_ clause could be interpreted with wither _writes_ or _modifies_ semantics, this
+An _assigns_ clause allows the user to specify that a memory location may be written by a function. The set of locations writable by a function is the union of the locations specified by the assigns clauses, or the empty set of no _assigns_ clause is specified. While, in general, an _assigns_ clause could be interpreted with either _writes_ or _modifies_ semantics, this
 design is based on the former. This means that memory not captured by an
 _assigns_ clause must not be written within the given function, even if the
 value(s) therein are not modified.
@@ -15,10 +15,11 @@ value(s) therein are not modified.
 
 An _assigns_ clause currently supports simple variable types and their pointers,
 structs, and arrays.  Recursive pointer structures are left to future work, as
-their support would require changes to CBMC's memory model. For example,
+their support would require changes to CBMC's memory model.
 
 ```c
-int *err_signal; // Global variable
+/* Examples */
+int err_signal; // Global variable
 
 int sum(const uint32_t a, const uint32_t b, uint32_t* out)
 __CPROVER_assigns(*out)
@@ -49,10 +50,10 @@ int sum(const uint32_t a, const uint32_t b, uint32_t* out)
 /* Writable Set */
 __CPROVER_assigns(*out)
 {
-    const uint64_t result = ((uint64_t) a) + ((uint64_t) b);
-    if (result > UINT32_MAX) return FAILURE;
-    *out = (uint32_t) result;
-    return SUCCESS;
+  const uint64_t result = ((uint64_t) a) + ((uint64_t) b);
+  if (result > UINT32_MAX) return FAILURE;
+  *out = (uint32_t) result;
+  return SUCCESS;
 }
 ```
 
@@ -65,28 +66,28 @@ is one of those options.
 ```c
 int __CPROVER_contracts_original_sum(const uint32_t a, const uint32_t b, uint32_t* out)
 {
-	 const uint64_t result;
-	 __CPROVER_assert((__CPROVER_POINTER_OBJECT(&result) == __CPROVER_POINTER_OBJECT(out)  &&
-	                   __CPROVER_POINTER_OFFSET(&result) == __CPROVER_POINTER_OFFSET(out)) ||
-	                  (__CPROVER_POINTER_OBJECT(&result) == __CPROVER_POINTER_OBJECT(&result)  &&
-	                   __CPROVER_POINTER_OFFSET(&result) == __CPROVER_POINTER_OFFSET(&result))
-	 , "Check that result is assignable");
-    result = ((uint64_t) *a) + ((uint64_t) *b);
-    if (result > UINT32_MAX) return FAILURE;
-    __CPROVER_assert((__CPROVER_POINTER_OBJECT(out) == __CPROVER_POINTER_OBJECT(out)  &&
-                      __CPROVER_POINTER_OFFSET(out) == __CPROVER_POINTER_OFFSET(out)) ||
-	                  (__CPROVER_POINTER_OBJECT(out) == __CPROVER_POINTER_OBJECT(&result)  &&
-	                   __CPROVER_POINTER_OFFSET(out) == __CPROVER_POINTER_OFFSET(&result))
-	 , "Check that result is assignable");
-    *out = (uint32_t) result;
-    return SUCCESS;
+  const uint64_t result;
+  __CPROVER_assert((__CPROVER_POINTER_OBJECT(&result) == __CPROVER_POINTER_OBJECT(out)  &&
+                    __CPROVER_POINTER_OFFSET(&result) == __CPROVER_POINTER_OFFSET(out)) ||
+                   (__CPROVER_POINTER_OBJECT(&result) == __CPROVER_POINTER_OBJECT(&result)  &&
+                    __CPROVER_POINTER_OFFSET(&result) == __CPROVER_POINTER_OFFSET(&result))
+                   , "Check that result is assignable");
+  result = ((uint64_t) a) + ((uint64_t) b);
+  if (result > UINT32_MAX) return FAILURE;
+  __CPROVER_assert((__CPROVER_POINTER_OBJECT(out) == __CPROVER_POINTER_OBJECT(out)  &&
+                     __CPROVER_POINTER_OFFSET(out) == __CPROVER_POINTER_OFFSET(out)) ||
+                    (__CPROVER_POINTER_OBJECT(out) == __CPROVER_POINTER_OBJECT(&result)  &&
+                     __CPROVER_POINTER_OFFSET(out) == __CPROVER_POINTER_OFFSET(&result))
+                    , "Check that result is assignable");
+  *out = (uint32_t) result;
+  return SUCCESS;
 }
 
 /* Function Contract Enforcement */
 int sum(const uint32_t a, const uint32_t b, uint32_t* out)
 {
-    int return_value_sum = __CPROVER_contracts_original_sum(a, b, out);
-    return return_value_sum;
+  int return_value_sum = __CPROVER_contracts_original_sum(a, b, out);
+  return return_value_sum;
 }
 ```
 
@@ -101,7 +102,8 @@ considered assignable as well.
 Finally, a set of freely-assignable symbols *free* is tracked during the
 traversal of the function body. These are locally-defined variables and formal
 parameters without dereferences.  For example, in a variable declaration `<type>
-x = <initial_value>`, `x` would be added to *free*. Assignment statements where the left-hand-side is in *free* are not instrumented with the above assertions.
+x = <initial_value>`, `x` would be added to the *free* set. Assignment statements
+where the left-hand-side is in the *free* set are not instrumented with the above assertions.
 
 #### Replacement
 
@@ -112,7 +114,7 @@ Clauses](contracts-requires-and-ensures.md) - Replacement section, and it will a
 non-deterministic assignments for each object listed in the `__CPROVER_assigns`
 clause. Since these objects might be modified by the function, CBMC uses
 non-deterministic assignments to havoc them and restrict their values only by
-assuming the postconditions.
+assuming the postconditions (i.e., requires clauses).
 
 In our example, consider that a function `foo` may call `sum`.
 
@@ -126,21 +128,21 @@ __CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (a + b)))
 /* Writable Set */
 __CPROVER_assigns(*out)
 {
-    const uint64_t result = ((uint64_t) a) + ((uint64_t) b);
-    if (result > UINT32_MAX) return FAILURE;
-    *out = (uint32_t) result;
-    return SUCCESS;
+  const uint64_t result = ((uint64_t) a) + ((uint64_t) b);
+  if (result > UINT32_MAX) return FAILURE;
+  *out = (uint32_t) result;
+  return SUCCESS;
 }
 
 int foo()
 {
-	uint32_t a;
-	uint32_t b;
-	uint32_t out;
-	int rval = sum(a, b, &out);
-	if (rval == SUCCESS) 
-		return out;
-	return rval;
+  uint32_t a;
+  uint32_t b;
+  uint32_t out;
+  int rval = sum(a, b, &out);
+  if (rval == SUCCESS) 
+    return out;
+  return rval;
 }
 ```
 
@@ -150,26 +152,25 @@ wherever the function is called.
 ```c
 int foo()
 {
-	uint32_t a;
-	uint32_t b;
-	uint32_t out;
+  uint32_t a;
+  uint32_t b;
+  uint32_t out;
 	
+  /* Function Contract Replacement */
+  /* Precondition */
+  __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause");
 	
-	/* Function Contract Replacement */
-	/* Precondition */
-	__CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause");
+  /* Writable Set */
+  *(&out) = nondet_uint32_t();
 	
-	/* Writable Set */
-	*(&out) = nondet_uint32_t();
-	
-	/* Postconditions */
-       int return_value_sum = nondet_int();
-	__CPROVER_assume(return_value_sum == SUCCESS || return_value_sum == FAILURE);
-	__CPROVER_assume((return_value_sum == SUCCESS) ==> (*out == (*a + *b)));
-
-	int rval = return_value_sum;
-	if (rval == SUCCESS) 
-		return out;
-	return rval;
+  /* Postconditions */
+  int return_value_sum = nondet_int();
+  __CPROVER_assume(return_value_sum == SUCCESS || return_value_sum == FAILURE);
+  __CPROVER_assume((return_value_sum == SUCCESS) ==> (*out == (a + b)));
+
+  int rval = return_value_sum;
+  if (rval == SUCCESS) 
+    return out;
+  return rval;
 }
 ```

branches/variant-submodule/doc/cprover-manual/contracts-history-variables.md

@@ -14,8 +14,7 @@ _ensures_ clause.
 ### Parameters
 
 `__CPROVER_old` takes a single argument, which is the identifier corresponding to
-a parameter of the function. For now, only scalar, structs, or pointer types are supported.
-
+a parameter of the function. For now, only scalar or pointer types are supported.
 
 ### Semantics
 
@@ -24,13 +23,12 @@ bellow.  If the function returns a failure code, the value of `*out` should not
 have been modified.
 
 ```c
-int sum(uint32_t* a, uint32_t* b, uint32_t* out)
-
+int sum(const uint32_t a, const uint32_t b, uint32_t* out)
 /* Postconditions */
 __CPROVER_ensures((__CPROVER_return_value == FAILURE) ==> (*out == __CPROVER_old(*out)))
 /* Writable Set */
 __CPROVER_assigns(*out)
 {
-    /* ... */
+  /* ... */
 }
 ```

branches/variant-submodule/doc/cprover-manual/contracts-memory-predicates.md

@@ -1,14 +1,13 @@
 # Memory Predicates
 
-
 ### Syntax
 
 ```c
 bool __CPROVER_is_fresh(void *p, size_t size);
 ```
 
 To specify memory footprint we use a special function called `__CPROVER_is_fresh `. The meaning of `__CPROVER_is_fresh` is that we are borrowing a pointer from the
-external environment (in a precondition), or returning it to the calling context  (in a postcondition).
+external environment (in a precondition), or returning it to the calling context (in a postcondition).
 
 ### Parameters
 
@@ -33,12 +32,12 @@ __CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out)))
 __CPROVER_ensures(__CPROVER_is_fresh(err_signal, sizeof(*err_signal)))
 __CPROVER_assigns(*out, err_signal)
 {
-    const uint64_t result = ((uint64_t) a) + ((uint64_t) b);
-    err_signal = malloc(sizeof(*err_signal));
-    if (!err_signal) return;
-    if (result > UINT32_MAX) *err_signal = FAILURE;
-    *out = (uint32_t) result;
-    *err_signal = SUCCESS;
+  const uint64_t result = ((uint64_t) a) + ((uint64_t) b);
+  err_signal = malloc(sizeof(*err_signal));
+  if (!err_signal) return;
+  if (result > UINT32_MAX) *err_signal = FAILURE;
+  *out = (uint32_t) result;
+  *err_signal = SUCCESS;
 }
 ```
 
@@ -53,21 +52,21 @@ int *err_signal; // Global variable
 
 int __CPROVER_contracts_original_sum(const uint32_t a, const uint32_t b, uint32_t* out)
 {	 
-    const uint64_t result = ((uint64_t) a) + ((uint64_t) b);
-    err_signal = malloc(sizeof(*err_signal));
-    if (!err_signal) return;
-    if (result > UINT32_MAX) *err_signal = FAILURE;
-    *out = (uint32_t) result;
-    *err_signal = SUCCESS;
+  const uint64_t result = ((uint64_t) a) + ((uint64_t) b);
+  err_signal = malloc(sizeof(*err_signal));
+  if (!err_signal) return;
+  if (result > UINT32_MAX) *err_signal = FAILURE;
+  *out = (uint32_t) result;
+  *err_signal = SUCCESS;
 }
 
 /* Function Contract Enforcement */
 int sum(const uint32_t a, const uint32_t b, uint32_t* out)
 {
-    __CPROVER_assume(__CPROVER_is_fresh(out, sizeof(*out))); // Assumes out is freshly allocated
-    int return_value_sum = __CPROVER_contracts_original_sum(a, b, out);
-	 __CPROVER_assert(__CPROVER_is_fresh(err_signal, sizeof(*err_signal)), "Check ensures clause");
-    return return_value_sum;
+  __CPROVER_assume(__CPROVER_is_fresh(out, sizeof(*out))); // Assumes out is freshly allocated
+  int return_value_sum = __CPROVER_contracts_original_sum(a, b, out);
+  __CPROVER_assert(__CPROVER_is_fresh(err_signal, sizeof(*err_signal)), "Check ensures clause");
+  return return_value_sum;
 }
 ```
 
@@ -80,11 +79,11 @@ int *err_signal; // Global variable
 
 int foo()
 {
-	uint32_t a;
-	uint32_t b;
-	uint32_t out;
-	sum(a, b, &out);
-	return *err_signal;
+  uint32_t a;
+  uint32_t b;
+  uint32_t out;
+  sum(a, b, &out);
+  return *err_signal;
 }
 ```
 
@@ -98,21 +97,21 @@ int *err_signal; // Global variable
 
 int foo()
 {
-	uint32_t a;
-	uint32_t b;
-	uint32_t out;
+  uint32_t a;
+  uint32_t b;
+  uint32_t out;
 
-	/* Function Contract Replacement */
-	/* Precondition */
-	__CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause");
+  /* Function Contract Replacement */
+  /* Precondition */
+  __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause");
 
-	/* Writable Set */
-	*(&out) = nondet_uint32_t();
-	err_signal = nondet_int_pointer();
+  /* Writable Set */
+  *(&out) = nondet_uint32_t();
+  err_signal = nondet_int_pointer();
 
-	/* Postconditions */
-	__CPROVER_assume(__CPROVER_is_fresh(err_signal, sizeof(*err_signal))); // Assumes out is allocated
+  /* Postconditions */
+  __CPROVER_assume(__CPROVER_is_fresh(err_signal, sizeof(*err_signal))); // Assumes out is allocated
 
-	return *err_signal;
+  return *err_signal;
 }
-```
+```