diff --git a/doc/cprover-manual/assigns-clause.md b/doc/cprover-manual/assigns-clause.md
new file mode 100644
index 00000000000..c949125de00
--- /dev/null
+++ b/doc/cprover-manual/assigns-clause.md
@@ -0,0 +1,89 @@
+## CBMC Assigns Clause
+
+
+### Introduction
+The _assigns_ clause allows the user to specify a list of memory
+locations which may be written within a particular scope. While an assigns
+clause may, in general, be interpreted with either _writes_ or _modifies_
+semantics, this design is based on the former.  This means that memory not
+captured by the assigns clause must not be written within the given scope, even
+if the value(s) therein are not modified.
+
+
+### Scalar Variables
+The initial iteration of this design focuses on specifying an assigns clause for
+primitive types and their pointers. Arrays, structured data, and pointers are
+left to future contributions.
+
+
+##### Syntax
+A special construct is introduced to specify assigns clauses. Its syntax is
+defined as follows.
+
+```
+ <assigns_clause> := __CPROVER_assigns ( <target_list> )
+```
+```
+ <target_list> := <target>
+                | <target> , <target_list>
+```
+```
+ <target> := <identifier>
+           | * <target>
+```
+
+
+The `<assigns_clause>` states that only the memory identified by the dereference
+expressions and identifiers listed in the contained `<target_list>` may be
+written within the associated scope, as follows.
+
+
+##### Semantics
+The semantics of an assigns clause *c* of some function *f* can be understood in
+two contexts. First, one may consider how the expressions in *c* are treated
+when a call to *f* is replaced by its contract specification, assuming the
+contract specification is a sound characterization of the behavior of *f*.
+Second, one may consider how *c* is applied to the function body of *f* in order
+to determine whether *c* is a sound characterization of the behavior of *f*. We
+begin by exploring these two perspectives for assigns clauses which contain only
+scalar expressions.
+
+Let the i<sup>th</sup> expression in some assigns clause *c* be denoted
+*exprs*<sub>*c*</sub>[i], the j<sup>th</sup> formal parameter of some function
+*f* be denoted *params*<sub>*f*</sub>[j], and the k<sup>th</sup> argument passed
+in a call to function *f* be denoted *args*<sub>*f*</sub>[k] (an identifying
+index may be added to distinguish a *particular* call to *f*, but for simplicity
+it is omitted here).
+
+
+###### Replacement
+Assuming an assigns clause *c* is a sound characterization of the behavior of
+the function *f*, a call  to *f* may be replaced a series of non-deterministic
+assignments. For each expression *e* &#8712; *exprs*<sub>*c*</sub>, let there be
+an assignment &#632; := &#8727;, where &#632; is *args*<sub>*f*</sub>[i] if *e*
+is identical to some *params*<sub>*f*</sub>[i], and *e* otherwise.
+
+
+###### Enforcement
+In order to determine whether an assigns clause *c* is a sound characterization
+of the behavior of a function *f*, the body of the function should be
+instrumented with additional statements as follows.
+
+- For each expression *e* &#8712; *exprs*<sub>*c*</sub>, create a temporary
+  variable *tmp*<sub>*e*</sub> to store \&(*e*), the address of *e*, at the
+start of *f*.
+- Before each assignment statement, *lhs* := *rhs*, add an assertion (structured
+  as a disjunction)
+assert(&#8707; *tmp*<sub>*e*</sub>. \_\_CPROVER\_same\_object(\&(*lhs*),
+*tmp*<sub>*e*</sub>)
+- Before each function call with an assigns clause *a*, add an assertion for
+  each *e*<sub>*a*</sub> &#8712; *exprs*<sub>*a*</sub> (also formulated as a
+disjunction)
+assert(&#8707; *tmp*<sub>*e*</sub>.
+\_\_CPROVER\_same\_object(\&(*e*<sub>*a*</sub>), *tmp*<sub>*e*</sub>)
+
+Here, \_\_CPROVER\_same\_object returns true if two pointers
+reference the same object in the CBMC memory model. Additionally, for each
+function call without an assigns clause, CBMC adds an assertion assert(*false*)
+to ensure that the assigns contract will only hold if all called functions
+have an assigns clause which is compatible with that of the calling function.
diff --git a/regression/contracts/assigns_enforce_01/main.c b/regression/contracts/assigns_enforce_01/main.c
new file mode 100644
index 00000000000..102a3870a72
--- /dev/null
+++ b/regression/contracts/assigns_enforce_01/main.c
@@ -0,0 +1,14 @@
+int foo(int *x) __CPROVER_assigns(*x)
+  __CPROVER_ensures(__CPROVER_return_value == *x + 5)
+{
+  *x = *x + 0;
+  return *x + 5;
+}
+
+int main()
+{
+  int n = 4;
+  n = foo(&n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_01/test.desc b/regression/contracts/assigns_enforce_01/test.desc
new file mode 100644
index 00000000000..7c24b33faf7
--- /dev/null
+++ b/regression/contracts/assigns_enforce_01/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds if only expressions inside the assigns clause are assigned within the function.
+
+Note: For all 'enforce' tests, nothing can be assumed about the return value of the function (as the function call is not replaced at this point).
+
+To make such assumptions would cause verification to fail.
diff --git a/regression/contracts/assigns_enforce_02/main.c b/regression/contracts/assigns_enforce_02/main.c
new file mode 100644
index 00000000000..e581b827ee6
--- /dev/null
+++ b/regression/contracts/assigns_enforce_02/main.c
@@ -0,0 +1,16 @@
+int z;
+
+int foo(int *x) __CPROVER_assigns(z)
+  __CPROVER_ensures(__CPROVER_return_value == *x + 5)
+{
+  *x = *x + 0;
+  return *x + 5;
+}
+
+int main()
+{
+  int n = 4;
+  n = foo(&n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_02/test.desc b/regression/contracts/assigns_enforce_02/test.desc
new file mode 100644
index 00000000000..f0dbbe8ceaa
--- /dev/null
+++ b/regression/contracts/assigns_enforce_02/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails if an expression outside the assigns clause is assigned within the function.
diff --git a/regression/contracts/assigns_enforce_03/main.c b/regression/contracts/assigns_enforce_03/main.c
new file mode 100644
index 00000000000..5886f49e080
--- /dev/null
+++ b/regression/contracts/assigns_enforce_03/main.c
@@ -0,0 +1,26 @@
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+{
+  f3(x2, y2, z2);
+}
+
+void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3, *y3, *z3)
+{
+  *x3 = *x3 + 1;
+  *y3 = *y3 + 1;
+  *z3 = *z3 + 1;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+  f1(&p, &q, &r);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_03/test.desc b/regression/contracts/assigns_enforce_03/test.desc
new file mode 100644
index 00000000000..05315288ad2
--- /dev/null
+++ b/regression/contracts/assigns_enforce_03/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds when assigns clauses are respected through multiple function calls.
diff --git a/regression/contracts/assigns_enforce_04/main.c b/regression/contracts/assigns_enforce_04/main.c
new file mode 100644
index 00000000000..0d0e4e4da39
--- /dev/null
+++ b/regression/contracts/assigns_enforce_04/main.c
@@ -0,0 +1,26 @@
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+{
+  f3(x2, y2, z2);
+}
+
+void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3)
+{
+  *x3 = *x3 + 1;
+  *y3 = *y3 + 1;
+  *z3 = *z3 + 1;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+  f1(&p, &q, &r);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_04/test.desc b/regression/contracts/assigns_enforce_04/test.desc
new file mode 100644
index 00000000000..ce340df66a7
--- /dev/null
+++ b/regression/contracts/assigns_enforce_04/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails when an assigns clause is not respected through multiple function calls.
diff --git a/regression/contracts/assigns_enforce_05/main.c b/regression/contracts/assigns_enforce_05/main.c
new file mode 100644
index 00000000000..fb891d002db
--- /dev/null
+++ b/regression/contracts/assigns_enforce_05/main.c
@@ -0,0 +1,23 @@
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+{
+  f3(x2, y2, z2);
+}
+
+void f3(int *x3, int *y3, int *z3)
+{
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+  f1(&p, &q, &r);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_05/test.desc b/regression/contracts/assigns_enforce_05/test.desc
new file mode 100644
index 00000000000..52c7a660e1f
--- /dev/null
+++ b/regression/contracts/assigns_enforce_05/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails when a function with an assigns clause calls a function without an assigns clause.
diff --git a/regression/contracts/assigns_enforce_06/main.c b/regression/contracts/assigns_enforce_06/main.c
new file mode 100644
index 00000000000..e4d12d140f6
--- /dev/null
+++ b/regression/contracts/assigns_enforce_06/main.c
@@ -0,0 +1,41 @@
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+{
+  f3(x2, y2, z2);
+}
+
+void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3, *y3, *z3)
+{
+  *x3 = *x3 + 1;
+  *y3 = *y3 + 1;
+  *z3 = *z3 + 1;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+
+  for(int i = 0; i < 3; ++i)
+  {
+    if(i == 0)
+    {
+      f1(&p, &q, &r);
+    }
+    if(i == 1)
+    {
+      f2(&p, &q, &r);
+    }
+    if(i == 2)
+    {
+      f3(&p, &q, &r);
+    }
+  }
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_06/test.desc b/regression/contracts/assigns_enforce_06/test.desc
new file mode 100644
index 00000000000..42959abee29
--- /dev/null
+++ b/regression/contracts/assigns_enforce_06/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds when functions with assigns clauses are called from within a loop.
diff --git a/regression/contracts/assigns_enforce_07/main.c b/regression/contracts/assigns_enforce_07/main.c
new file mode 100644
index 00000000000..384807e6218
--- /dev/null
+++ b/regression/contracts/assigns_enforce_07/main.c
@@ -0,0 +1,41 @@
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+{
+  f3(x2, y2, z2);
+}
+
+void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3)
+{
+  *x3 = *x3 + 1;
+  *y3 = *y3 + 1;
+  *z3 = *z3 + 1;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+
+  for(int i = 0; i < 3; ++i)
+  {
+    if(i == 0)
+    {
+      f1(&p, &q, &r);
+    }
+    if(i == 1)
+    {
+      f2(&p, &q, &r);
+    }
+    if(i == 2)
+    {
+      f3(&p, &q, &r);
+    }
+  }
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_07/test.desc b/regression/contracts/assigns_enforce_07/test.desc
new file mode 100644
index 00000000000..00878112f4c
--- /dev/null
+++ b/regression/contracts/assigns_enforce_07/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails when functions with assigns clauses are called within a loop and one of them does not obey its assigns clause.
diff --git a/regression/contracts/assigns_enforce_08/main.c b/regression/contracts/assigns_enforce_08/main.c
new file mode 100644
index 00000000000..8f562a91cee
--- /dev/null
+++ b/regression/contracts/assigns_enforce_08/main.c
@@ -0,0 +1,17 @@
+void f1(int *x) __CPROVER_assigns(*x)
+{
+  int *a = x;
+  f2(&a);
+}
+void f2(int **y) __CPROVER_assigns(**y)
+{
+  **y = 5;
+}
+
+int main()
+{
+  int n = 3;
+  f1(&n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_08/test.desc b/regression/contracts/assigns_enforce_08/test.desc
new file mode 100644
index 00000000000..f2b63278a84
--- /dev/null
+++ b/regression/contracts/assigns_enforce_08/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds when a function with an assigns
+clause calls another with an additional level of indirection, and that
+functions respects the assigns clause of the caller.
diff --git a/regression/contracts/assigns_enforce_09/main.c b/regression/contracts/assigns_enforce_09/main.c
new file mode 100644
index 00000000000..f0ddf187eca
--- /dev/null
+++ b/regression/contracts/assigns_enforce_09/main.c
@@ -0,0 +1,17 @@
+void f1(int **x) __CPROVER_assigns(*x)
+{
+  f2(x);
+}
+void f2(int **y) __CPROVER_assigns(**y)
+{
+  **y = 5;
+}
+
+int main()
+{
+  int p = 3;
+  int *q = &p;
+  f1(&q);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_09/test.desc b/regression/contracts/assigns_enforce_09/test.desc
new file mode 100644
index 00000000000..da304d4adc9
--- /dev/null
+++ b/regression/contracts/assigns_enforce_09/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails when a function with an assigns clause calls another with an assigns clause that adds one too many dereferences.
diff --git a/regression/contracts/assigns_enforce_10/main.c b/regression/contracts/assigns_enforce_10/main.c
new file mode 100644
index 00000000000..232d68a4ea7
--- /dev/null
+++ b/regression/contracts/assigns_enforce_10/main.c
@@ -0,0 +1,20 @@
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*y2, *z2)
+{
+  *y2 = 5;
+  *z2 = 5;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+  f1(&p, &q, &r);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_10/test.desc b/regression/contracts/assigns_enforce_10/test.desc
new file mode 100644
index 00000000000..4dab3e42137
--- /dev/null
+++ b/regression/contracts/assigns_enforce_10/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails when a function with an assigns clause calls another function with an assigns clause that is incompatible with the caller's assigns clause.
diff --git a/regression/contracts/assigns_enforce_11/main.c b/regression/contracts/assigns_enforce_11/main.c
new file mode 100644
index 00000000000..ac7a36c56d0
--- /dev/null
+++ b/regression/contracts/assigns_enforce_11/main.c
@@ -0,0 +1,20 @@
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2)
+{
+  *y2 = 5;
+  *z2 = 5;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+  f1(&p, &q, &r);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_11/test.desc b/regression/contracts/assigns_enforce_11/test.desc
new file mode 100644
index 00000000000..9129b3828e5
--- /dev/null
+++ b/regression/contracts/assigns_enforce_11/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails when a function with an assigns clause calls another function with a compatible assigns clause, but the callee does not abide by the shared assigns clause.
diff --git a/regression/contracts/assigns_enforce_12/main.c b/regression/contracts/assigns_enforce_12/main.c
new file mode 100644
index 00000000000..0af9f968420
--- /dev/null
+++ b/regression/contracts/assigns_enforce_12/main.c
@@ -0,0 +1,13 @@
+void f1(int *x) __CPROVER_assigns(*x)
+{
+  int *a = x;
+  *a = 5;
+}
+
+int main()
+{
+  int n = 3;
+  f1(&n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_12/test.desc b/regression/contracts/assigns_enforce_12/test.desc
new file mode 100644
index 00000000000..a24b653bc85
--- /dev/null
+++ b/regression/contracts/assigns_enforce_12/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification still succeeds if an expression in the assigns clause is written via an aliasing variable.
diff --git a/regression/contracts/assigns_enforce_13/main.c b/regression/contracts/assigns_enforce_13/main.c
new file mode 100644
index 00000000000..65e7795a3b7
--- /dev/null
+++ b/regression/contracts/assigns_enforce_13/main.c
@@ -0,0 +1,14 @@
+void f1(int *x, int *y) __CPROVER_assigns(*y)
+{
+  int *a = x;
+  *a = 5;
+}
+
+int main()
+{
+  int m = 3;
+  int n = 3;
+  f1(&n, &m);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_13/test.desc b/regression/contracts/assigns_enforce_13/test.desc
new file mode 100644
index 00000000000..32fb21ce7c1
--- /dev/null
+++ b/regression/contracts/assigns_enforce_13/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails if an expression outside of the assigns clause is written via an aliasing local variable.
diff --git a/regression/contracts/assigns_enforce_14/main.c b/regression/contracts/assigns_enforce_14/main.c
new file mode 100644
index 00000000000..9d205896302
--- /dev/null
+++ b/regression/contracts/assigns_enforce_14/main.c
@@ -0,0 +1,19 @@
+int z;
+
+// z is not assigned, but it *may* be assigned.
+// The assigns clause does not need to exactly match the
+// set of variables which are assigned in the function.
+int foo(int *x) __CPROVER_assigns(z, *x)
+  __CPROVER_ensures(__CPROVER_return_value == *x + 5)
+{
+  *x = *x + 0;
+  return *x + 5;
+}
+
+int main()
+{
+  int n = 4;
+  n = foo(&n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_14/test.desc b/regression/contracts/assigns_enforce_14/test.desc
new file mode 100644
index 00000000000..7c24b33faf7
--- /dev/null
+++ b/regression/contracts/assigns_enforce_14/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds if only expressions inside the assigns clause are assigned within the function.
+
+Note: For all 'enforce' tests, nothing can be assumed about the return value of the function (as the function call is not replaced at this point).
+
+To make such assumptions would cause verification to fail.
diff --git a/regression/contracts/assigns_enforce_malloc_01/main.c b/regression/contracts/assigns_enforce_malloc_01/main.c
new file mode 100644
index 00000000000..f3b91ea8147
--- /dev/null
+++ b/regression/contracts/assigns_enforce_malloc_01/main.c
@@ -0,0 +1,16 @@
+#include <stdlib.h>
+
+int f1(int *a, int *b) __CPROVER_assigns(*a)
+{
+  b = (int *)malloc(sizeof(int));
+  *b = 5;
+}
+
+int main()
+{
+  int m = 4;
+  int n = 3;
+  f1(&m, &n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_malloc_01/test.desc b/regression/contracts/assigns_enforce_malloc_01/test.desc
new file mode 100644
index 00000000000..72c6afae2e1
--- /dev/null
+++ b/regression/contracts/assigns_enforce_malloc_01/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds when a formal parameter pointer outside of the assigns clause is instead pointed as freshly allocated memory before being assigned.
diff --git a/regression/contracts/assigns_enforce_malloc_02/main.c b/regression/contracts/assigns_enforce_malloc_02/main.c
new file mode 100644
index 00000000000..e634c9cb058
--- /dev/null
+++ b/regression/contracts/assigns_enforce_malloc_02/main.c
@@ -0,0 +1,19 @@
+#include <stdlib.h>
+
+int f1(int *a, int *b) __CPROVER_assigns(*a)
+{
+  while(*a > 0)
+  {
+    int *b = (int *)malloc(sizeof(int));
+    *b = 5;
+  }
+}
+
+int main()
+{
+  int m = 4;
+  int n = 3;
+  f1(&m, &n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_malloc_02/test.desc b/regression/contracts/assigns_enforce_malloc_02/test.desc
new file mode 100644
index 00000000000..6acfd6a0854
--- /dev/null
+++ b/regression/contracts/assigns_enforce_malloc_02/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=6$
+^SIGNAL=0$
+Unable to complete instrumentation, as this malloc may be in a loop.$
+--
+--
+This test checks that an error is thrown when malloc is called within a loop.
diff --git a/regression/contracts/assigns_enforce_scoping_01/main.c b/regression/contracts/assigns_enforce_scoping_01/main.c
new file mode 100644
index 00000000000..e5ae6e48376
--- /dev/null
+++ b/regression/contracts/assigns_enforce_scoping_01/main.c
@@ -0,0 +1,18 @@
+int f1(int *a, int *b) __CPROVER_assigns(*a)
+{
+  if(*a > 0)
+  {
+    int *b = a;
+    *b = 5;
+  }
+  *b = 5;
+}
+
+int main()
+{
+  int m = 4;
+  int n = 3;
+  f1(&m, &n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_scoping_01/test.desc b/regression/contracts/assigns_enforce_scoping_01/test.desc
new file mode 100644
index 00000000000..ac134e83d35
--- /dev/null
+++ b/regression/contracts/assigns_enforce_scoping_01/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+assertion: SUCCESS$
+assertion: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test checks that variables which mask a formal parameter are logically distinct from the formal parameter itself. Specifically, we check that the masked variable may alias a parameter in the assigns clause, while the formal parameter does not, so verification fails, but not because of the masking variable.
diff --git a/regression/contracts/assigns_enforce_scoping_02/main.c b/regression/contracts/assigns_enforce_scoping_02/main.c
new file mode 100644
index 00000000000..89e176e1e76
--- /dev/null
+++ b/regression/contracts/assigns_enforce_scoping_02/main.c
@@ -0,0 +1,20 @@
+#include <stdlib.h>
+
+int f1(int *a, int *b) __CPROVER_assigns(*a)
+{
+  if(*a > 0)
+  {
+    int *b = (int *)malloc(sizeof(int));
+    *b = 5;
+  }
+  *b = 5;
+}
+
+int main()
+{
+  int m = 4;
+  int n = 3;
+  f1(&m, &n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_scoping_02/test.desc b/regression/contracts/assigns_enforce_scoping_02/test.desc
new file mode 100644
index 00000000000..d746bd0f0da
--- /dev/null
+++ b/regression/contracts/assigns_enforce_scoping_02/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+assertion: SUCCESS$
+assertion: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test checks that variables which mask a formal parameter are logically distinct from the formal parameter itself. In this test, we check that the masked variable may point to freshly-allocated memory, while the masked parameter may not be assigned, so verification fails, but not because of the masking variable.
diff --git a/regression/contracts/assigns_replace_01/main.c b/regression/contracts/assigns_replace_01/main.c
new file mode 100644
index 00000000000..d3f93979d10
--- /dev/null
+++ b/regression/contracts/assigns_replace_01/main.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+
+void foo(int *x) __CPROVER_assigns(*x)
+{
+  *x = 7;
+}
+
+int main()
+{
+  int n = 6;
+  foo(&n);
+  assert(n == 7);
+  assert(n == 6);
+  return 0;
+}
diff --git a/regression/contracts/assigns_replace_01/test.desc b/regression/contracts/assigns_replace_01/test.desc
new file mode 100644
index 00000000000..6ca65891f80
--- /dev/null
+++ b/regression/contracts/assigns_replace_01/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+assertion n == 7: FAILURE
+assertion n == 6: FAILURE
+^VERIFICATION FAILED$
+--
+--
+This test checks that a variable inside the assigns clause is havocked.
diff --git a/regression/contracts/assigns_replace_02/main.c b/regression/contracts/assigns_replace_02/main.c
new file mode 100644
index 00000000000..8487c6564c9
--- /dev/null
+++ b/regression/contracts/assigns_replace_02/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+void foo(int *x, int *y) __CPROVER_assigns(*x)
+{
+  *x = 7;
+}
+
+int main()
+{
+  int n;
+  int m = 4;
+  bar(&n);
+  assert(m == 4);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_replace_02/test.desc b/regression/contracts/assigns_replace_02/test.desc
new file mode 100644
index 00000000000..8c1d2534916
--- /dev/null
+++ b/regression/contracts/assigns_replace_02/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that a variable outside the assigns clause is not havocked.
diff --git a/regression/contracts/assigns_replace_03/main.c b/regression/contracts/assigns_replace_03/main.c
new file mode 100644
index 00000000000..e96665bee44
--- /dev/null
+++ b/regression/contracts/assigns_replace_03/main.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int y;
+double z;
+
+void bar(char **c) __CPROVER_assigns(y, z, **c) __CPROVER_ensures(**c == 6)
+{
+}
+
+int main()
+{
+  char **b;
+  bar(b);
+  assert(**b == 6);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_replace_03/test.desc b/regression/contracts/assigns_replace_03/test.desc
new file mode 100644
index 00000000000..93cd2e13787
--- /dev/null
+++ b/regression/contracts/assigns_replace_03/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that a havocked variable can be constrained by a function post-condition.
diff --git a/regression/contracts/assigns_replace_04/main.c b/regression/contracts/assigns_replace_04/main.c
new file mode 100644
index 00000000000..6ec35cf8d29
--- /dev/null
+++ b/regression/contracts/assigns_replace_04/main.c
@@ -0,0 +1,33 @@
+#include <assert.h>
+
+void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5)
+{
+  *x2 = 10;
+}
+
+void f3(int *x3, int *y3) __CPROVER_assigns(*x3) __CPROVER_ensures(*x3 > 100)
+{
+  *x3 = 101;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+
+  for(int i = 0; i < 5; ++i)
+  {
+    if(p < 3)
+    {
+      f2(&p, &q);
+    }
+    else
+    {
+      f3(&p, &q);
+    }
+  }
+  assert(p > 100);
+  assert(q == 2);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_replace_04/test.desc b/regression/contracts/assigns_replace_04/test.desc
new file mode 100644
index 00000000000..01b0f878661
--- /dev/null
+++ b/regression/contracts/assigns_replace_04/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds when an assigns clause is combined with a function contract in a loop properly.
diff --git a/regression/contracts/assigns_replace_05/main.c b/regression/contracts/assigns_replace_05/main.c
new file mode 100644
index 00000000000..42d98843653
--- /dev/null
+++ b/regression/contracts/assigns_replace_05/main.c
@@ -0,0 +1,33 @@
+#include <assert.h>
+
+void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5)
+{
+  *x2 = 10;
+}
+
+void f3(int *x3, int *y3) __CPROVER_ensures(*x3 > 100)
+{
+  *x3 = 101;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+
+  for(int i = 0; i < 5; ++i)
+  {
+    if(i < 3)
+    {
+      f2(&p, &q);
+    }
+    else
+    {
+      f3(&p, &q);
+    }
+  }
+  assert(p > 100);
+  assert(q == 2);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_replace_05/test.desc b/regression/contracts/assigns_replace_05/test.desc
new file mode 100644
index 00000000000..5e2bdc834ac
--- /dev/null
+++ b/regression/contracts/assigns_replace_05/test.desc
@@ -0,0 +1,12 @@
+KNOWNBUG
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails when assigns clauses are combined with function contracts
+in a loop improperly, i.e., always assumes memory not mention in ensures clauses are unchanged.
+
+BUG: Currently, function call replacement using 'ensures' specifications encodes an implicit assumption that any memory not mentioned in the ensures clause remains unchanged throughout the function, even when an 'assigns' clause is not present.
diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc
index 7dafb10d751..947fd5207b4 100644
--- a/regression/contracts/function_check_01/test.desc
+++ b/regression/contracts/function_check_01/test.desc
@@ -1,11 +1,9 @@
-KNOWNBUG
+CORE
 main.c
---apply-code-contracts
+--replace-all-calls-with-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.
+This tests a simple example of a function with requires and ensures which should both be satisfied.
diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h
index e98b3ef27f2..d1b2d3c2ce1 100644
--- a/src/ansi-c/ansi_c_declaration.h
+++ b/src/ansi-c/ansi_c_declaration.h
@@ -244,6 +244,21 @@ class ansi_c_declarationt:public exprt
     assert(!declarators().empty());
     declarators().back().value().swap(value);
   }
+
+  const exprt &spec_assigns() const
+  {
+    return static_cast<const exprt &>(find(ID_C_spec_assigns));
+  }
+
+  const exprt &spec_requires() const
+  {
+    return static_cast<const exprt &>(find(ID_C_spec_requires));
+  }
+
+  const exprt &spec_ensures() const
+  {
+    return static_cast<const exprt &>(find(ID_C_spec_ensures));
+  }
 };
 
 inline ansi_c_declarationt &to_ansi_c_declaration(exprt &expr)
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 4979fab69fc..5c0d114b1ed 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -17,9 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/prefix.h>
 #include <util/std_types.h>
 
+#include "c_storage_spec.h"
 #include "expr2c.h"
 #include "type2name.h"
-#include "c_storage_spec.h"
 
 std::string c_typecheck_baset::to_string(const exprt &expr)
 {
@@ -645,13 +645,14 @@ void c_typecheck_baset::typecheck_declaration(
     irept contract;
 
     {
-      exprt spec_requires=
-        static_cast<const exprt&>(declaration.find(ID_C_spec_requires));
-      contract.add(ID_C_spec_requires).swap(spec_requires);
+      exprt spec_assigns = declaration.spec_assigns();
+      contract.add(ID_C_spec_assigns).swap(spec_assigns);
 
-      exprt spec_ensures=
-        static_cast<const exprt&>(declaration.find(ID_C_spec_ensures));
+      exprt spec_ensures = declaration.spec_ensures();
       contract.add(ID_C_spec_ensures).swap(spec_ensures);
+
+      exprt spec_requires = declaration.spec_requires();
+      contract.add(ID_C_spec_requires).swap(spec_requires);
     }
 
     // Now do declarators, if any.
@@ -725,6 +726,12 @@ void c_typecheck_baset::typecheck_declaration(
       irep_idt identifier=symbol.name;
       declarator.set_name(identifier);
 
+      // If the declarator is for a function definition, typecheck it.
+      if(can_cast_type<code_typet>(declarator.type()))
+      {
+        typecheck_assigns(to_code_type(declarator.type()), contract);
+      }
+
       typecheck_symbol(symbol);
 
       // add code contract (if any); we typecheck this after the
@@ -732,6 +739,8 @@ void c_typecheck_baset::typecheck_declaration(
       // available
       symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
 
+      typecheck_assigns_exprs(
+        static_cast<codet &>(contract), ID_C_spec_assigns);
       typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_requires);
 
       typet ret_type = void_type();
@@ -743,12 +752,15 @@ void c_typecheck_baset::typecheck_declaration(
       typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_ensures);
       parameter_map.clear();
 
-      if(contract.find(ID_C_spec_requires).is_not_nil())
-        new_symbol.type.add(ID_C_spec_requires)=
-          contract.find(ID_C_spec_requires);
-      if(contract.find(ID_C_spec_ensures).is_not_nil())
-        new_symbol.type.add(ID_C_spec_ensures)=
-          contract.find(ID_C_spec_ensures);
+      irept assigns_to_add = contract.find(ID_C_spec_assigns);
+      if(assigns_to_add.is_not_nil())
+        new_symbol.type.add(ID_C_spec_assigns) = assigns_to_add;
+      irept requires_to_add = contract.find(ID_C_spec_requires);
+      if(requires_to_add.is_not_nil())
+        new_symbol.type.add(ID_C_spec_requires) = requires_to_add;
+      irept ensures_to_add = contract.find(ID_C_spec_ensures);
+      if(ensures_to_add.is_not_nil())
+        new_symbol.type.add(ID_C_spec_ensures) = ensures_to_add;
     }
   }
 }
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index 01981f9d99c..650eac010da 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -144,6 +144,11 @@ class c_typecheck_baset:
   virtual void typecheck_dowhile(code_dowhilet &code);
   virtual void typecheck_start_thread(codet &code);
   virtual void typecheck_spec_expr(codet &code, const irep_idt &spec);
+  virtual void
+  typecheck_assigns(const code_typet &function_declarator, const irept &spec);
+  virtual void
+  typecheck_assigns(const ansi_c_declaratort &declarator, const exprt &assigns);
+  virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec);
 
   bool break_is_allowed;
   bool continue_is_allowed;
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 041b9b3bf4f..480d80b0bb2 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -794,16 +794,75 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
   typecheck_spec_expr(code, ID_C_spec_loop_invariant);
 }
 
-void c_typecheck_baset::typecheck_spec_expr(
+void c_typecheck_baset::typecheck_spec_expr(codet &code, const irep_idt &spec)
+{
+  if(code.find(spec).is_not_nil())
+  {
+    exprt &constraint = static_cast<exprt &>(code.add(spec));
+
+    typecheck_expr(constraint);
+    implicit_typecast_bool(constraint);
+  }
+}
+
+void c_typecheck_baset::typecheck_assigns(
+  const code_typet &function_declarator,
+  const irept &contract)
+{
+  exprt assigns = static_cast<const exprt &>(contract.find(ID_C_spec_assigns));
+
+  // Make sure there is an assigns clause to check
+  if(assigns.is_not_nil())
+  {
+    for(const auto &curr_param : function_declarator.parameters())
+    {
+      if(curr_param.id() == ID_declaration)
+      {
+        const ansi_c_declarationt &param_declaration =
+          to_ansi_c_declaration(curr_param);
+
+        for(const auto &decl : param_declaration.declarators())
+        {
+          typecheck_assigns(decl, assigns);
+        }
+      }
+    }
+  }
+}
+
+void c_typecheck_baset::typecheck_assigns(
+  const ansi_c_declaratort &declarator,
+  const exprt &assigns)
+{
+  for(exprt curr_op : assigns.operands())
+  {
+    if(curr_op.id() != ID_symbol)
+    {
+      continue;
+    }
+    const symbol_exprt &symbol_op = to_symbol_expr(curr_op);
+
+    if(symbol_op.get(ID_C_base_name) == declarator.get_base_name())
+    {
+      error().source_location = declarator.source_location();
+      error() << "Formal parameter " << declarator.get_name() << " without "
+              << "dereference appears in ASSIGNS clause. Assigning this "
+              << "parameter will never affect the state of the calling context."
+              << " Did you mean to write *" << declarator.get_name() << "?"
+              << eom;
+      throw 0;
+    }
+  }
+}
+
+void c_typecheck_baset::typecheck_assigns_exprs(
   codet &code,
   const irep_idt &spec)
 {
   if(code.find(spec).is_not_nil())
   {
-    exprt &constraint=
-      static_cast<exprt&>(code.add(spec));
+    exprt &constraint = static_cast<exprt &>(code.add(spec));
 
     typecheck_expr(constraint);
-    implicit_typecast_bool(constraint);
   }
 }
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 6a455ccdd38..802a6daa23f 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -470,6 +470,10 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
   {
     // already type checked
   }
+  else if(expr.id() == ID_C_spec_assigns || expr.id() == ID_target_list)
+  {
+    // already type checked
+  }
   else
   {
     error().source_location = expr.source_location();
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index b4455369e0c..8bd13ee94f3 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -204,6 +204,7 @@ extern char *yyansi_ctext;
 %token TOK_CPROVER_LOOP_INVARIANT  "__CPROVER_loop_invariant"
 %token TOK_CPROVER_REQUIRES  "__CPROVER_requires"
 %token TOK_CPROVER_ENSURES  "__CPROVER_ensures"
+%token TOK_CPROVER_ASSIGNS "__CPROVER_assigns"
 %token TOK_IMPLIES     "==>"
 %token TOK_EQUIVALENT  "<==>"
 %token TOK_XORXOR      "^^"
@@ -510,6 +511,36 @@ ensures_opt:
         { $$=$3; }
         ;
 
+assigns_opt:
+        /* nothing */
+        { init($$); parser_stack($$).make_nil(); }
+        | TOK_CPROVER_ASSIGNS '(' target_list ')'
+        { $$=$3; }
+        ;
+
+target_list:
+          target
+        {
+          init($$, ID_target_list);
+          mto($$, $1);
+        }
+        | target_list ',' target
+        {
+          $$=$1;
+          mto($$, $3);
+        }
+        ;
+
+target:
+          identifier
+        | '*' target
+        {
+          $$=$1;
+          set($$, ID_dereference);
+          mto($$, $2);
+        }
+        ;
+
 statement_expression: '(' compound_statement ')'
         { 
           $$=$1;
@@ -2853,14 +2884,21 @@ asm_definition:
 
 function_definition:
           function_head
+          assigns_opt
           requires_opt
           ensures_opt
           function_body
         {
+
+          // Capture assigns clause
           if(parser_stack($2).is_not_nil())
-            parser_stack($1).add(ID_C_spec_requires).swap(parser_stack($2));
+            parser_stack($1).add(ID_C_spec_assigns).swap(parser_stack($2));
+
+          // Capture code contract
           if(parser_stack($3).is_not_nil())
-            parser_stack($1).add(ID_C_spec_ensures).swap(parser_stack($3));
+            parser_stack($1).add(ID_C_spec_requires).swap(parser_stack($3));
+          if(parser_stack($4).is_not_nil())
+            parser_stack($1).add(ID_C_spec_ensures).swap(parser_stack($4));
           // The head is a declaration with one declarator,
           // and the body becomes the 'value'.
           $$=$1;
@@ -2868,7 +2906,7 @@ function_definition:
             to_ansi_c_declaration(parser_stack($$));
             
           assert(ansi_c_declaration.declarators().size()==1);
-          ansi_c_declaration.add_initializer(parser_stack($4));
+          ansi_c_declaration.add_initializer(parser_stack($5));
           
           // Kill the scope that 'function_head' creates.
           PARSER.pop_scope();
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index d3eeceaf08c..2b45492e515 100644
--- a/src/ansi-c/scanner.l
+++ b/src/ansi-c/scanner.l
@@ -1277,6 +1277,7 @@ __decltype          { if(PARSER.cpp98 &&
 {CPROVER_PREFIX}"loop_invariant" { loc(); return TOK_CPROVER_LOOP_INVARIANT; }
 {CPROVER_PREFIX}"requires"     { loc(); return TOK_CPROVER_REQUIRES; }
 {CPROVER_PREFIX}"ensures"      { loc(); return TOK_CPROVER_ENSURES; }
+{CPROVER_PREFIX}"assigns"      { loc(); return TOK_CPROVER_ASSIGNS; }
 
 "\xe2\x88\x80" |
 "\\forall"      { /* Non-standard, obviously. Found in ACSL syntax. */
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
index e0115fb34fa..23a369a2391 100644
--- a/src/goto-instrument/code_contracts.cpp
+++ b/src/goto-instrument/code_contracts.cpp
@@ -11,20 +11,23 @@ Date: February 2016
 /// \file
 /// Verify and use annotated invariants and pre/post-conditions
 
-#include "code_contracts.h"
+#include <algorithm>
+#include <unordered_set>
 
-#include <util/expr_util.h>
-#include <util/fresh_symbol.h>
-#include <util/replace_symbol.h>
+#include <analyses/local_may_alias.h>
 
 #include <goto-programs/remove_skip.h>
 
-#include <analyses/local_may_alias.h>
-
 #include <linking/static_lifetime_init.h>
 
+#include <util/c_types.h>
+#include <util/expr_util.h>
+#include <util/fresh_symbol.h>
 #include <util/message.h>
+#include <util/pointer_predicates.h>
+#include <util/replace_symbol.h>
 
+#include "code_contracts.h"
 #include "loop_utils.h"
 
 /// Predicate to be used with the exprt::visit() function. The function
@@ -62,7 +65,7 @@ static void check_apply_invariants(
   const goto_programt::targett loop_head,
   const loopt &loop)
 {
-  assert(!loop.empty());
+  PRECONDITION(!loop.empty());
 
   // find the last back edge
   goto_programt::targett loop_end=loop_head;
@@ -145,11 +148,13 @@ static void check_apply_invariants(
 
 bool code_contractst::has_contract(const irep_idt fun_name)
 {
-  const symbolt &f_sym = ns.lookup(fun_name);
-  const code_typet &type = to_code_type(f_sym.type);
-  const exprt ensures =
-    static_cast<const exprt &>(type.find(ID_C_spec_ensures));
-  return ensures.is_not_nil();
+  const symbolt &function_symbol = ns.lookup(fun_name);
+  const code_typet &type = to_code_type(function_symbol.type);
+  if(type.find(ID_C_spec_assigns).is_not_nil())
+    return true;
+
+  return type.find(ID_C_spec_requires).is_not_nil() ||
+         type.find(ID_C_spec_ensures).is_not_nil();
 }
 
 bool code_contractst::apply_contract(
@@ -158,39 +163,47 @@ bool code_contractst::apply_contract(
 {
   const code_function_callt &call = target->get_function_call();
 
-  // we don't handle function pointers
-  if(call.function().id()!=ID_symbol)
+  // Return if the function is not named in the call; currently we don't handle
+  // function pointers.
+  // TODO: handle function pointers.
+  if(call.function().id() != ID_symbol)
     return false;
 
-  const irep_idt &function=
-    to_symbol_expr(call.function()).get_identifier();
-  const symbolt &f_sym=ns.lookup(function);
-  const code_typet &type=to_code_type(f_sym.type);
+  // Retrieve the function type, which is needed to extract the contract
+  // components.
+  const irep_idt &function = to_symbol_expr(call.function()).get_identifier();
+  const symbolt &function_symbol = ns.lookup(function);
+  const code_typet &type = to_code_type(function_symbol.type);
 
-  exprt requires=
-    static_cast<const exprt&>(type.find(ID_C_spec_requires));
-  exprt ensures=
-    static_cast<const exprt&>(type.find(ID_C_spec_ensures));
+  // Isolate each component of the contract.
+  exprt assigns = static_cast<const exprt &>(type.find(ID_C_spec_assigns));
+  exprt requires = static_cast<const exprt &>(type.find(ID_C_spec_requires));
+  exprt ensures = static_cast<const exprt &>(type.find(ID_C_spec_ensures));
 
-  // is there a contract?
-  if(ensures.is_nil())
+  // Check to see if the function  contract actually constrains its effect on
+  // the program state; if not, return.
+  if(ensures.is_nil() && assigns.is_nil())
     return false;
 
+  // Create a replace_symbolt object, for replacing expressions in the callee
+  // with expressions from the call site (e.g. the return value).
   replace_symbolt replace;
-  // Replace return value
   if(type.return_type() != empty_typet())
   {
+    // Check whether the function's return value is not disregarded.
     if(call.lhs().is_not_nil())
     {
-      // foo() ensures that its return value is > 5. Then rewrite calls to foo:
+      // If so, have it replaced appropriately.
+      // For example, if foo() ensures that its return value is > 5, then
+      // rewrite calls to foo as follows:
       // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
       symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
       replace.insert(ret_val, call.lhs());
     }
     else
     {
-      // Function does have a return value, but call is not being assigned to
-      // anything so we can't use the trick above.
+      // If the function does return a value, but the return value is
+      // disregarded, check if the postcondition includes the return value.
       return_value_visitort v;
       ensures.visit(v);
       if(v.found_return_value())
@@ -214,20 +227,23 @@ bool code_contractst::apply_contract(
   // Replace formal parameters
   code_function_callt::argumentst::const_iterator a_it=
     call.arguments().begin();
-  for(code_typet::parameterst::const_iterator
-      p_it=type.parameters().begin();
-      p_it!=type.parameters().end() &&
-      a_it!=call.arguments().end();
+  for(code_typet::parameterst::const_iterator p_it = type.parameters().begin();
+      p_it != type.parameters().end() && a_it != call.arguments().end();
       ++p_it, ++a_it)
+  {
     if(!p_it->get_identifier().empty())
     {
       symbol_exprt p(p_it->get_identifier(), p_it->type());
       replace.insert(p, *a_it);
     }
+  }
 
+  // Replace expressions in the contract components.
+  replace(assigns);
   replace(requires);
   replace(ensures);
 
+  // Insert assertion of the precondition immediately before the call site.
   if(requires.is_not_nil())
   {
     goto_programt::instructiont a =
@@ -237,9 +253,47 @@ bool code_contractst::apply_contract(
     ++target;
   }
 
-  // overwrite the function call
-  *target = goto_programt::make_assumption(ensures, target->source_location);
+  // Create a series of non-deterministic assignments to havoc the variables
+  // in the assigns clause.
+  if(assigns.is_not_nil())
+  {
+    goto_programt assigns_havoc;
+    modifiest assigns_tgts;
+    const exprt::operandst &targets = assigns.operands();
+    for(const exprt &curr_op : targets)
+    {
+      if(curr_op.id() == ID_symbol || curr_op.id() == ID_dereference)
+      {
+        assigns_tgts.insert(curr_op);
+      }
+      else
+      {
+        log.error() << "Unable to apply assigns clause for expression of type '"
+                    << curr_op.id() << "'; not enforcing assigns clause."
+                    << messaget::eom;
+        return true;
+      }
+    }
+    build_havoc_code(target, assigns_tgts, assigns_havoc);
+
+    // Insert the non-deterministic assignment immediately before the call site.
+    goto_program.insert_before_swap(target, assigns_havoc);
+    std::advance(target, assigns_tgts.size());
+  }
 
+  // To remove the function call, replace it with an assumption statement
+  // assuming the postcondition, if there is one. Otherwise, replace the
+  // function call with a SKIP statement.
+  if(ensures.is_not_nil())
+  {
+    *target = goto_programt::make_assumption(ensures, target->source_location);
+  }
+  else
+  {
+    *target = goto_programt::make_skip();
+  }
+
+  // Add this function to the set of replaced functions.
   summarized.insert(function);
   return false;
 }
@@ -251,15 +305,12 @@ void code_contractst::code_contracts(
   natural_loops_mutablet natural_loops(goto_function.body);
 
   // iterate over the (natural) loops in the function
-  for(natural_loops_mutablet::loop_mapt::const_iterator
-      l_it=natural_loops.loop_map.begin();
-      l_it!=natural_loops.loop_map.end();
+  for(natural_loops_mutablet::loop_mapt::const_iterator l_it =
+        natural_loops.loop_map.begin();
+      l_it != natural_loops.loop_map.end();
       l_it++)
     check_apply_invariants(
-      goto_function,
-      local_may_alias,
-      l_it->first,
-      l_it->second);
+      goto_function, local_may_alias, l_it->first, l_it->second);
 
   // look at all function calls
   Forall_goto_program_instructions(ins, goto_function.body)
@@ -282,24 +333,388 @@ const symbolt &code_contractst::new_tmp_symbol(
     symbol_table);
 }
 
+static exprt create_alias_expression(
+  const exprt &assigns,
+  const exprt &lhs,
+  std::vector<exprt> &aliasable_references)
+{
+  bool first_iter = true;
+  exprt running = false_exprt();
+  for(auto aliasable : aliasable_references)
+  {
+    exprt left_ptr = address_of_exprt{lhs};
+    exprt right_ptr = aliasable;
+    exprt same = same_object(left_ptr, right_ptr);
+
+    if(first_iter)
+    {
+      running = same;
+      first_iter = false;
+    }
+    else
+    {
+      exprt::operandst disjuncts;
+      disjuncts.push_back(same);
+      disjuncts.push_back(running);
+      running = disjunction(disjuncts);
+    }
+  }
+
+  return running;
+}
+
+void code_contractst::populate_assigns_references(
+  const symbolt &function_symbol,
+  const irep_idt &function_id,
+  goto_programt &created_decls,
+  std::vector<exprt> &created_references)
+{
+  const code_typet &type = to_code_type(function_symbol.type);
+  const exprt &assigns =
+    static_cast<const exprt &>(type.find(ID_C_spec_assigns));
+
+  const exprt::operandst &targets = assigns.operands();
+  for(const exprt &curr_op : targets)
+  {
+    // Declare a new symbol to stand in for the reference
+    symbol_exprt standin = new_tmp_symbol(
+                             pointer_type(curr_op.type()),
+                             function_symbol.location,
+                             function_id,
+                             function_symbol.mode)
+                             .symbol_expr();
+
+    created_decls.add(
+      goto_programt::make_decl(standin, function_symbol.location));
+
+    created_decls.add(goto_programt::make_assignment(
+      code_assignt(standin, std::move(address_of_exprt{curr_op})),
+      function_symbol.location));
+
+    // Add a map entry from the original operand to the new symbol
+    created_references.push_back(standin);
+  }
+}
+
+void code_contractst::instrument_assigns_statement(
+  goto_programt::instructionst::iterator &instruction_iterator,
+  goto_programt &program,
+  exprt &assigns,
+  std::vector<exprt> &assigns_references,
+  std::set<exprt> &freely_assignable_exprs)
+{
+  INVARIANT(
+    instruction_iterator->is_assign(),
+    "The first argument of instrument_assigns_statement should always be"
+    " an assignment");
+  const exprt &lhs = instruction_iterator->get_assign().lhs();
+  if(freely_assignable_exprs.find(lhs) != freely_assignable_exprs.end())
+  {
+    return;
+  }
+  exprt alias_expr = create_alias_expression(assigns, lhs, assigns_references);
+
+  goto_programt alias_assertion;
+  alias_assertion.add(goto_programt::make_assertion(
+    alias_expr, instruction_iterator->source_location));
+  program.insert_before_swap(instruction_iterator, alias_assertion);
+  ++instruction_iterator;
+}
+
+void code_contractst::instrument_call_statement(
+  goto_programt::instructionst::iterator &instruction_iterator,
+  goto_programt &program,
+  exprt &assigns,
+  std::vector<exprt> &aliasable_references,
+  std::set<exprt> &freely_assignable_exprs)
+{
+  INVARIANT(
+    instruction_iterator->is_function_call(),
+    "The first argument of instrument_call_statement should always be "
+    "a function call");
+  code_function_callt call = instruction_iterator->get_function_call();
+  const irep_idt &called_name =
+    to_symbol_expr(call.function()).get_identifier();
+
+  // Malloc allocates memory which is not part of the caller's memory
+  // frame, so we want to capture the newly-allocated memory and
+  // treat it as assignable.
+  if(called_name == "malloc")
+  {
+    aliasable_references.push_back(call.lhs());
+
+    // Make the variable, where result of malloc is stored, freely assignable.
+    goto_programt::instructionst::iterator local_instruction_iterator =
+      instruction_iterator;
+    local_instruction_iterator++;
+    if(
+      local_instruction_iterator->is_assign() &&
+      local_instruction_iterator->get_assign().lhs().is_not_nil())
+    {
+      freely_assignable_exprs.insert(
+        local_instruction_iterator->get_assign().lhs());
+    }
+    return; // assume malloc edits no currently-existing memory objects.
+  }
+
+  if(call.lhs().is_not_nil())
+  {
+    exprt alias_expr =
+      create_alias_expression(assigns, call.lhs(), aliasable_references);
+
+    goto_programt alias_assertion;
+    alias_assertion.add(goto_programt::make_assertion(
+      alias_expr, instruction_iterator->source_location));
+    program.insert_before_swap(instruction_iterator, alias_assertion);
+    ++instruction_iterator;
+  }
+
+  // TODO we don't handle function pointers
+  if(call.function().id() == ID_symbol)
+  {
+    const symbolt &called_sym = ns.lookup(called_name);
+    const code_typet &called_type = to_code_type(called_sym.type);
+
+    auto called_func = goto_functions.function_map.find(called_name);
+    if(called_func == goto_functions.function_map.end())
+    {
+      log.error() << "Could not find function '" << called_name
+                  << "' in goto-program; not enforcing assigns clause."
+                  << messaget::eom;
+      return;
+    }
+
+    exprt called_assigns = static_cast<const exprt &>(
+      called_func->second.type.find(ID_C_spec_assigns));
+    if(called_assigns.is_nil()) // Called function has no assigns clause
+    {
+      // Fail if called function has no assigns clause.
+      log.error() << "No assigns specification found for function '"
+                  << called_name
+                  << "' in goto-program; not enforcing assigns clause."
+                  << messaget::eom;
+
+      // Create a false assertion, so the analysis will fail if this function
+      // is called.
+      goto_programt failing_assertion;
+      failing_assertion.add(goto_programt::make_assertion(
+        false_exprt(), instruction_iterator->source_location));
+      program.insert_before_swap(instruction_iterator, failing_assertion);
+      ++instruction_iterator;
+
+      return;
+    }
+    else // Called function has assigns clause
+    {
+      replace_symbolt replace;
+      // Replace formal parameters
+      code_function_callt::argumentst::const_iterator a_it =
+        call.arguments().begin();
+      for(code_typet::parameterst::const_iterator p_it =
+            called_type.parameters().begin();
+          p_it != called_type.parameters().end() &&
+          a_it != call.arguments().end();
+          ++p_it, ++a_it)
+      {
+        if(!p_it->get_identifier().empty())
+        {
+          symbol_exprt p(p_it->get_identifier(), p_it->type());
+          replace.insert(p, *a_it);
+        }
+      }
+
+      replace(called_assigns);
+      for(exprt::operandst::const_iterator called_op_it =
+            called_assigns.operands().begin();
+          called_op_it != called_assigns.operands().end();
+          called_op_it++)
+      {
+        if(
+          freely_assignable_exprs.find(*called_op_it) !=
+          freely_assignable_exprs.end())
+        {
+          continue;
+        }
+        exprt alias_expr =
+          create_alias_expression(assigns, *called_op_it, aliasable_references);
+
+        goto_programt alias_assertion;
+        alias_assertion.add(goto_programt::make_assertion(
+          alias_expr, instruction_iterator->source_location));
+        program.insert_before_swap(instruction_iterator, alias_assertion);
+        ++instruction_iterator;
+      }
+    }
+  }
+}
+
+bool code_contractst::check_for_looped_mallocs(const goto_programt &program)
+{
+  // Collect all GOTOs and mallocs
+  std::vector<goto_programt::instructiont> back_gotos;
+  std::vector<goto_programt::instructiont> malloc_calls;
+
+  int idx = 0;
+  for(goto_programt::instructiont instruction : program.instructions)
+  {
+    if(instruction.is_backwards_goto())
+    {
+      back_gotos.push_back(instruction);
+    }
+    if(instruction.is_function_call())
+    {
+      code_function_callt call = instruction.get_function_call();
+      const irep_idt &called_name =
+        to_symbol_expr(call.function()).get_identifier();
+
+      if(called_name == "malloc")
+      {
+        malloc_calls.push_back(instruction);
+      }
+    }
+    idx++;
+  }
+  // Make sure there are no gotos that go back such that a malloc is between
+  // the goto and its destination (possible loop).
+  for(auto goto_entry : back_gotos)
+  {
+    for(const auto &target : goto_entry.targets)
+    {
+      for(auto malloc_entry : malloc_calls)
+      {
+        if(
+          malloc_entry.location_number >= target->location_number &&
+          malloc_entry.location_number < goto_entry.location_number)
+        {
+          // In order to statically keep track of all the memory we should
+          //   be able to assign, we need to create ghost variables to store
+          //   references to that memory.
+          // If a malloc is in a loop, we can't generally determine how many
+          //   times it will run in order to create an appropriate number of
+          //   references for the assignable memory.
+          // So, if we have a malloc in a loop, we can't statically create the
+          //   assertion statements needed to enforce the assigns clause.
+          log.error() << "Call to malloc at location "
+                      << malloc_entry.location_number << " falls between goto "
+                      << "source location " << goto_entry.location_number
+                      << " and it's destination at location "
+                      << target->location_number << ". "
+                      << "Unable to complete instrumentation, as this malloc "
+                      << "may be in a loop." << messaget::eom;
+          throw 0;
+        }
+      }
+    }
+  }
+  return false;
+}
+
+bool code_contractst::add_pointer_checks(const std::string &function_name)
+{
+  // Get the function object before instrumentation.
+  auto old_function = goto_functions.function_map.find(function_name);
+  if(old_function == goto_functions.function_map.end())
+  {
+    log.error() << "Could not find function '" << function_name
+                << "' in goto-program; not enforcing contracts."
+                << messaget::eom;
+    return true;
+  }
+  goto_programt &program = old_function->second.body;
+  if(program.instructions.empty()) // empty function body
+  {
+    return false;
+  }
+
+  const irep_idt function_id(function_name);
+  const symbolt &function_symbol = ns.lookup(function_id);
+  const code_typet &type = to_code_type(function_symbol.type);
+
+  exprt assigns = static_cast<const exprt &>(type.find(ID_C_spec_assigns));
+
+  // Return if there are no reference checks to perform.
+  if(assigns.is_nil())
+    return false;
+
+  goto_programt::instructionst::iterator instruction_iterator =
+    program.instructions.begin();
+
+  // Create temporary variables to hold the assigns clause targets before
+  // they can be modified.
+  goto_programt standin_decls;
+  std::vector<exprt> original_references;
+  populate_assigns_references(
+    function_symbol, function_id, standin_decls, original_references);
+
+  // Create a list of variables that are okay to assign.
+  std::set<exprt> freely_assignable_exprs;
+  for(code_typet::parametert param : type.parameters())
+  {
+    freely_assignable_exprs.insert(param);
+  }
+
+  int lines_to_iterate = standin_decls.instructions.size();
+  program.insert_before_swap(instruction_iterator, standin_decls);
+  std::advance(instruction_iterator, lines_to_iterate);
+
+  if(check_for_looped_mallocs(program))
+  {
+    return true;
+  }
+
+  // Insert aliasing assertions
+  for(; instruction_iterator != program.instructions.end();
+      ++instruction_iterator)
+  {
+    if(instruction_iterator->is_decl())
+    {
+      freely_assignable_exprs.insert(instruction_iterator->get_decl().symbol());
+    }
+    else if(instruction_iterator->is_assign())
+    {
+      instrument_assigns_statement(
+        instruction_iterator,
+        program,
+        assigns,
+        original_references,
+        freely_assignable_exprs);
+    }
+    else if(instruction_iterator->is_function_call())
+    {
+      instrument_call_statement(
+        instruction_iterator,
+        program,
+        assigns,
+        original_references,
+        freely_assignable_exprs);
+    }
+  }
+  return false;
+}
+
 bool code_contractst::enforce_contract(const std::string &fun_to_enforce)
 {
-  // Rename old function
+  // Add statements to the source function to ensure assigns clause is
+  // respected.
+  add_pointer_checks(fun_to_enforce);
+
+  // Rename source function
   std::stringstream ss;
   ss << CPROVER_PREFIX << "contracts_original_" << fun_to_enforce;
   const irep_idt mangled(ss.str());
   const irep_idt original(fun_to_enforce);
 
-  auto old_fun = goto_functions.function_map.find(original);
-  if(old_fun == goto_functions.function_map.end())
+  auto old_function = goto_functions.function_map.find(original);
+  if(old_function == goto_functions.function_map.end())
   {
     log.error() << "Could not find function '" << fun_to_enforce
                 << "' in goto-program; not enforcing contracts."
                 << messaget::eom;
     return true;
   }
-  std::swap(goto_functions.function_map[mangled], old_fun->second);
-  goto_functions.function_map.erase(old_fun);
+
+  std::swap(goto_functions.function_map[mangled], old_function->second);
+  goto_functions.function_map.erase(old_function);
 
   // Place a new symbol with the mangled name into the symbol table
   source_locationt sl;
@@ -318,9 +733,9 @@ bool code_contractst::enforce_contract(const std::string &fun_to_enforce)
       " in the symbol table because that name is a mangled name");
 
   // Insert wrapper function into goto_functions
-  auto nexist_old_fun = goto_functions.function_map.find(original);
+  auto nexist_old_function = goto_functions.function_map.find(original);
   INVARIANT(
-    nexist_old_fun == goto_functions.function_map.end(),
+    nexist_old_function == goto_functions.function_map.end(),
     "There should be no function called " + fun_to_enforce +
       " in the function map because that function should have had its"
       " name mangled");
@@ -346,19 +761,24 @@ void code_contractst::add_contract_check(
   const irep_idt &mangled_fun,
   goto_programt &dest)
 {
-  assert(!dest.instructions.empty());
+  PRECONDITION(!dest.instructions.empty());
 
   goto_functionst::function_mapt::iterator f_it =
     goto_functions.function_map.find(mangled_fun);
-  assert(f_it!=goto_functions.function_map.end());
+  PRECONDITION(f_it != goto_functions.function_map.end());
 
-  const goto_functionst::goto_functiont &gf=f_it->second;
+  const goto_functionst::goto_functiont &gf = f_it->second;
 
-  const exprt &requires=
-    static_cast<const exprt&>(gf.type.find(ID_C_spec_requires));
-  const exprt &ensures=
-    static_cast<const exprt&>(gf.type.find(ID_C_spec_ensures));
-  assert(ensures.is_not_nil());
+  const exprt &assigns =
+    static_cast<const exprt &>(gf.type.find(ID_C_spec_assigns));
+  const exprt &requires =
+    static_cast<const exprt &>(gf.type.find(ID_C_spec_requires));
+  const exprt &ensures =
+    static_cast<const exprt &>(gf.type.find(ID_C_spec_ensures));
+  INVARIANT(
+    ensures.is_not_nil() || assigns.is_not_nil(),
+    "Code contract enforcement is trivial without an ensures or assigns "
+    "clause.");
 
   // build:
   // if(nondet)
@@ -367,7 +787,6 @@ void code_contractst::add_contract_check(
   //   assume(requires)  [optional]
   //   ret=function(parameter1, ...)
   //   assert(ensures)
-  //   assume(false)
   // skip: ...
 
   // build skip so that if(nondet) can refer to it
@@ -443,12 +862,11 @@ void code_contractst::add_contract_check(
   replace(ensures_cond);
 
   // assert(ensures)
-  check.add(
-    goto_programt::make_assertion(ensures_cond, ensures.source_location()));
-
-  // assume(false)
-  check.add(
-    goto_programt::make_assumption(false_exprt(), ensures.source_location()));
+  if(ensures.is_not_nil())
+  {
+    check.add(
+      goto_programt::make_assertion(ensures_cond, ensures.source_location()));
+  }
 
   // prepend the new code to dest
   check.destructive_append(tmp_skip);
diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h
index 9aa3554a0e2..0c696de4437 100644
--- a/src/goto-instrument/code_contracts.h
+++ b/src/goto-instrument/code_contracts.h
@@ -92,6 +92,47 @@ class code_contractst
   /// \brief Enforce contract of a single function
   bool enforce_contract(const std::string &);
 
+  /// Insert assertion statements into the goto program to ensure that
+  /// assigned memory is within the assignable memory frame.
+  bool add_pointer_checks(const std::string &);
+
+  /// Check if there are any malloc statements which may be repeated because of
+  /// a goto statement that jumps back.
+  bool check_for_looped_mallocs(const goto_programt &);
+
+  /// Inserts an assertion statement into program before the assignment ins_it,
+  /// to ensure that the left-hand-side of the assignment aliases some
+  /// expression in original_references, unless it is contained in
+  /// freely_assignable_exprs.
+  void instrument_assigns_statement(
+    goto_programt::instructionst::iterator &ins_it,
+    goto_programt &program,
+    exprt &assigns,
+    std::vector<exprt> &original_references,
+    std::set<exprt> &freely_assignable_exprs);
+
+  /// Inserts an assertion statement into program before the function call at
+  /// ins_it, to ensure that any memory which may be written by the call is
+  /// aliased by some expression in assigns_references,unless it is contained
+  /// in freely_assignable_exprs.
+  void instrument_call_statement(
+    goto_programt::instructionst::iterator &ins_it,
+    goto_programt &program,
+    exprt &assigns,
+    std::vector<exprt> &assigns_references,
+    std::set<exprt> &freely_assignable_exprs);
+
+  /// Creates a local variable declaration for each expression in the assigns
+  /// clause (of the function given by f_sym), and stores them in created_decls.
+  /// Then creates assignment statements to capture the memory addresses of each
+  /// expression in the assigns clause within the associated local variable,
+  /// populating a vector created_references of these local variables.
+  void populate_assigns_references(
+    const symbolt &f_sym,
+    const irep_idt &func_id,
+    goto_programt &created_decls,
+    std::vector<exprt> &created_references);
+
   void code_contracts(goto_functionst::goto_functiont &goto_function);
 
   /// \brief Does the named function have a contract?
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 917e1e79af6..f6943c80aa7 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -573,6 +573,8 @@ IREP_ID_ONE(is_used)
 IREP_ID_TWO(C_spec_loop_invariant, #spec_loop_invariant)
 IREP_ID_TWO(C_spec_requires, #spec_requires)
 IREP_ID_TWO(C_spec_ensures, #spec_ensures)
+IREP_ID_TWO(C_spec_assigns, #spec_assigns)
+IREP_ID_ONE(target_list)
 IREP_ID_ONE(virtual_function)
 IREP_ID_TWO(element_type, element_type)
 IREP_ID_ONE(working_directory)