diff --git a/doc/cprover-manual/contracts-assigns.md b/doc/cprover-manual/contracts-assigns.md
index de8930f269a..7492acbfa89 100644
--- a/doc/cprover-manual/contracts-assigns.md
+++ b/doc/cprover-manual/contracts-assigns.md
@@ -18,25 +18,44 @@ value(s) therein are not modified.
 The following functions can be used in assigns clause to specify ranges of 
 assignable addresses.
 
+Given an lvalue expression `expr` with a complete type `expr_t`,
+ `__CPROVER_typed_target(expr)` specifies that the range 
+ of `sizeof(expr_t)` bytes starting at `&expr` is assignable:
+```c
+__CPROVER_assignable_t __CPROVER_typed_target(expr_t expr);
+```
+
+Given a pointer `ptr` pointing into some object `o`, 
+`__CPROVER_whole_object(ptr)` specifies that all bytes of the object `o`
+are assignable:
+```c
+__CPROVER_assignable_t __CPROVER_whole_object(void *ptr);
+```
+
 Given a pointer `ptr` pointing into some object `o`, `__CPROVER_object_from(ptr)` 
-specifies that all bytes starting from the given pointer and until the end of 
-the object are assignable:
+specifies that the range of bytes starting from the pointer and until the end of 
+the object `o` are assignable:
 ```c
-__CPROVER_size_t __CPROVER_object_from(void *ptr); 
+__CPROVER_assignable_t __CPROVER_object_from(void *ptr);
 ```
 
-Given a pointer `ptr` pointing into some object `o`, `__CPROVER_object_from(ptr, size)` 
-specifies that `size` bytes starting from the given pointer and until the end of the object are assignable.
-The `size` value must such that `size <= __CPROVER_object_size(ptr) - __CPROVER_pointer_offset(ptr)` holds:
+Given a pointer `ptr` pointing into some object `o`, `__CPROVER_object_upto(ptr, size)` 
+specifies that the range of `size` bytes of `o` starting at `ptr` are assignable:
+The `size` value must such that the range does not exceed the object boundary,
+that is, `__CPROVER_object_size(ptr) - __CPROVER_pointer_offset(ptr) >= size` must hold:
 
 ```c
-__CPROVER_size_t __CPROVER_object_slice(void *ptr, __CPROVER_size_t size);
+__CPROVER_assignable_t __CPROVER_object_upto(void *ptr, __CPROVER_size_t size);
 ```
 
-Caveats and limitations: The slices in question must *not*
-be interpreted as pointers by the program. During call-by-contract replacement, 
-`__CPROVER_havoc_slice(ptr, size)` is used to havoc these targets, 
-and `__CPROVER_havoc_slice` does not support havocing pointers. 
+CAVEAT: The ranges specified by `__CPROVER_whole_object`,
+`__CPROVER_object_from` and `__CPROVER_object_upto` must *not*
+be interpreted as pointers by the program. This is because during 
+call-by-contract replacement, `__CPROVER_havoc_slice(ptr, size)` is used to
+havoc these byte ranges, and `__CPROVER_havoc_slice` does not support
+havocing pointers. `__CPROVER_typed_target` must be used to specify targets
+that are pointers.
+
 ### Parameters
 
 An _assigns_ clause currently supports simple variable types and their pointers,
diff --git a/regression/contracts/assigns-slice-targets/main-enforce.c b/regression/contracts/assigns-slice-targets/main-enforce.c
index 7f39d6f06cd..aa1c5a4070d 100644
--- a/regression/contracts/assigns-slice-targets/main-enforce.c
+++ b/regression/contracts/assigns-slice-targets/main-enforce.c
@@ -7,11 +7,14 @@ struct st
   int c;
 };
 
-void foo(struct st *s)
+void foo(struct st *s, struct st *ss)
   // clang-format off
   __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s)))
-  __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5))
-  __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5))
+  __CPROVER_assigns(
+    __CPROVER_object_upto(s->arr1, 5);
+    __CPROVER_object_from(s->arr2 + 5);
+    __CPROVER_whole_object(ss);
+)
 // clang-format on
 {
   // PASS
@@ -41,13 +44,24 @@ void foo(struct st *s)
   s->arr2[7] = 0;
   s->arr2[8] = 0;
   s->arr2[9] = 0;
+
+  // PASS
+  ss->a = 0;
+  ss->arr1[0] = 0;
+  ss->arr1[7] = 0;
+  ss->arr1[9] = 0;
+  ss->b = 0;
+  ss->arr2[6] = 0;
+  ss->arr2[8] = 0;
+  ss->c = 0;
 }
 
 int main()
 {
   struct st s;
+  struct st ss;
 
-  foo(&s);
+  foo(&s, &ss);
 
   return 0;
 }
diff --git a/regression/contracts/assigns-slice-targets/main-replace.c b/regression/contracts/assigns-slice-targets/main-replace.c
index 5f21100ee7c..975d43b8606 100644
--- a/regression/contracts/assigns-slice-targets/main-replace.c
+++ b/regression/contracts/assigns-slice-targets/main-replace.c
@@ -7,11 +7,14 @@ struct st
   int c;
 };
 
-void foo(struct st *s)
+void foo(struct st *s, struct st *ss)
   // clang-format off
   __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s)))
-  __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5))
-  __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5))
+  __CPROVER_assigns(
+    __CPROVER_object_upto(s->arr1, 5);
+    __CPROVER_object_from(s->arr2 + 5);
+    __CPROVER_whole_object(ss);
+  )
 // clang-format on
 {
   s->arr1[0] = 0;
@@ -54,7 +57,32 @@ int main()
   s.arr2[9] = 0;
   s.c = 0;
 
-  foo(&s);
+  struct st ss;
+  ss.a = 0;
+  ss.arr1[0] = 0;
+  ss.arr1[1] = 0;
+  ss.arr1[2] = 0;
+  ss.arr1[3] = 0;
+  ss.arr1[4] = 0;
+  ss.arr1[5] = 0;
+  ss.arr1[6] = 0;
+  ss.arr1[7] = 0;
+  ss.arr1[8] = 0;
+  ss.arr1[9] = 0;
+
+  ss.arr2[0] = 0;
+  ss.arr2[1] = 0;
+  ss.arr2[2] = 0;
+  ss.arr2[3] = 0;
+  ss.arr2[4] = 0;
+  ss.arr2[5] = 0;
+  ss.arr2[6] = 0;
+  ss.arr2[7] = 0;
+  ss.arr2[8] = 0;
+  ss.arr2[9] = 0;
+  ss.c = 0;
+
+  foo(&s, &ss);
 
   // PASS
   assert(s.a == 0);
@@ -92,5 +120,31 @@ int main()
 
   // PASS
   assert(s.c == 0);
+
+  // FAIL
+  assert(ss.a == 0);
+  assert(ss.arr1[0] == 0);
+  assert(ss.arr1[1] == 0);
+  assert(ss.arr1[2] == 0);
+  assert(ss.arr1[3] == 0);
+  assert(ss.arr1[4] == 0);
+  assert(ss.arr1[5] == 0);
+  assert(ss.arr1[6] == 0);
+  assert(ss.arr1[7] == 0);
+  assert(ss.arr1[8] == 0);
+  assert(ss.arr1[9] == 0);
+  assert(ss.b == 0);
+  assert(ss.arr2[0] == 0);
+  assert(ss.arr2[1] == 0);
+  assert(ss.arr2[2] == 0);
+  assert(ss.arr2[3] == 0);
+  assert(ss.arr2[4] == 0);
+  assert(ss.arr2[5] == 0);
+  assert(ss.arr2[6] == 0);
+  assert(ss.arr2[7] == 0);
+  assert(ss.arr2[8] == 0);
+  assert(ss.arr2[9] == 0);
+  assert(ss.c == 0);
+
   return 0;
 }
diff --git a/regression/contracts/assigns-slice-targets/test-enforce.desc b/regression/contracts/assigns-slice-targets/test-enforce.desc
index 5b8f4fe5f58..d7c221d1a86 100644
--- a/regression/contracts/assigns-slice-targets/test-enforce.desc
+++ b/regression/contracts/assigns-slice-targets/test-enforce.desc
@@ -1,8 +1,6 @@
 CORE
 main-enforce.c
 --enforce-contract foo
-^\[foo.assigns.\d+\].* Check that __CPROVER_object_slice\(\(void \*\)s->arr1, \(.*\)5\) is valid: SUCCESS$
-^\[foo.assigns.\d+\].* Check that __CPROVER_object_from\(\(void \*\)\(s->arr2 \+ \(.*\)5\)\) is valid: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$
@@ -23,6 +21,14 @@ main-enforce.c
 ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->a is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)7\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)9\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->b is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)6\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)8\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->c is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns-slice-targets/test-replace.desc b/regression/contracts/assigns-slice-targets/test-replace.desc
index 1f23fb0ae7e..1c7532841a1 100644
--- a/regression/contracts/assigns-slice-targets/test-replace.desc
+++ b/regression/contracts/assigns-slice-targets/test-replace.desc
@@ -24,6 +24,29 @@ main-replace.c
 ^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)8\] == 0: FAILURE$
 ^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)9\] == 0: FAILURE$
 ^\[main.assertion.\d+\].*assertion s.c == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion ss.a == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)0\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)1\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)2\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)3\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)4\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)5\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)6\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)7\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)8\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)9\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion ss.b == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)0\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)1\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)2\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)3\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)4\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)5\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)6\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)7\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)8\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)9\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion ss.c == 0: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/regression/contracts/assigns_enforce_address_of/test.desc
index 7500be4b1e4..9b717247265 100644
--- a/regression/contracts/assigns_enforce_address_of/test.desc
+++ b/regression/contracts/assigns_enforce_address_of/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc
index 2a9141844c9..dd48913cefd 100644
--- a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc
+++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc
index 2a9141844c9..dd48913cefd 100644
--- a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc
+++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc
index 5f482125c08..a8e3b382646 100644
--- a/regression/contracts/assigns_enforce_function_calls/test.desc
+++ b/regression/contracts/assigns_enforce_function_calls/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: function calls in assigns clause targets must be to __CPROVER_object_from, __CPROVER_object_slice$
+^.*error: expecting __CPROVER_assignable_t return type for function bar called in assigns clause$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/regression/contracts/assigns_enforce_literal/test.desc
index 74d1d576235..d1952cdfe3c 100644
--- a/regression/contracts/assigns_enforce_literal/test.desc
+++ b/regression/contracts/assigns_enforce_literal/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_side_effects_2/test.desc b/regression/contracts/assigns_enforce_side_effects_2/test.desc
index 8cab6884f92..368481cb54d 100644
--- a/regression/contracts/assigns_enforce_side_effects_2/test.desc
+++ b/regression/contracts/assigns_enforce_side_effects_2/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_side_effects_3/test.desc b/regression/contracts/assigns_enforce_side_effects_3/test.desc
index 8cab6884f92..368481cb54d 100644
--- a/regression/contracts/assigns_enforce_side_effects_3/test.desc
+++ b/regression/contracts/assigns_enforce_side_effects_3/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc
index 51c84807dcb..232c8b3f575 100644
--- a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc
+++ b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 --
 Checks whether type checking rejects literal constants in assigns clause.
diff --git a/regression/contracts/cprover-assignable-fail/main.c b/regression/contracts/cprover-assignable-fail/main.c
new file mode 100644
index 00000000000..073504f16d8
--- /dev/null
+++ b/regression/contracts/cprover-assignable-fail/main.c
@@ -0,0 +1,28 @@
+#include <stdlib.h>
+
+__CPROVER_assignable_t my_write_set(char *arr, size_t size)
+{
+  __CPROVER_assert(
+    !arr || __CPROVER_rw_ok(arr, size), "target null or writable");
+
+  if(arr && size > 0)
+  {
+    __CPROVER_whole_object(arr);
+    __CPROVER_object_upto(arr, size);
+    __CPROVER_object_from(arr);
+    __CPROVER_typed_target(arr[0]);
+  }
+}
+
+void main()
+{
+  size_t size;
+  char *arr;
+  int do_init;
+  if(do_init)
+  {
+    int nondet;
+    arr = nondet ? malloc(size) : NULL;
+  }
+  my_write_set(arr, size);
+}
diff --git a/regression/contracts/cprover-assignable-fail/test.desc b/regression/contracts/cprover-assignable-fail/test.desc
new file mode 100644
index 00000000000..976c79c3c54
--- /dev/null
+++ b/regression/contracts/cprover-assignable-fail/test.desc
@@ -0,0 +1,26 @@
+CORE
+main.c
+
+^\[my_write_set.assertion.\d+\] .* target null or writable: FAILURE$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: pointer NULL in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): FAILURE$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: pointer invalid in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): FAILURE$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: deallocated dynamic object in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): FAILURE$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: dead object in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): FAILURE$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: pointer outside object bounds in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): SUCCESS$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: invalid integer address in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): SUCCESS$
+^\[my_write_set.overflow.\d+\] .* arithmetic overflow on unsigned - in OBJECT_SIZE\(\(void \*\)arr\) - POINTER_OFFSET\(\(void \*\)arr\): FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+CALL __CPROVER_whole_object
+CALL __CPROVER_object_upto
+CALL __CPROVER_object_from
+CALL __CPROVER_typed_target
+--
+This test checks that:
+- the built-in functions used to specify assignable memory locations are
+  supported;
+- that GOTO conversion rewrites calls to __CPROVER_assignable(...) calls;
+- checks for invalid pointers and of overflows in the computations of
+  interval bounds are in place.
diff --git a/regression/contracts/cprover-assignable-pass/main.c b/regression/contracts/cprover-assignable-pass/main.c
new file mode 100644
index 00000000000..04cdbb8f5ff
--- /dev/null
+++ b/regression/contracts/cprover-assignable-pass/main.c
@@ -0,0 +1,24 @@
+#include <stdlib.h>
+
+__CPROVER_assignable_t my_write_set(char *arr, size_t size)
+{
+  __CPROVER_assert(
+    !arr || __CPROVER_rw_ok(arr, size), "target null or writable");
+
+  if(arr && size > 0)
+  {
+    __CPROVER_whole_object(arr);
+    __CPROVER_object_upto(arr, size);
+    __CPROVER_object_from(arr);
+    __CPROVER_typed_target(arr[0]);
+  }
+}
+
+void main()
+{
+  int nondet;
+  size_t size;
+  char *arr;
+  arr = nondet ? malloc(size) : NULL;
+  my_write_set(arr, size);
+}
diff --git a/regression/contracts/cprover-assignable-pass/test.desc b/regression/contracts/cprover-assignable-pass/test.desc
new file mode 100644
index 00000000000..170c541827b
--- /dev/null
+++ b/regression/contracts/cprover-assignable-pass/test.desc
@@ -0,0 +1,27 @@
+CORE
+main.c
+
+^\[my_write_set.assertion.\d+\] .* target null or writable: SUCCESS$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: pointer NULL in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): SUCCESS$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: pointer invalid in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): SUCCESS$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: deallocated dynamic object in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): SUCCESS$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: dead object in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): SUCCESS$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: pointer outside object bounds in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): SUCCESS$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: invalid integer address in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): SUCCESS$
+^\[my_write_set.overflow.\d+\] .* arithmetic overflow on unsigned - in OBJECT_SIZE\(\(void \*\)arr\) - POINTER_OFFSET\(\(void \*\)arr\): SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+CALL __CPROVER_whole_object
+CALL __CPROVER_object_upto
+CALL __CPROVER_object_from
+CALL __CPROVER_typed_target
+--
+This test checks that:
+- the built-in functions used to specify assignable memory locations are
+  supported;
+- that GOTO conversion rewrites calls to __CPROVER_assignable(...) calls;
+- checks for invalid pointers and of overflows in the computations of
+  interval bounds are in place.
+
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 6ea08fb5b44..6df2af503a8 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -216,7 +216,23 @@ void ansi_c_internal_additions(std::string &code)
     // This function needs to be declared, or otherwise can't be called
     // by the entry-point construction.
     "void " INITIALIZE_FUNCTION "(void);\n"
+    "\n"
+    // frame specifications for contracts
+    // Type that describes assignable memory locations
+    "typedef void " CPROVER_PREFIX "assignable_t;\n"
+    // Declares a range of bytes as assignable (internal representation)
+    CPROVER_PREFIX "assignable_t " CPROVER_PREFIX "assignable(void *ptr, "
+    CPROVER_PREFIX "size_t size,"
+    CPROVER_PREFIX "bool is_pointer_to_pointer);\n"
+    // Declares a range of bytes as assignable
+    CPROVER_PREFIX "assignable_t " CPROVER_PREFIX "object_upto(void *ptr, "
+    CPROVER_PREFIX "size_t size);\n"
+    // Declares bytes from ptr to the end of the object as assignable
+    CPROVER_PREFIX "assignable_t " CPROVER_PREFIX "object_from(void *ptr);\n"
+    // Declares the whole object pointer to by ptr
+    CPROVER_PREFIX "assignable_t " CPROVER_PREFIX "whole_object(void *ptr);\n"
     "\n";
+
   // clang-format on
 
   // GCC junk stuff, also for CLANG and ARM
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index e2924c811d3..7a773e8882a 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -909,7 +909,11 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target)
   typecheck_expr(target);
 
   // fatal errors
-  if(target.type().id() == ID_empty)
+  bool is_empty_type = target.type().id() == ID_empty;
+  bool is_assignable_typedef =
+    target.type().get(ID_C_typedef) == CPROVER_PREFIX "assignable_t";
+  // only allow void type if it is the typedef CPROVER_PREFIX "assignable_t"
+  if(target.type().id() == ID_empty && !is_assignable_typedef)
   {
     error().source_location = target.source_location();
     error() << "void-typed expressions not allowed as assigns clause targets"
@@ -950,37 +954,33 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target)
     if(can_cast_expr<symbol_exprt>(funcall.function()))
     {
       const auto &ident = to_symbol_expr(funcall.function()).get_identifier();
-      if(
-        ident == CPROVER_PREFIX "object_from" || ident == CPROVER_PREFIX
-                                                   "object_slice")
-      {
-        for(const auto &argument : funcall.arguments())
-          throw_on_side_effects(argument);
-      }
-      else
+      if(!(is_empty_type && is_assignable_typedef))
       {
         error().source_location = target.source_location();
-        error() << "function calls in assigns clause targets must be "
-                   "to " CPROVER_PREFIX "object_from, " CPROVER_PREFIX
-                   "object_slice"
+        error() << "expecting " CPROVER_PREFIX
+                   "assignable_t return type for function " +
+                     id2string(ident) + " called in assigns clause"
                 << eom;
         throw 0;
       }
+      for(const auto &argument : funcall.arguments())
+        throw_on_side_effects(argument);
     }
     else
     {
       error().source_location = target.source_location();
-      error() << "function pointer calls not allowed in assigns targets" << eom;
+      error() << "function pointer calls not allowed in assigns clauses" << eom;
       throw 0;
     }
   }
   else
   {
     error().source_location = target.source_location();
-    error() << "assigns clause target must be an lvalue or a " CPROVER_PREFIX
-               "POINTER_OBJECT, " CPROVER_PREFIX "object_from, " CPROVER_PREFIX
-               "object_slice expression"
-            << eom;
+    error()
+      << "assigns clause target must be an lvalue or a call to " CPROVER_PREFIX
+         "POINTER_OBJECT or to a function returning " CPROVER_PREFIX
+         "assignable_t"
+      << eom;
     throw 0;
   }
 }
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index fc6589243c4..9bf54ec09b3 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -1943,8 +1943,46 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
     if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
     {
       // This is an undeclared function.
+
+      // Is it the polymorphic assigns clause function ?
+      if(identifier == CPROVER_PREFIX "typed_target")
+      {
+        auto arg0 = expr.arguments().at(0);
+        typecheck_expr(arg0);
+        if(!is_assignable(arg0) || !arg0.get_bool(ID_C_lvalue))
+        {
+          error().source_location = arg0.source_location();
+          error() << "argument of " << CPROVER_PREFIX "typed_target"
+                  << "must be assignable" << eom;
+          throw 0;
+        }
+        const auto &size = size_of_expr(arg0.type(), *this);
+        if(!size.has_value())
+        {
+          error().source_location = arg0.source_location();
+          error() << "sizeof not defined for argument of "
+                  << CPROVER_PREFIX "typed_target"
+                  << " of type " << to_string(arg0.type()) << eom;
+          throw 0;
+        }
+        // rewrite call to "assignable"
+        to_symbol_expr(f_op).set_identifier(CPROVER_PREFIX "assignable");
+        exprt::operandst arguments;
+        // pointer
+        arguments.push_back(address_of_exprt(arg0));
+        // size
+        arguments.push_back(size.value());
+        // is_pointer
+        if(arg0.type().id() == ID_pointer)
+          arguments.push_back(true_exprt());
+        else
+          arguments.push_back(false_exprt());
+
+        expr.arguments().swap(arguments);
+        typecheck_side_effect_function_call(expr);
+      }
       // Is this a builtin?
-      if(!builtin_factory(identifier, symbol_table, get_message_handler()))
+      else if(!builtin_factory(identifier, symbol_table, get_message_handler()))
       {
         // yes, it's a builtin
       }
diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h
index ceec83d14d3..5bd09625ecb 100644
--- a/src/ansi-c/cprover_builtin_headers.h
+++ b/src/ansi-c/cprover_builtin_headers.h
@@ -124,6 +124,11 @@ __CPROVER_bool __CPROVER_overflow_unary_minus();
 __CPROVER_bool __CPROVER_enum_is_in_range();
 
 // contracts
-__CPROVER_size_t __CPROVER_object_from(void *); 
-__CPROVER_size_t __CPROVER_object_slice(void *, __CPROVER_size_t);
+__CPROVER_assignable_t __CPROVER_assignable(
+  void *ptr,
+  __CPROVER_size_t size,
+  __CPROVER_bool is_pointer_to_pointer);
+__CPROVER_assignable_t __CPROVER_whole_object(void *ptr);
+__CPROVER_assignable_t __CPROVER_object_from(void *ptr);
+__CPROVER_assignable_t __CPROVER_object_upto(void *ptr, __CPROVER_size_t size);
 // clang-format on
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
index 16b17990ea8..61bf2687c68 100644
--- a/src/ansi-c/library/cprover.h
+++ b/src/ansi-c/library/cprover.h
@@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 typedef __typeof__(sizeof(int)) __CPROVER_size_t;
 // NOLINTNEXTLINE(readability/identifiers)
 typedef signed long long __CPROVER_ssize_t;
+// NOLINTNEXTLINE(readability/identifiers)
+typedef void __CPROVER_assignable_t;
 
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 void __CPROVER_deallocate(void *);
diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp
index 26e93618a67..dcafb8bc701 100644
--- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp
+++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp
@@ -517,7 +517,7 @@ car_exprt instrument_spec_assignst::create_car_expr(
           upper_bound_var,
           car_havoc_methodt::HAVOC_SLICE};
       }
-      if(ident == CPROVER_PREFIX "object_slice")
+      else if(ident == CPROVER_PREFIX "object_upto")
       {
         const auto &ptr = funcall.arguments().at(0);
         const auto &size = funcall.arguments().at(1);
@@ -531,6 +531,44 @@ car_exprt instrument_spec_assignst::create_car_expr(
           upper_bound_var,
           car_havoc_methodt::HAVOC_SLICE};
       }
+      else if(ident == CPROVER_PREFIX "whole_object")
+      {
+        const auto &ptr = funcall.arguments().at(0);
+        return {
+          condition,
+          target,
+          minus_exprt(
+            typecast_exprt::conditional_cast(ptr, pointer_type(char_type())),
+            pointer_offset(ptr)),
+          typecast_exprt::conditional_cast(object_size(ptr), size_type()),
+          valid_var,
+          lower_bound_var,
+          upper_bound_var,
+          car_havoc_methodt::HAVOC_OBJECT};
+      }
+      else if(ident == CPROVER_PREFIX "assignable")
+      {
+        const auto &ptr = funcall.arguments().at(0);
+        const auto &size = funcall.arguments().at(1);
+        const auto &is_ptr_to_ptr = funcall.arguments().at(2);
+        return {
+          condition,
+          target,
+          typecast_exprt::conditional_cast(ptr, pointer_type(char_type())),
+          typecast_exprt::conditional_cast(size, size_type()),
+          valid_var,
+          lower_bound_var,
+          upper_bound_var,
+          is_ptr_to_ptr.is_true() ? car_havoc_methodt::NONDET_ASSIGN
+                                  : car_havoc_methodt::HAVOC_SLICE};
+      }
+      else
+      {
+        log.error().source_location = target.source_location();
+        log.error() << "call to " + id2string(ident) +
+                         " in assigns clauses not supported in "
+                         "this version";
+      }
     }
   }
   else if(is_assignable(target))
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 3bb44a0ec4c..b5441bf7866 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -721,6 +721,101 @@ void goto_convertt::do_havoc_slice(
   dest.add(goto_programt::make_other(array_replace, source_location));
 }
 
+void goto_convertt::do_whole_object(
+  const exprt &lhs,
+  const symbol_exprt &function,
+  const exprt::operandst &arguments,
+  goto_programt &dest,
+  const irep_idt &mode)
+{
+  // We enable overflow checks on pointer and size computation
+  auto source_location = function.find_source_location();
+  source_location.add_pragma("enable:pointer-check");
+  source_location.add_pragma("enable:pointer-overflow-check");
+  source_location.add_pragma("enable:signed-overflow-check");
+  source_location.add_pragma("enable:unsigned-overflow-check");
+  const auto &arg0 = arguments[0];
+
+  // Rewrite to a call to CPROVER_PREFIX "assignable"
+  exprt::operandst new_arguments;
+  // pointer
+  new_arguments.emplace_back(typecast_exprt::conditional_cast(
+    minus_exprt{
+      typecast_exprt::conditional_cast(arg0, pointer_type(char_type())),
+      pointer_offset_exprt{arg0, size_type()}},
+    pointer_type(empty_typet())));
+  // size
+  new_arguments.emplace_back(object_size_exprt{arg0, size_type()});
+  // is_pointer
+  new_arguments.emplace_back(false_exprt());
+
+  const auto &fun =
+    symbol_table.lookup_ref(CPROVER_PREFIX "assignable").symbol_expr();
+  code_function_callt function_call(std::move(fun), std::move(new_arguments));
+
+  dest.add(goto_programt::make_function_call(function_call, source_location));
+}
+
+void goto_convertt::do_object_from(
+  const exprt &lhs,
+  const symbol_exprt &function,
+  const exprt::operandst &arguments,
+  goto_programt &dest,
+  const irep_idt &mode)
+{
+  // We enable overflow checks on pointer and size computation
+  auto source_location = function.find_source_location();
+  source_location.add_pragma("enable:pointer-check");
+  source_location.add_pragma("enable:pointer-overflow-check");
+  source_location.add_pragma("enable:signed-overflow-check");
+  source_location.add_pragma("enable:unsigned-overflow-check");
+  const auto &arg0 = arguments[0];
+
+  // Rewrite to a call to CPROVER_PREFIX "assignable"
+  exprt::operandst new_arguments;
+  // ptr
+  new_arguments.emplace_back(arg0);
+  // size
+  new_arguments.emplace_back(minus_exprt{
+    object_size_exprt{arg0, size_type()},
+    pointer_offset_exprt{arg0, size_type()}});
+  // is_pointer
+  new_arguments.emplace_back(false_exprt());
+
+  const auto &fun =
+    symbol_table.lookup_ref(CPROVER_PREFIX "assignable").symbol_expr();
+  code_function_callt function_call(std::move(fun), std::move(new_arguments));
+
+  dest.add(goto_programt::make_function_call(function_call, source_location));
+}
+
+void goto_convertt::do_object_upto(
+  const exprt &lhs,
+  const symbol_exprt &function,
+  const exprt::operandst &arguments,
+  goto_programt &dest,
+  const irep_idt &mode)
+{
+  // We enable overflow checks on pointer and size computation
+  auto source_location = function.find_source_location();
+  const auto &arg0 = arguments[0];
+  const auto &arg1 = arguments[1];
+
+  // Rewrite to a call to CPROVER_PREFIX "assignable"
+  exprt::operandst new_arguments;
+  // pointer
+  new_arguments.emplace_back(arg0);
+  // size
+  new_arguments.emplace_back(arg1);
+  // is_pointer
+  new_arguments.emplace_back(false_exprt());
+  const auto &fun =
+    symbol_table.lookup_ref(CPROVER_PREFIX "assignable").symbol_expr();
+  code_function_callt function_call(std::move(fun), std::move(new_arguments));
+
+  dest.add(goto_programt::make_function_call(function_call, source_location));
+}
+
 /// add function calls to function queue for later processing
 void goto_convertt::do_function_call_symbol(
   const exprt &lhs,
@@ -767,7 +862,19 @@ void goto_convertt::do_function_call_symbol(
     return;
   }
 
-  if(identifier == CPROVER_PREFIX "havoc_slice")
+  if(identifier == CPROVER_PREFIX "object_from")
+  {
+    do_object_from(lhs, function, arguments, dest, mode);
+  }
+  else if(identifier == CPROVER_PREFIX "object_upto")
+  {
+    do_object_upto(lhs, function, arguments, dest, mode);
+  }
+  else if(identifier == CPROVER_PREFIX "whole_object")
+  {
+    do_whole_object(lhs, function, arguments, dest, mode);
+  }
+  else if(identifier == CPROVER_PREFIX "havoc_slice")
   {
     do_havoc_slice(lhs, function, arguments, dest, mode);
   }
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index 61317628b7f..daee847fdd8 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -679,6 +679,24 @@ class goto_convertt:public messaget
     const exprt::operandst &arguments,
     goto_programt &dest,
     const irep_idt &mode);
+  void do_whole_object(
+    const exprt &lhs,
+    const symbol_exprt &function,
+    const exprt::operandst &arguments,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void do_object_upto(
+    const exprt &lhs,
+    const symbol_exprt &function,
+    const exprt::operandst &arguments,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void do_object_from(
+    const exprt &lhs,
+    const symbol_exprt &function,
+    const exprt::operandst &arguments,
+    goto_programt &dest,
+    const irep_idt &mode);
 
   exprt get_array_argument(const exprt &src);
 };