diff --git a/regression/contracts/assigns_enforce_arrays_01/main.c b/regression/contracts/assigns_enforce_arrays_01/main.c
index 1ec59383c7e..352e0782494 100644
--- a/regression/contracts/assigns_enforce_arrays_01/main.c
+++ b/regression/contracts/assigns_enforce_arrays_01/main.c
@@ -1,4 +1,6 @@
-void f1(int a[], int len) __CPROVER_assigns(a)
+/* clang-format off */
+void f1(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
 {
   int b[10];
   a = b;
diff --git a/regression/contracts/assigns_enforce_arrays_02/main.c b/regression/contracts/assigns_enforce_arrays_02/main.c
index 6f0330dedeb..7aba74a1f64 100644
--- a/regression/contracts/assigns_enforce_arrays_02/main.c
+++ b/regression/contracts/assigns_enforce_arrays_02/main.c
@@ -8,7 +8,9 @@ int nextIdx() __CPROVER_assigns(idx)
   return idx;
 }
 
-void f1(int a[], int len)
+/* clang-format off */
+void f1(int a[], int len) __CPROVER_assigns(idx, a[2 .. 5])
+/* clang-format on */
 {
   a[nextIdx()] = 5;
 }
diff --git a/regression/contracts/assigns_enforce_arrays_03/main.c b/regression/contracts/assigns_enforce_arrays_03/main.c
index 9a51b358f75..a2450ca98e4 100644
--- a/regression/contracts/assigns_enforce_arrays_03/main.c
+++ b/regression/contracts/assigns_enforce_arrays_03/main.c
@@ -1,12 +1,16 @@
-void assign_out_under(int a[], int len) __CPROVER_assigns(a)
+/* clang-format off */
+void f1(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
 {
-  a[1] = 5;
+  int *indr;
+  indr = a + 3;
+  *indr = 5;
 }
 
 int main()
 {
   int arr[10];
-  assign_out_under(arr, 10);
+  f1(arr, 10);
 
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_arrays_03/test.desc b/regression/contracts/assigns_enforce_arrays_03/test.desc
index e5c01665aa6..39e6d7656c4 100644
--- a/regression/contracts/assigns_enforce_arrays_03/test.desc
+++ b/regression/contracts/assigns_enforce_arrays_03/test.desc
@@ -1,10 +1,10 @@
 CORE
 main.c
 --enforce-all-contracts
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
+^VERIFICATION SUCCESSFUL$
 --
 --
-Checks whether verification fails when an array is assigned at an index
-below its lower bound.
+Checks whether verification succeeds when an array is assigned indirectly
+through a pointer.
diff --git a/regression/contracts/assigns_enforce_arrays_04/main.c b/regression/contracts/assigns_enforce_arrays_04/main.c
index 6e51934a449..64360838fa2 100644
--- a/regression/contracts/assigns_enforce_arrays_04/main.c
+++ b/regression/contracts/assigns_enforce_arrays_04/main.c
@@ -1,21 +1,28 @@
-void assigns_single(int a[], int len) __CPROVER_assigns(a)
+void assigns_single(int a[], int len) __CPROVER_assigns(a[8])
 {
+  a[8] = 20;
 }
 
-void assigns_range(int a[], int len) __CPROVER_assigns(a)
+/* clang-format off */
+void assigns_upper_bound(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
 {
+  a[5] = 10;
 }
 
-void assigns_big_range(int a[], int len) __CPROVER_assigns(a)
+/* clang-format off */
+void assigns_lower_bound(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format oon */
 {
-  assigns_single(a, len);
-  assigns_range(a, len);
+  a[2] = 10;
 }
 
 int main()
 {
   int arr[10];
-  assigns_big_range(arr, 10);
+  assigns_upper_bound(arr, 10);
+  assigns_lower_bound(arr, 10);
+  assigns_single(arr, 10);
 
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_arrays_04/test.desc b/regression/contracts/assigns_enforce_arrays_04/test.desc
index 4ce2c8bc8d2..9029d280c1c 100644
--- a/regression/contracts/assigns_enforce_arrays_04/test.desc
+++ b/regression/contracts/assigns_enforce_arrays_04/test.desc
@@ -6,6 +6,6 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Checks whether verification succeeds when an array is assigned through
-calls to functions with array assigns clauses which are compatible with
-that of the caller.
+Checks whether verification succeeds when an array is assigned at both upper
+and lower bounds of its assignable array range. Single-value array range
+assignment is checked as well.
diff --git a/regression/contracts/assigns_enforce_arrays_05/main.c b/regression/contracts/assigns_enforce_arrays_05/main.c
index 4eade02f201..52864d9a318 100644
--- a/regression/contracts/assigns_enforce_arrays_05/main.c
+++ b/regression/contracts/assigns_enforce_arrays_05/main.c
@@ -1,18 +1,14 @@
-void assigns_ptr(int *x) __CPROVER_assigns(*x)
+/* clang-format off */
+void assign_out_under(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
 {
-  *x = 200;
-}
-
-void assigns_range(int a[], int len) __CPROVER_assigns(a)
-{
-  int *ptr = &(a[7]);
-  assigns_ptr(ptr);
+  a[1] = 5;
 }
 
 int main()
 {
   int arr[10];
-  assigns_range(arr, 10);
+  assign_out_under(arr, 10);
 
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/regression/contracts/assigns_enforce_arrays_05/test.desc
index 948fc5eb2e3..e5c01665aa6 100644
--- a/regression/contracts/assigns_enforce_arrays_05/test.desc
+++ b/regression/contracts/assigns_enforce_arrays_05/test.desc
@@ -6,6 +6,5 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-Checks whether verification fails when an array is assigned via a
-function call which assigns a pointer to an element out of the
-allowable range.
+Checks whether verification fails when an array is assigned at an index
+below its lower bound.
diff --git a/regression/contracts/assigns_enforce_arrays_06/main.c b/regression/contracts/assigns_enforce_arrays_06/main.c
new file mode 100644
index 00000000000..e4135eff68b
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_06/main.c
@@ -0,0 +1,12 @@
+void assign_out_under(int a[], int len) __CPROVER_assigns(a[8])
+{
+  a[7] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  assign_out_under(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_06/test.desc b/regression/contracts/assigns_enforce_arrays_06/test.desc
new file mode 100644
index 00000000000..bc12b9ec703
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_06/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when an array is assigned at an index below
+its allowed index and specification contains only a single cell
+instead of a range.
diff --git a/regression/contracts/assigns_enforce_arrays_07/main.c b/regression/contracts/assigns_enforce_arrays_07/main.c
new file mode 100644
index 00000000000..7c6354ad779
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_07/main.c
@@ -0,0 +1,14 @@
+/* clang-format off */
+void assign_out_over(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+  a[6] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  assign_out_over(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_07/test.desc b/regression/contracts/assigns_enforce_arrays_07/test.desc
new file mode 100644
index 00000000000..9b98c8432d1
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_07/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when an array is assigned at an index
+above its upper bound.
diff --git a/regression/contracts/assigns_enforce_arrays_08/main.c b/regression/contracts/assigns_enforce_arrays_08/main.c
new file mode 100644
index 00000000000..1482be83ee4
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_08/main.c
@@ -0,0 +1,12 @@
+void assign_out_under(int a[], int len) __CPROVER_assigns(a[8])
+{
+  a[9] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  assign_out_under(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_08/test.desc b/regression/contracts/assigns_enforce_arrays_08/test.desc
new file mode 100644
index 00000000000..f9dde7d0011
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_08/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when an array is assigned at an index
+above its allowed index.
diff --git a/regression/contracts/assigns_enforce_arrays_09/main.c b/regression/contracts/assigns_enforce_arrays_09/main.c
new file mode 100644
index 00000000000..03ffb9f9b72
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_09/main.c
@@ -0,0 +1,14 @@
+/* clang-format off */
+void assigns_in_range(int a[], int last_idx) __CPROVER_assigns(a[2 .. last_idx])
+/* clang-format on */
+{
+  a[last_idx] = 6;
+}
+
+int main()
+{
+  int arr[10];
+  assigns_in_range(arr, 9);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_09/test.desc b/regression/contracts/assigns_enforce_arrays_09/test.desc
new file mode 100644
index 00000000000..b44b6a39da7
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_09/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when an array is assigned at the upper
+bounds of its assignable array range, when the range has a non-constant bound.
diff --git a/regression/contracts/assigns_enforce_arrays_10/main.c b/regression/contracts/assigns_enforce_arrays_10/main.c
new file mode 100644
index 00000000000..376cfdf442b
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_10/main.c
@@ -0,0 +1,15 @@
+/* clang-format off */
+void assigns_in_range(int a[], int last_idx) __CPROVER_assigns(a[2 .. last_idx])
+/* clang-format on */
+{
+  last_idx++;
+  a[last_idx] = 6;
+}
+
+int main()
+{
+  int arr[10];
+  assigns_in_range(arr, 9);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_10/test.desc b/regression/contracts/assigns_enforce_arrays_10/test.desc
new file mode 100644
index 00000000000..abb4c6a465c
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_10/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when an array is assigned past the upper
+bound of its assignable array range, using the symbol of the upper bound,
+after it has been incremented. This is intended to show that the bounds
+are determined at the time the function is called.
diff --git a/regression/contracts/assigns_enforce_arrays_11/main.c b/regression/contracts/assigns_enforce_arrays_11/main.c
new file mode 100644
index 00000000000..93e60ce0516
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_11/main.c
@@ -0,0 +1,25 @@
+void assigns_single(int a[], int len) __CPROVER_assigns(a[7])
+{
+}
+
+/* clang-format off */
+void assigns_range(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+}
+
+/* clang-format off */
+void assigns_big_range(int a[], int len) __CPROVER_assigns(a[2 .. 7])
+/* clang-format on */
+{
+  assigns_single(a, len);
+  assigns_range(a, len);
+}
+
+int main()
+{
+  int arr[10];
+  assigns_big_range(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_11/test.desc b/regression/contracts/assigns_enforce_arrays_11/test.desc
new file mode 100644
index 00000000000..4ce2c8bc8d2
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_11/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when an array is assigned through
+calls to functions with array assigns clauses which are compatible with
+that of the caller.
diff --git a/regression/contracts/assigns_enforce_arrays_12/main.c b/regression/contracts/assigns_enforce_arrays_12/main.c
new file mode 100644
index 00000000000..3b1997f02de
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_12/main.c
@@ -0,0 +1,20 @@
+/* clang-format off */
+void assign_25(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+}
+
+/* clang-format off */
+void assign_37(int a[], int len) __CPROVER_assigns(a[3 .. 7])
+/* clang-format on */
+{
+  assign_25(a, len);
+}
+
+int main()
+{
+  int arr[10];
+  assign_37(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_12/test.desc b/regression/contracts/assigns_enforce_arrays_12/test.desc
new file mode 100644
index 00000000000..a1713e27414
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_12/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when a function with an array assigns target
+calls a function which may assign below the allowable range.
diff --git a/regression/contracts/assigns_enforce_arrays_13/main.c b/regression/contracts/assigns_enforce_arrays_13/main.c
new file mode 100644
index 00000000000..c71bd5a84a7
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_13/main.c
@@ -0,0 +1,20 @@
+void assigns_ptr(int *x) __CPROVER_assigns(*x)
+{
+  *x = 200;
+}
+
+/* clang-format off */
+void assigns_range(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+  int *ptr = &(a[3]);
+  assigns_ptr(ptr);
+}
+
+int main()
+{
+  int arr[10];
+  assigns_range(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_13/test.desc b/regression/contracts/assigns_enforce_arrays_13/test.desc
new file mode 100644
index 00000000000..a468f50b98a
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_13/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when an array is assigned via a
+function call which assigns a pointer to one of its elements.
diff --git a/regression/contracts/assigns_enforce_arrays_14/main.c b/regression/contracts/assigns_enforce_arrays_14/main.c
new file mode 100644
index 00000000000..ff7c0deec8d
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_14/main.c
@@ -0,0 +1,20 @@
+void assigns_ptr(int *x) __CPROVER_assigns(*x)
+{
+  *x = 200;
+}
+
+/* clang-format off */
+void assigns_range(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+  int *ptr = &(a[7]);
+  assigns_ptr(ptr);
+}
+
+int main()
+{
+  int arr[10];
+  assigns_range(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_arrays_14/test.desc b/regression/contracts/assigns_enforce_arrays_14/test.desc
new file mode 100644
index 00000000000..948fc5eb2e3
--- /dev/null
+++ b/regression/contracts/assigns_enforce_arrays_14/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when an array is assigned via a
+function call which assigns a pointer to an element out of the
+allowable range.
diff --git a/regression/contracts/assigns_enforce_multi_file_03/header.h b/regression/contracts/assigns_enforce_multi_file_03/header.h
new file mode 100644
index 00000000000..56149c42aa2
--- /dev/null
+++ b/regression/contracts/assigns_enforce_multi_file_03/header.h
@@ -0,0 +1,24 @@
+void assigns_single(int a[], int len);
+
+void assigns_upper_bound(int a[], int len);
+
+void assigns_lower_bound(int a[], int len);
+
+void assigns_single(int a[], int len) __CPROVER_assigns(a[8])
+{
+  a[8] = 20;
+}
+
+/* clang-format off */
+void assigns_upper_bound(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+  a[5] = 10;
+}
+
+/* clang-format off */
+void assigns_lower_bound(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+  a[2] = 10;
+}
diff --git a/regression/contracts/assigns_enforce_multi_file_03/main.c b/regression/contracts/assigns_enforce_multi_file_03/main.c
new file mode 100644
index 00000000000..4e71f7c610d
--- /dev/null
+++ b/regression/contracts/assigns_enforce_multi_file_03/main.c
@@ -0,0 +1,11 @@
+#include "header.h"
+
+int main()
+{
+  int arr[10];
+  assigns_upper_bound(arr, 10);
+  assigns_lower_bound(arr, 10);
+  assigns_single(arr, 10);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_multi_file_03/test.desc b/regression/contracts/assigns_enforce_multi_file_03/test.desc
new file mode 100644
index 00000000000..05289a4a199
--- /dev/null
+++ b/regression/contracts/assigns_enforce_multi_file_03/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test replicates the behavior of assigns_enforce_arrays_04, but separates
+the function headers and contracts into a separate file header.h.
diff --git a/regression/contracts/assigns_replace_06/main.c b/regression/contracts/assigns_replace_06/main.c
index dc54f4ff8e2..4a98c8345a9 100644
--- a/regression/contracts/assigns_replace_06/main.c
+++ b/regression/contracts/assigns_replace_06/main.c
@@ -1,10 +1,12 @@
 #include <assert.h>
 
-void foo(char c[]) __CPROVER_assigns(c)
+/* clang-format off */
+void foo(char c[]) __CPROVER_assigns(c[2 .. 4])
+/* clang-format on */
 {
 }
 
-void bar(char d[]) __CPROVER_assigns(d)
+void bar(char d[]) __CPROVER_assigns(d[7])
 {
 }
 
diff --git a/regression/contracts/assigns_replace_07/main.c b/regression/contracts/assigns_replace_07/main.c
index 84e534f6562..830ccff9d97 100644
--- a/regression/contracts/assigns_replace_07/main.c
+++ b/regression/contracts/assigns_replace_07/main.c
@@ -1,6 +1,8 @@
 #include <assert.h>
 
-void bar(char d[]) __CPROVER_assigns(d[7])
+/* clang-format off */
+void foo(char c[]) __CPROVER_assigns(c[2 .. 4])
+/* clang-format on */
 {
 }
 
@@ -17,8 +19,8 @@ int main()
   b[7] = 'h';
   b[8] = 'i';
   b[9] = 'j';
-  bar(b);
-  assert(b[7] == 'h');
+  foo(b);
+  assert(b[2] == 'c' || b[3] == 'd' || b[4] == 'e');
 
   return 0;
 }
diff --git a/regression/contracts/assigns_replace_07/test.desc b/regression/contracts/assigns_replace_07/test.desc
index db3a9dbd079..40a1916c54c 100644
--- a/regression/contracts/assigns_replace_07/test.desc
+++ b/regression/contracts/assigns_replace_07/test.desc
@@ -6,5 +6,5 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-Checks whether the value inside a single-index array assigns target is
-havocked when calling the associated function.
+Checks whether the values inside an array range specified by the assigns
+target are havocked when calling the associated function.
diff --git a/regression/contracts/assigns_replace_08/main.c b/regression/contracts/assigns_replace_08/main.c
new file mode 100644
index 00000000000..84e534f6562
--- /dev/null
+++ b/regression/contracts/assigns_replace_08/main.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+
+void bar(char d[]) __CPROVER_assigns(d[7])
+{
+}
+
+int main()
+{
+  char b[10];
+  b[0] = 'a';
+  b[1] = 'b';
+  b[2] = 'c';
+  b[3] = 'd';
+  b[4] = 'e';
+  b[5] = 'f';
+  b[6] = 'g';
+  b[7] = 'h';
+  b[8] = 'i';
+  b[9] = 'j';
+  bar(b);
+  assert(b[7] == 'h');
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_replace_08/test.desc b/regression/contracts/assigns_replace_08/test.desc
new file mode 100644
index 00000000000..db3a9dbd079
--- /dev/null
+++ b/regression/contracts/assigns_replace_08/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether the value inside a single-index array assigns target is
+havocked when calling the associated function.
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index 47b6cd77b05..effde697f28 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -163,6 +163,7 @@ class c_typecheck_baset:
   virtual void typecheck_expr_operands(exprt &expr);
   virtual void typecheck_expr_comma(exprt &expr);
   virtual void typecheck_expr_constant(exprt &expr);
+  virtual void typecheck_expr_range(exprt &expr);
   virtual void typecheck_expr_side_effect(side_effect_exprt &expr);
   virtual void typecheck_expr_unary_arithmetic(exprt &expr);
   virtual void typecheck_expr_unary_boolean(exprt &expr);
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 25eee7f69e5..f31c3d4fd90 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -491,6 +491,10 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
   {
     // already type checked
   }
+  else if(expr.id() == ID_range)
+  {
+    typecheck_expr_range(expr);
+  }
   else
   {
     error().source_location = expr.source_location();
@@ -499,6 +503,16 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
   }
 }
 
+void c_typecheck_baset::typecheck_expr_range(exprt &expr)
+{
+  // Already type checked
+  exprt &lower = to_range_exprt(expr).lower();
+  exprt &upper = to_range_exprt(expr).upper();
+
+  implicit_typecast_arithmetic(lower);
+  implicit_typecast_arithmetic(upper);
+}
+
 void c_typecheck_baset::typecheck_expr_comma(exprt &expr)
 {
   expr.type() = to_binary_expr(expr).op1().type();
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 38bcd911c3a..46237ad4930 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -102,6 +102,7 @@ extern char *yyansi_ctext;
 %token TOK_ANDAND    "&&"
 %token TOK_OROR      "||"
 %token TOK_ELLIPSIS  "..."
+%token TOK_RANGE     ".."
 
 /*** modifying assignment operators ***/
 
@@ -3243,7 +3244,7 @@ cprover_contract:
           set($$, ID_C_spec_requires);
           mto($$, $3);
         }
-        | TOK_CPROVER_ASSIGNS '(' argument_expression_list ')'
+        | TOK_CPROVER_ASSIGNS '(' target_list ')'
         {
           $$=$1;
           set($$, ID_C_spec_assigns);
@@ -3252,6 +3253,76 @@ cprover_contract:
         }
         ;
 
+target_list:
+          target
+        {
+          init($$, ID_target_list);
+          mto($$, $1);
+        }
+        | target_list ',' target
+        {
+          $$=$1;
+          mto($$, $3);
+        }
+        ;
+
+target:
+          deref_target
+        | target '[' array_index ']'
+        { binary($$, $1, $2, ID_range, $3); }
+        | target '[' array_range ']'
+        { binary($$, $1, $2, ID_range, $3); }
+        ;
+
+array_index:
+          identifier
+        | integer
+        ;
+
+array_range:
+        array_index TOK_RANGE array_index
+        {
+          $$=$2;
+          set($$, ID_range);
+          mto($$, $1);
+          mto($$, $3);
+        }
+        ;
+
+deref_target:
+          member_target
+        | '*' deref_target
+        {
+          $$=$1;
+          set($$, ID_dereference);
+          mto($$, $2);
+        }
+        ;
+
+member_target:
+          primary_target
+        | member_target '.' member_name
+        {
+          $$=$2;
+          set($$, ID_member);
+          mto($$, $1);
+          parser_stack($$).set(ID_component_name, parser_stack($3).get(ID_C_base_name));
+        }
+        | member_target TOK_ARROW member_name
+        {
+          $$=$2;
+          set($$, ID_ptrmember);
+          mto($$, $1);
+          parser_stack($$).set(ID_component_name, parser_stack($3).get(ID_C_base_name));
+        }
+        ;
+
+primary_target:
+          identifier
+        | '(' target ')'
+        { $$ = $2; }
+        ;
+
 cprover_contract_sequence:
           cprover_contract
         | cprover_contract_sequence cprover_contract
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index 79b87f1a833..3d79dab47d6 100644
--- a/src/ansi-c/scanner.l
+++ b/src/ansi-c/scanner.l
@@ -1517,6 +1517,7 @@ __decltype          { if(PARSER.cpp98 &&
 "&&"            { loc(); return TOK_ANDAND; }
 "||"            { loc(); return TOK_OROR; }
 "..."           { loc(); return TOK_ELLIPSIS; }
+".."            { loc(); return TOK_RANGE; }
 
 "*="            { loc(); return TOK_MULTASSIGN; }
 "/="            { loc(); return TOK_DIVASSIGN; }
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
index c1788326964..e0ec766c356 100644
--- a/src/goto-instrument/code_contracts.cpp
+++ b/src/goto-instrument/code_contracts.cpp
@@ -1173,13 +1173,26 @@ assigns_clause_array_targett::assigns_clause_array_targett(
   code_contractst &contract,
   messaget &log_parameter,
   const irep_idt &function_id)
-  : assigns_clause_targett(Array, object_ptr, contract, log_parameter),
+  : assigns_clause_targett(
+      Array,
+      to_range_exprt(object_ptr).lower(),
+      contract,
+      log_parameter),
     lower_offset_object(),
     upper_offset_object(),
     array_standin_variable(typet()),
     lower_offset_variable(typet()),
     upper_offset_variable(typet())
 {
+  const exprt &array = to_range_exprt(object_ptr).lower();
+  const exprt &range = to_range_exprt(object_ptr).upper();
+
+  // If the range doesn't have operands, it is just a single value
+  const exprt &lower_operand =
+    range.has_operands() ? to_range_exprt(range).lower() : range;
+  const exprt &upper_operand =
+    range.has_operands() ? to_range_exprt(range).upper() : range;
+
   const symbolt &function_symbol = contract.ns.lookup(function_id);
 
   // Declare a new symbol to stand in for the reference
@@ -1198,13 +1211,24 @@ assigns_clause_array_targett::assigns_clause_array_targett(
     code_assignt(array_standin_variable, pointer_object),
     function_symbol.location));
 
-  if(object_ptr.id() == ID_address_of)
+  if(lower_operand.id() == ID_constant)
   {
-    exprt constant_size =
-      get_size(object_ptr.type().subtype(), contract.ns, log);
+    int lowerbase = std::stoi(
+      to_constant_expr(lower_operand).get(ID_C_base).c_str(), nullptr, 10);
+    lower_bound = std::stoi(
+      to_constant_expr(lower_operand).get_value().c_str(), nullptr, lowerbase);
+
+    irep_idt lower_const_string(
+      from_integer(lower_bound, integer_typet()).get_value());
+    irep_idt lower_const_irep(lower_const_string);
+    constant_exprt lower_val_const(lower_const_irep, lower_operand.type());
+
+    exprt lower_constant_size =
+      get_size(array.type().subtype(), contract.ns, log);
     lower_offset_object = typecast_exprt(
       mult_exprt(
-        typecast_exprt(object_ptr, unsigned_long_int_type()), constant_size),
+        typecast_exprt(lower_val_const, unsigned_long_int_type()),
+        lower_constant_size),
       signed_int_type());
 
     // Declare a new symbol to stand in for the reference
@@ -1222,10 +1246,78 @@ assigns_clause_array_targett::assigns_clause_array_targett(
     init_block.add(goto_programt::make_assignment(
       code_assignt(lower_offset_variable, lower_offset_object),
       function_symbol.location));
+  }
+  else
+  {
+    exprt lower_constant_size =
+      get_size(array.type().subtype(), contract.ns, log);
+    lower_offset_object = typecast_exprt(
+      mult_exprt(
+        typecast_exprt(lower_operand, unsigned_long_int_type()),
+        lower_constant_size),
+      signed_int_type());
+
+    // Declare a new symbol to stand in for the reference
+    symbolt lower_standin_symbol = contract.new_tmp_symbol(
+      lower_offset_object.type(),
+      function_symbol.location,
+      function_id,
+      function_symbol.mode);
+
+    lower_offset_variable = lower_standin_symbol.symbol_expr();
 
+    // Add array temp to variable initialization block
+    init_block.add(goto_programt::make_decl(
+      lower_offset_variable, function_symbol.location));
+    init_block.add(goto_programt::make_assignment(
+      code_assignt(lower_offset_variable, lower_offset_object),
+      function_symbol.location));
+  }
+
+  if(upper_operand.id() == ID_constant)
+  {
+    int upperbase = std::stoi(
+      to_constant_expr(upper_operand).get(ID_C_base).c_str(), nullptr, 10);
+    upper_bound = std::stoi(
+      to_constant_expr(upper_operand).get_value().c_str(), nullptr, upperbase);
+
+    irep_idt upper_const_string(
+      from_integer(upper_bound, integer_typet()).get_value());
+    irep_idt upper_const_irep(upper_const_string);
+    constant_exprt upper_val_const(upper_const_irep, upper_operand.type());
+
+    exprt upper_constant_size =
+      get_size(array.type().subtype(), contract.ns, log);
+    upper_offset_object = typecast_exprt(
+      mult_exprt(
+        typecast_exprt(upper_val_const, unsigned_long_int_type()),
+        upper_constant_size),
+      signed_int_type());
+
+    // Declare a new symbol to stand in for the reference
+    symbolt upper_standin_symbol = contract.new_tmp_symbol(
+      upper_offset_object.type(),
+      function_symbol.location,
+      function_id,
+      function_symbol.mode);
+
+    upper_offset_variable = upper_standin_symbol.symbol_expr();
+
+    // Add array temp to variable initialization block
+    init_block.add(goto_programt::make_decl(
+      upper_offset_variable, function_symbol.location));
+    init_block.add(goto_programt::make_assignment(
+      code_assignt(upper_offset_variable, upper_offset_object),
+      function_symbol.location));
+  }
+  else
+  {
+    exprt upper_constant_size =
+      get_size(array.type().subtype(), contract.ns, log);
     upper_offset_object = typecast_exprt(
       mult_exprt(
-        typecast_exprt(object_ptr, unsigned_long_int_type()), constant_size),
+        typecast_exprt(upper_operand, unsigned_long_int_type()),
+        upper_constant_size),
       signed_int_type());
 
     // Declare a new symbol to stand in for the reference
@@ -1267,7 +1359,7 @@ assigns_clause_array_targett::havoc_code(source_locationt location) const
   exprt array_type_size =
     get_size(pointer_object.type().subtype(), contract.ns, log);
 
-  for(mp_integer i = lower_bound; i < upper_bound; ++i)
+  for(mp_integer i = lower_bound; i <= upper_bound; ++i)
   {
     irep_idt offset_string(from_integer(i, integer_typet()).get_value());
     irep_idt offset_irep(offset_string);
@@ -1360,7 +1452,7 @@ assigns_clauset::~assigns_clauset()
 
 assigns_clause_targett *assigns_clauset::add_target(exprt current_operation)
 {
-  if(current_operation.id() == ID_address_of)
+  if(current_operation.id() == ID_range)
   {
     assigns_clause_array_targett *array_target =
       new assigns_clause_array_targett(
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 3988f8b0777..e413dd4f342 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -824,6 +824,67 @@ inline multi_ary_exprt &to_multi_ary_expr(exprt &expr)
   return static_cast<multi_ary_exprt &>(expr);
 }
 
+/// \brief A base class for int-range expressions
+class range_exprt : public expr_protectedt
+{
+public:
+  range_exprt(exprt &lower, exprt &upper, typet _type)
+    : expr_protectedt(
+        ID_range,
+        std::move(_type),
+        {std::move(lower), std::move(upper)})
+  {
+  }
+
+  exprt &lower()
+  {
+    return op0();
+  }
+
+  const exprt &lower() const
+  {
+    return op0();
+  }
+
+  exprt &upper()
+  {
+    return op1();
+  }
+
+  const exprt &upper() const
+  {
+    return op1();
+  }
+
+  const exprt &op2() const = delete;
+  exprt &op2() = delete;
+  const exprt &op3() const = delete;
+  exprt &op3() = delete;
+};
+
+/// \brief Cast an exprt to a \ref range_exprt
+///
+/// \a expr must be known to be \ref range_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref range_exprt
+inline const range_exprt &to_range_exprt(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_range);
+  return static_cast<const range_exprt &>(expr);
+}
+
+/// \brief Cast an exprt to a \ref range_exprt
+///
+/// \a expr must be known to be \ref range_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref range_exprt
+inline range_exprt &to_range_exprt(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_range);
+  return static_cast<range_exprt &>(expr);
+}
 
 /// \brief The plus expression
 /// Associativity is not specified.