From 14cfdbf1d83e677be79698e38407a7303da4c369 Mon Sep 17 00:00:00 2001
From: Remi Delmas <delmasrd@amazon.com>
Date: Mon, 22 Aug 2022 14:40:47 -0400
Subject: [PATCH 1/2] CONTRACTS: Front-end extensions for assigns clauses and
 frees clauses.

Add new functions to specify assignable
targets in assigns clauses:
- add type __CPROVER_assignable_t
- add builtin __CPROVER_assignable
- add builtin __CPROVER_whole_object
- add builtin __CPROVER_object_upto
- add builtin __CPROVER_typed_target
- allow function call expressions as assigns
  clause targets as long as they have the
  return type __CPROVER_assignable_t and
  are one of the built-ins.

Add support for `__CPROVER_frees()` clauses
to the contract language to let users specify
the pointers a function (or loop) is allowed
to free.
---
 doc/cprover-manual/contracts-assigns.md       |  46 ++++--
 doc/cprover-manual/contracts-frees.md         |  80 ++++++++++
 .../assigns-slice-targets/main-enforce.c      |  22 ++-
 .../assigns-slice-targets/main-replace.c      |  62 +++++++-
 .../assigns-slice-targets/test-enforce.desc   |  10 +-
 .../assigns-slice-targets/test-replace.desc   |  23 +++
 .../assigns_enforce_address_of/test.desc      |   2 +-
 .../test.desc                                 |   2 +-
 .../test.desc                                 |   2 +-
 .../assigns_enforce_function_calls/test.desc  |   2 +-
 .../assigns_enforce_literal/test.desc         |   2 +-
 .../assigns_enforce_side_effects_2/test.desc  |   2 +-
 .../assigns_enforce_side_effects_3/test.desc  |   2 +-
 .../test.desc                                 |   2 +-
 .../contracts/cprover-assignable-fail/main.c  |  29 ++++
 .../cprover-assignable-fail/test.desc         |  20 +++
 .../contracts/cprover-assignable-pass/main.c  |  25 +++
 .../cprover-assignable-pass/test.desc         |  20 +++
 .../frees-clause-for-loop-fail/main.c         |  19 +++
 .../frees-clause-for-loop-fail/test.desc      |  10 ++
 .../frees-clause-for-loop-pass/main.c         |  19 +++
 .../frees-clause-for-loop-pass/test.desc      |   9 ++
 .../frees-clause-function-fail/main.c         |  19 +++
 .../frees-clause-function-fail/test.desc      |  10 ++
 .../frees-clause-function-pass/main.c         |  20 +++
 .../frees-clause-function-pass/test.desc      |   9 ++
 .../frees-clause-while-loop-fail/main.c       |  20 +++
 .../frees-clause-while-loop-fail/test.desc    |  10 ++
 .../frees-clause-while-loop-pass/main.c       |  20 +++
 .../frees-clause-while-loop-pass/test.desc    |   9 ++
 src/ansi-c/ansi_c_convert_type.cpp            |  11 ++
 src/ansi-c/ansi_c_convert_type.h              |   2 +-
 src/ansi-c/ansi_c_internal_additions.cpp      |  15 ++
 src/ansi-c/c_typecheck_base.cpp               |  29 ++++
 src/ansi-c/c_typecheck_base.h                 |   9 +-
 src/ansi-c/c_typecheck_code.cpp               | 143 ++++++++++++------
 src/ansi-c/c_typecheck_expr.cpp               |  52 ++++++-
 src/ansi-c/cprover_builtin_headers.h          |   7 +-
 src/ansi-c/library/cprover.h                  |   2 +
 src/ansi-c/parser.y                           |  59 ++++++--
 src/ansi-c/scanner.l                          |   1 +
 .../contracts/instrument_spec_assigns.cpp     |  40 ++++-
 src/goto-programs/goto_convert.cpp            |   7 +
 src/linking/remove_internal_symbols.cpp       |   5 +
 src/util/c_types.h                            |  12 +-
 src/util/irep_ids.def                         |   1 +
 src/util/rename_symbol.cpp                    |   8 +
 src/util/replace_symbol.cpp                   |   5 +
 48 files changed, 840 insertions(+), 95 deletions(-)
 create mode 100644 doc/cprover-manual/contracts-frees.md
 create mode 100644 regression/contracts/cprover-assignable-fail/main.c
 create mode 100644 regression/contracts/cprover-assignable-fail/test.desc
 create mode 100644 regression/contracts/cprover-assignable-pass/main.c
 create mode 100644 regression/contracts/cprover-assignable-pass/test.desc
 create mode 100644 regression/contracts/frees-clause-for-loop-fail/main.c
 create mode 100644 regression/contracts/frees-clause-for-loop-fail/test.desc
 create mode 100644 regression/contracts/frees-clause-for-loop-pass/main.c
 create mode 100644 regression/contracts/frees-clause-for-loop-pass/test.desc
 create mode 100644 regression/contracts/frees-clause-function-fail/main.c
 create mode 100644 regression/contracts/frees-clause-function-fail/test.desc
 create mode 100644 regression/contracts/frees-clause-function-pass/main.c
 create mode 100644 regression/contracts/frees-clause-function-pass/test.desc
 create mode 100644 regression/contracts/frees-clause-while-loop-fail/main.c
 create mode 100644 regression/contracts/frees-clause-while-loop-fail/test.desc
 create mode 100644 regression/contracts/frees-clause-while-loop-pass/main.c
 create mode 100644 regression/contracts/frees-clause-while-loop-pass/test.desc

diff --git a/doc/cprover-manual/contracts-assigns.md b/doc/cprover-manual/contracts-assigns.md
index 3c9a3048cc8..bbafa46e1c0 100644
--- a/doc/cprover-manual/contracts-assigns.md
+++ b/doc/cprover-manual/contracts-assigns.md
@@ -17,28 +17,46 @@ value(s) therein are not modified.
 
 ### Object slice expressions
 
-The following functions can be used in assigns clause to specify ranges of 
-assignable addresses.
+The following functions can be used in assigns clauses to specify ranges of assignable bytes.
 
-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:
+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_size_t __CPROVER_object_from(void *ptr); 
+__CPROVER_assignable_t __CPROVER_typed_target(expr_t expr);
 ```
 
-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_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 the range of bytes starting from the pointer and until the end of
+the object `o` are assignable:
 ```c
-__CPROVER_size_t __CPROVER_object_slice(void *ptr, __CPROVER_size_t size);
+__CPROVER_assignable_t __CPROVER_object_from(void *ptr);
 ```
 
-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. 
+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_assignable_t __CPROVER_object_upto(void *ptr, __CPROVER_size_t size);
+```
+
+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/doc/cprover-manual/contracts-frees.md b/doc/cprover-manual/contracts-frees.md
new file mode 100644
index 00000000000..7b8134ce5c8
--- /dev/null
+++ b/doc/cprover-manual/contracts-frees.md
@@ -0,0 +1,80 @@
+[CPROVER Manual TOC](../../)
+
+# Frees Clause
+
+### Syntax
+
+```c
+__CPROVER_frees(*pointer-typed-expression*, ...)
+```
+
+A _frees_ clause allows the user to specify a set of pointers that may be freed
+by a function or the body of a loop.
+A function or loop contract contract may have zero or more _frees_ clauses.
+
+_Frees_ clause targets must be pointer-typed expressions.
+
+_Frees_ clause targets can also be _conditional_ and written as follows:
+
+```
+condition: list-of-pointer-typed-expressions;
+```
+
+### Examples
+
+In a function contract
+```c
+int foo(char *arr1, char *arr2, size_t size)
+__CPROVER_frees(
+    // arr1 freeable only if the condition holds
+    size > 0 && arr1: arr1;
+    // arr2 always freeable
+    arr2
+)
+{
+  if(size > 0 && arr1)
+    free(arr1);
+  free(arr2);
+  return 0;
+}
+```
+
+In a loop contract:
+
+```c
+int main()
+{
+  size_t size = 10;
+  char *arr = malloc(size);
+
+  for(size_t i = 0; i <= size; i++)
+    // clang-format off
+  __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(arr))
+  __CPROVER_frees(arr)
+    // clang-format on2
+    {
+      if(i < size)
+        arr[i] = 0;
+      else
+        free(arr);
+    }
+  return 0;
+}
+```
+
+### Semantics
+
+The set of pointers specified by the frees clause of the contract is interpreted
+at the function call-site for function contracts, and right before entering the
+loop for loop contracts.
+
+#### For contract checking
+When checking a contract against a function or a loop, each pointer that the
+function or loop body attempts to free gets checked for membership in the set of
+pointers specified by the contract.
+
+#### For replacement of function calls or loops by contracts
+When replacing a function call or a loop by a contract, each pointer of the
+_frees_ clause is non-deterministically freed after the function call
+or after the loop.
+
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..9db72b0af93
--- /dev/null
+++ b/regression/contracts/cprover-assignable-fail/main.c
@@ -0,0 +1,29 @@
+#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;
+  }
+  // pointer can be invalid expecting failed checks
+  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..0550c09fb40
--- /dev/null
+++ b/regression/contracts/cprover-assignable-fail/test.desc
@@ -0,0 +1,20 @@
+CORE
+main.c
+
+CALL __CPROVER_whole_object
+CALL __CPROVER_object_upto
+CALL __CPROVER_object_from
+CALL __CPROVER_assignable
+^\[my_write_set.assertion.\d+\] .* target null or writable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+CALL __CPROVER_typed_target
+--
+This test checks that:
+- built-in __CPROVER_assignable_t functions are supported;
+- GOTO conversion preserves calls to __CPROVER_whole_object,
+  __CPROVER_object_upto, __CPROVER_object_from;
+- GOTO conversion translates __CPROVER_typed_target to __CPROVER_assignable;
+- user-defined checks embedded in `my_write_set` persist after conversion.
diff --git a/regression/contracts/cprover-assignable-pass/main.c b/regression/contracts/cprover-assignable-pass/main.c
new file mode 100644
index 00000000000..bbeb08acc03
--- /dev/null
+++ b/regression/contracts/cprover-assignable-pass/main.c
@@ -0,0 +1,25 @@
+#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;
+  // pointer is not invalid
+  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..ee96e43352f
--- /dev/null
+++ b/regression/contracts/cprover-assignable-pass/test.desc
@@ -0,0 +1,20 @@
+CORE
+main.c
+
+CALL __CPROVER_whole_object
+CALL __CPROVER_object_upto
+CALL __CPROVER_object_from
+CALL __CPROVER_assignable
+^\[my_write_set.assertion.\d+\] .* target null or writable: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+CALL __CPROVER_typed_target
+--
+This test checks that:
+- built-in __CPROVER_assignable_t functions are supported;
+- GOTO conversion preserves calls to __CPROVER_whole_object,
+  __CPROVER_object_upto, __CPROVER_object_from;
+- GOTO conversion translates __CPROVER_typed_target to __CPROVER_assignable;
+- user-defined checks embedded in `my_write_set` persist after conversion.
diff --git a/regression/contracts/frees-clause-for-loop-fail/main.c b/regression/contracts/frees-clause-for-loop-fail/main.c
new file mode 100644
index 00000000000..587374681e7
--- /dev/null
+++ b/regression/contracts/frees-clause-for-loop-fail/main.c
@@ -0,0 +1,19 @@
+#include <stdlib.h>
+int main()
+{
+  size_t size = 10;
+  char *arr = malloc(size);
+
+  for(size_t i = 0; i <= size; i++)
+    // clang-format off
+  __CPROVER_assigns(i, arr[2], __CPROVER_POINTER_OBJECT(arr))
+  __CPROVER_frees(arr[2])
+    // clang-format on
+    {
+      if(i == 2)
+        arr[i] = 0;
+      if(i == size)
+        free(arr);
+    }
+  return 0;
+}
diff --git a/regression/contracts/frees-clause-for-loop-fail/test.desc b/regression/contracts/frees-clause-for-loop-fail/test.desc
new file mode 100644
index 00000000000..e39b9ce3349
--- /dev/null
+++ b/regression/contracts/frees-clause-for-loop-fail/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c.*: error: frees clause target must be a pointer-typed expression$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test is expected trigger a typchecking error on a frees clause target.
diff --git a/regression/contracts/frees-clause-for-loop-pass/main.c b/regression/contracts/frees-clause-for-loop-pass/main.c
new file mode 100644
index 00000000000..df228091be7
--- /dev/null
+++ b/regression/contracts/frees-clause-for-loop-pass/main.c
@@ -0,0 +1,19 @@
+#include <stdlib.h>
+int main()
+{
+  size_t size = 10;
+  char *arr = malloc(size);
+
+  for(size_t i = 0; i <= size; i++)
+    // clang-format off
+  __CPROVER_assigns(i, arr[2], __CPROVER_POINTER_OBJECT(arr))
+  __CPROVER_frees(arr)
+    // clang-format on
+    {
+      if(i == 2)
+        arr[i] = 0;
+      if(i == size)
+        free(arr);
+    }
+  return 0;
+}
diff --git a/regression/contracts/frees-clause-for-loop-pass/test.desc b/regression/contracts/frees-clause-for-loop-pass/test.desc
new file mode 100644
index 00000000000..85d74473748
--- /dev/null
+++ b/regression/contracts/frees-clause-for-loop-pass/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--apply-loop-contracts
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that frees clauses are parsed and typechecked for for loops.
diff --git a/regression/contracts/frees-clause-function-fail/main.c b/regression/contracts/frees-clause-function-fail/main.c
new file mode 100644
index 00000000000..f25c8e0be67
--- /dev/null
+++ b/regression/contracts/frees-clause-function-fail/main.c
@@ -0,0 +1,19 @@
+#include <stdlib.h>
+
+int foo(char *arr, int size)
+  // clang-format off
+__CPROVER_frees(size)
+// clang-format on
+{
+  // the body does not actually free the array
+  // since we are only testing parsing and typechecking
+  return 0;
+}
+
+int main()
+{
+  size_t size;
+  char *arr = malloc(size);
+  foo(arr, size);
+  return 0;
+}
diff --git a/regression/contracts/frees-clause-function-fail/test.desc b/regression/contracts/frees-clause-function-fail/test.desc
new file mode 100644
index 00000000000..6936f96e1ba
--- /dev/null
+++ b/regression/contracts/frees-clause-function-fail/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c.*: error: frees clause target must be a pointer-typed expression$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test is expected trigger a typchecking error on a frees clause target.
diff --git a/regression/contracts/frees-clause-function-pass/main.c b/regression/contracts/frees-clause-function-pass/main.c
new file mode 100644
index 00000000000..99c5ee2b0e0
--- /dev/null
+++ b/regression/contracts/frees-clause-function-pass/main.c
@@ -0,0 +1,20 @@
+#include <stdlib.h>
+
+int foo(char *arr1, char *arr2, size_t size)
+  // clang-format off
+__CPROVER_frees(size > 0 && arr1: arr1; arr2)
+// clang-format on
+{
+  // the body does not actually free the function
+  // since we are only testing parsing and typechecking
+  return 0;
+}
+
+int main()
+{
+  size_t size;
+  char *arr1 = malloc(size);
+  char *arr2 = malloc(size);
+  foo(arr1, arr2, size);
+  return 0;
+}
diff --git a/regression/contracts/frees-clause-function-pass/test.desc b/regression/contracts/frees-clause-function-pass/test.desc
new file mode 100644
index 00000000000..88f63207658
--- /dev/null
+++ b/regression/contracts/frees-clause-function-pass/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that frees clauses are parsed and typechecked.
diff --git a/regression/contracts/frees-clause-while-loop-fail/main.c b/regression/contracts/frees-clause-while-loop-fail/main.c
new file mode 100644
index 00000000000..e563c13fc5d
--- /dev/null
+++ b/regression/contracts/frees-clause-while-loop-fail/main.c
@@ -0,0 +1,20 @@
+#include <stdlib.h>
+int main()
+{
+  size_t size = 10;
+  char *arr = malloc(size);
+  size_t i = 0;
+  while(i <= size)
+    // clang-format off
+  __CPROVER_assigns(i, arr[2], __CPROVER_POINTER_OBJECT(arr))
+  __CPROVER_frees(arr[2])
+    // clang-format on
+    {
+      if(i == 2)
+        arr[i] = 0;
+      if(i == size)
+        free(arr);
+      i++;
+    }
+  return 0;
+}
diff --git a/regression/contracts/frees-clause-while-loop-fail/test.desc b/regression/contracts/frees-clause-while-loop-fail/test.desc
new file mode 100644
index 00000000000..e39b9ce3349
--- /dev/null
+++ b/regression/contracts/frees-clause-while-loop-fail/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c.*: error: frees clause target must be a pointer-typed expression$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test is expected trigger a typchecking error on a frees clause target.
diff --git a/regression/contracts/frees-clause-while-loop-pass/main.c b/regression/contracts/frees-clause-while-loop-pass/main.c
new file mode 100644
index 00000000000..5a75c5743dc
--- /dev/null
+++ b/regression/contracts/frees-clause-while-loop-pass/main.c
@@ -0,0 +1,20 @@
+#include <stdlib.h>
+int main()
+{
+  size_t size = 10;
+  char *arr = malloc(size);
+  size_t i = 0;
+  while(i <= size)
+    // clang-format off
+  __CPROVER_assigns(i, arr[2], __CPROVER_POINTER_OBJECT(arr))
+  __CPROVER_frees(arr)
+    // clang-format on
+    {
+      if(i == 2)
+        arr[i] = 0;
+      if(i == size)
+        free(arr);
+      i++;
+    }
+  return 0;
+}
diff --git a/regression/contracts/frees-clause-while-loop-pass/test.desc b/regression/contracts/frees-clause-while-loop-pass/test.desc
new file mode 100644
index 00000000000..44420a4a998
--- /dev/null
+++ b/regression/contracts/frees-clause-while-loop-pass/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--apply-loop-contracts
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that frees clauses are parsed and typechecked for while loops.
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index 425d30113f3..a4e195888ef 100644
--- a/src/ansi-c/ansi_c_convert_type.cpp
+++ b/src/ansi-c/ansi_c_convert_type.cpp
@@ -273,6 +273,14 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     for(const exprt &target : to_unary_expr(as_expr).op().operands())
       assigns.push_back(target);
   }
+  else if(type.id() == ID_C_spec_frees)
+  {
+    const exprt &as_expr =
+      static_cast<const exprt &>(static_cast<const irept &>(type));
+
+    for(const exprt &target : to_unary_expr(as_expr).op().operands())
+      frees.push_back(target);
+  }
   else if(type.id() == ID_C_spec_ensures)
   {
     const exprt &as_expr =
@@ -341,6 +349,9 @@ void ansi_c_convert_typet::write(typet &type)
     if(!assigns.empty())
       to_code_with_contract_type(type).assigns() = std::move(assigns);
 
+    if(!frees.empty())
+      to_code_with_contract_type(type).frees() = std::move(frees);
+
     if(!ensures.empty())
       to_code_with_contract_type(type).ensures() = std::move(ensures);
 
diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h
index 83f65ffe3ff..1eabc279006 100644
--- a/src/ansi-c/ansi_c_convert_type.h
+++ b/src/ansi-c/ansi_c_convert_type.h
@@ -47,7 +47,7 @@ class ansi_c_convert_typet:public messaget
   bool constructor, destructor;
 
   // contracts
-  exprt::operandst assigns, ensures, requires, ensures_contract,
+  exprt::operandst assigns, frees, ensures, requires, ensures_contract,
     requires_contract;
 
   // storage spec
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 6ea08fb5b44..b9952f9a4d2 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -216,6 +216,21 @@ 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_ptr_to_ptr);\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
 
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 287c9f0e13f..b392f92ec0c 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -777,6 +777,24 @@ void c_typecheck_baset::typecheck_declaration(
           CPROVER_PREFIX "loop_entry is not allowed in preconditions.");
       };
 
+      auto check_return_value = [&](const exprt &expr) {
+        const irep_idt id = CPROVER_PREFIX "return_value";
+
+        auto pred = [&](const exprt &expr) {
+          if(!can_cast_expr<symbol_exprt>(expr))
+            return false;
+
+          return to_symbol_expr(expr).get_identifier() == id;
+        };
+
+        if(!has_subexpr(expr, pred))
+          return;
+
+        error().source_location = expr.source_location();
+        error() << id2string(id) + "is not allowed in preconditions." << eom;
+        throw 0;
+      };
+
       // check the contract, if any
       symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
       if(
@@ -833,6 +851,8 @@ void c_typecheck_baset::typecheck_declaration(
           typecheck_expr(requires);
           implicit_typecast_bool(requires);
           check_history_expr(requires);
+          check_return_value(requires);
+          check_return_value(requires);
           lambda_exprt lambda{temporary_parameter_symbols, requires};
           lambda.add_source_location() = requires.source_location();
           requires.swap(lambda);
@@ -846,6 +866,14 @@ void c_typecheck_baset::typecheck_declaration(
           assigns.swap(lambda);
         }
 
+        typecheck_spec_frees(code_type.frees());
+        for(auto &frees : code_type.frees())
+        {
+          lambda_exprt lambda{temporary_parameter_symbols, frees};
+          lambda.add_source_location() = frees.source_location();
+          frees.swap(lambda);
+        }
+
         for(auto &expr : code_type.ensures_contract())
         {
           typecheck_spec_function_pointer_obeys_contract(expr);
@@ -898,6 +926,7 @@ void c_typecheck_baset::typecheck_declaration(
         // Remove the contract from the original symbol as we have created a
         // dedicated contract symbol.
         new_symbol.type.remove(ID_C_spec_assigns);
+        new_symbol.type.remove(ID_C_spec_frees);
         new_symbol.type.remove(ID_C_spec_ensures);
         new_symbol.type.remove(ID_C_spec_ensures_contract);
         new_symbol.type.remove(ID_C_spec_requires);
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index 10dbb1f8196..f9080af5eb8 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -148,10 +148,17 @@ class c_typecheck_baset:
   // contracts
   virtual void typecheck_spec_function_pointer_obeys_contract(exprt &expr);
   virtual void typecheck_spec_assigns(exprt::operandst &targets);
-  virtual void typecheck_spec_assigns_condition(exprt &condition);
+  virtual void typecheck_spec_frees(exprt::operandst &targets);
+  virtual void typecheck_conditional_targets(
+    exprt::operandst &targets,
+    const std::function<void(exprt &)> typecheck_target,
+    const std::string &clause_type);
+  virtual void typecheck_spec_condition(exprt &condition);
   virtual void typecheck_spec_assigns_target(exprt &target);
+  virtual void typecheck_spec_frees_target(exprt &target);
   virtual void typecheck_spec_loop_invariant(codet &code);
   virtual void typecheck_spec_decreases(codet &code);
+  virtual void throw_on_side_effects(const exprt &expr);
 
   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 e2924c811d3..3855121db88 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -505,6 +505,12 @@ void c_typecheck_baset::typecheck_for(codet &code)
     typecheck_spec_assigns(
       static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
   }
+
+  if(code.find(ID_C_spec_frees).is_not_nil())
+  {
+    typecheck_spec_frees(
+      static_cast<unary_exprt &>(code.add(ID_C_spec_frees)).op().operands());
+  }
 }
 
 void c_typecheck_baset::typecheck_label(code_labelt &code)
@@ -805,6 +811,12 @@ void c_typecheck_baset::typecheck_while(code_whilet &code)
     typecheck_spec_assigns(
       static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
   }
+
+  if(code.find(ID_C_spec_frees).is_not_nil())
+  {
+    typecheck_spec_frees(
+      static_cast<unary_exprt &>(code.add(ID_C_spec_frees)).op().operands());
+  }
 }
 
 void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
@@ -845,9 +857,15 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
     typecheck_spec_assigns(
       static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
   }
+
+  if(code.find(ID_C_spec_frees).is_not_nil())
+  {
+    typecheck_spec_frees(
+      static_cast<unary_exprt &>(code.add(ID_C_spec_frees)).op().operands());
+  }
 }
 
-void c_typecheck_baset::typecheck_spec_assigns_condition(exprt &condition)
+void c_typecheck_baset::typecheck_spec_condition(exprt &condition)
 {
   // compute type
   typecheck_expr(condition);
@@ -903,13 +921,36 @@ void c_typecheck_baset::typecheck_spec_assigns_condition(exprt &condition)
     throw 0;
 }
 
+void c_typecheck_baset::throw_on_side_effects(const exprt &expr)
+{
+  if(has_subexpr(expr, ID_side_effect))
+  {
+    error().source_location = expr.source_location();
+    error() << "side-effects not allowed in assigns clause targets"
+            << messaget::eom;
+    throw 0;
+  }
+  if(has_subexpr(expr, ID_if))
+  {
+    error().source_location = expr.source_location();
+    error() << "ternary expressions not allowed in assigns "
+               "clause targets"
+            << messaget::eom;
+    throw 0;
+  }
+}
+
 void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target)
 {
   // compute type
   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"
@@ -917,25 +958,6 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target)
     throw 0;
   }
 
-  // throws exception if expr contains side effect or ternary expr
-  auto throw_on_side_effects = [&](const exprt &expr) {
-    if(has_subexpr(expr, ID_side_effect))
-    {
-      error().source_location = expr.source_location();
-      error() << "side-effects not allowed in assigns clause targets"
-              << messaget::eom;
-      throw 0;
-    }
-    if(has_subexpr(expr, ID_if))
-    {
-      error().source_location = expr.source_location();
-      error() << "ternary expressions not allowed in assigns "
-                 "clause targets"
-              << messaget::eom;
-      throw 0;
-    }
-  };
-
   if(target.get_bool(ID_C_lvalue))
   {
     throw_on_side_effects(target);
@@ -950,37 +972,53 @@ 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;
+  }
+}
+
+void c_typecheck_baset::typecheck_spec_frees_target(exprt &target)
+{
+  // compute type
+  typecheck_expr(target);
+  const auto &type = target.type();
+
+  if(can_cast_type<pointer_typet>(type))
+  {
+    // an expression with pointer-type without side effects
+    throw_on_side_effects(target);
+  }
+  else
+  {
+    // anything else is rejected
+    error().source_location = target.source_location();
+    error() << "frees clause target must be a pointer-typed expression" << eom;
     throw 0;
   }
 }
@@ -1067,7 +1105,10 @@ void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract(
   }
 }
 
-void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
+void c_typecheck_baset::typecheck_conditional_targets(
+  exprt::operandst &targets,
+  const std::function<void(exprt &)> typecheck_target,
+  const std::string &clause_type)
 {
   exprt::operandst tmp;
   bool must_throw = false;
@@ -1078,8 +1119,8 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
     {
       must_throw = true;
       error().source_location = target.source_location();
-      error() << "expected ID_conditional_target_group expression in assigns "
-                 "clause, found "
+      error() << "expected ID_conditional_target_group expression in " +
+                   clause_type + "clause, found "
               << id2string(target.id()) << eom;
     }
 
@@ -1088,7 +1129,7 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
 
     // typecheck condition
     auto &condition = conditional_target_group.condition();
-    typecheck_spec_assigns_condition(condition);
+    typecheck_spec_condition(condition);
 
     if(condition.is_true())
     {
@@ -1096,7 +1137,7 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
       // simplify expr and expose the bare expressions
       for(auto &actual_target : conditional_target_group.targets())
       {
-        typecheck_spec_assigns_target(actual_target);
+        typecheck_target(actual_target);
         tmp.push_back(actual_target);
       }
     }
@@ -1105,7 +1146,7 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
       // if the condition is not trivially true, typecheck in place
       for(auto &actual_target : conditional_target_group.targets())
       {
-        typecheck_spec_assigns_target(actual_target);
+        typecheck_target(actual_target);
       }
       tmp.push_back(std::move(target));
     }
@@ -1123,6 +1164,22 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
   std::swap(targets, tmp);
 }
 
+void c_typecheck_baset::typecheck_spec_frees(exprt::operandst &targets)
+{
+  const std::function<void(exprt &)> typecheck_target = [&](exprt &target) {
+    typecheck_spec_frees_target(target);
+  };
+  typecheck_conditional_targets(targets, typecheck_target, "frees");
+}
+
+void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
+{
+  const std::function<void(exprt &)> typecheck_target = [&](exprt &target) {
+    typecheck_spec_assigns_target(target);
+  };
+  typecheck_conditional_targets(targets, typecheck_target, "assigns");
+}
+
 void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
 {
   if(code.find(ID_C_spec_loop_invariant).is_not_nil())
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 09575c40c5c..1e08f893e1b 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -492,7 +492,9 @@ 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)
+  else if(
+    expr.id() == ID_C_spec_assigns || expr.id() == ID_C_spec_frees ||
+    expr.id() == ID_target_list)
   {
     // already type checked
   }
@@ -1943,8 +1945,54 @@ 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 typed_target function ?
+      if(identifier == CPROVER_PREFIX "typed_target")
+      {
+        if(expr.arguments().size() != 1)
+        {
+          error().source_location = f_op.source_location();
+          error() << "expected 1 argument for " << CPROVER_PREFIX "typed_target"
+                  << " found " << expr.arguments().size() << eom;
+          throw 0;
+        }
+
+        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..a8a4d8fe29e 100644
--- a/src/ansi-c/cprover_builtin_headers.h
+++ b/src/ansi-c/cprover_builtin_headers.h
@@ -124,6 +124,9 @@ __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_ptr_to_ptr);
+__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/ansi-c/parser.y b/src/ansi-c/parser.y
index 9941c9e7184..2ad2ee3581b 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -209,6 +209,7 @@ extern char *yyansi_ctext;
 %token TOK_CPROVER_ENSURES_CONTRACT "__CPROVER_ensures_contract"
 %token TOK_CPROVER_ENSURES  "__CPROVER_ensures"
 %token TOK_CPROVER_ASSIGNS "__CPROVER_assigns"
+%token TOK_CPROVER_FREES "__CPROVER_frees"
 %token TOK_IMPLIES     "==>"
 %token TOK_EQUIVALENT  "<==>"
 %token TOK_XORXOR      "^^"
@@ -2447,26 +2448,31 @@ declaration_or_expression_statement:
 iteration_statement:
         TOK_WHILE '(' comma_expression_opt ')'
           cprover_contract_assigns_opt
-          cprover_contract_loop_invariant_list_opt 
+          cprover_contract_frees_opt
+          cprover_contract_loop_invariant_list_opt
           cprover_contract_decreases_opt
           statement
         {
           $$=$1;
           statement($$, ID_while);
-          parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($8)));
+          parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($9)));
 
           if(!parser_stack($5).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($5).operands());
 
           if(!parser_stack($6).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands());
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_frees)).operands().swap(parser_stack($6).operands());
 
           if(!parser_stack($7).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($7).operands());
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($7).operands());
+
+          if(!parser_stack($8).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($8).operands());
         }
         | TOK_DO statement TOK_WHILE '(' comma_expression ')'
           cprover_contract_assigns_opt
-          cprover_contract_loop_invariant_list_opt 
+          cprover_contract_frees_opt
+          cprover_contract_loop_invariant_list_opt
           cprover_contract_decreases_opt ';'
         {
           $$=$1;
@@ -2477,10 +2483,13 @@ iteration_statement:
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($7).operands());
 
           if(!parser_stack($8).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands());
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_frees)).operands().swap(parser_stack($8).operands());
 
           if(!parser_stack($9).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($9).operands());
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($9).operands());
+
+          if(!parser_stack($10).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($10).operands());
         }
         | TOK_FOR
           {
@@ -2495,7 +2504,8 @@ iteration_statement:
               comma_expression_opt ';'
               comma_expression_opt ')'
               cprover_contract_assigns_opt
-              cprover_contract_loop_invariant_list_opt 
+              cprover_contract_frees_opt
+              cprover_contract_loop_invariant_list_opt
               cprover_contract_decreases_opt
           statement
         {
@@ -2505,16 +2515,19 @@ iteration_statement:
           mto($$, $4);
           mto($$, $5);
           mto($$, $7);
-          mto($$, $12);
+          mto($$, $13);
 
           if(!parser_stack($9).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($9).operands());
 
           if(!parser_stack($10).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($10).operands());
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_frees)).operands().swap(parser_stack($10).operands());
 
           if(!parser_stack($11).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($11).operands());
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($11).operands());
+
+          if(!parser_stack($12).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($12).operands());
 
           if(PARSER.for_has_scope)
             PARSER.pop_scope(); // remove the C99 for-scope
@@ -3317,6 +3330,7 @@ cprover_function_contract:
           parser_stack($$).add_to_operands(std::move(tmp));
         }
         | cprover_contract_assigns
+        | cprover_contract_frees
         ;
 
 unary_expression_list:
@@ -3370,7 +3384,7 @@ conditional_target_list_opt_semicol:
         }
         | conditional_target_list
         {
-          $$ = $1;          
+          $$ = $1;
         }
 
 cprover_contract_assigns:
@@ -3394,6 +3408,27 @@ cprover_contract_assigns_opt:
         | cprover_contract_assigns
         ;
 
+cprover_contract_frees:
+         TOK_CPROVER_FREES '(' conditional_target_list_opt_semicol ')'
+        {
+          $$=$1;
+          set($$, ID_C_spec_frees);
+          mto($$, $3);
+        }
+        | TOK_CPROVER_FREES '(' ')'
+        {
+          $$=$1;
+          set($$, ID_C_spec_frees);
+          parser_stack($$).add_to_operands(exprt(ID_target_list));
+        }
+        ;
+
+cprover_contract_frees_opt:
+        /* nothing */
+        { init($$); parser_stack($$).make_nil(); }
+        | cprover_contract_frees
+        ;
+
 cprover_function_contract_sequence:
           cprover_function_contract
         | cprover_function_contract_sequence cprover_function_contract
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index 210e6866dac..05faae82d62 100644
--- a/src/ansi-c/scanner.l
+++ b/src/ansi-c/scanner.l
@@ -1292,6 +1292,7 @@ __decltype          { if(PARSER.cpp98 &&
 {CPROVER_PREFIX}"requires"     { loc(); return TOK_CPROVER_REQUIRES; }
 {CPROVER_PREFIX}"ensures"      { loc(); return TOK_CPROVER_ENSURES; }
 {CPROVER_PREFIX}"assigns"      { loc(); return TOK_CPROVER_ASSIGNS; }
+{CPROVER_PREFIX}"frees"        { loc(); return TOK_CPROVER_FREES; }
 {CPROVER_PREFIX}"requires_contract" { loc(); return TOK_CPROVER_REQUIRES_CONTRACT; }
 {CPROVER_PREFIX}"ensures_contract" { loc(); return TOK_CPROVER_ENSURES_CONTRACT; }
 
diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp
index f56f4a47d27..0f1956e99d3 100644
--- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp
+++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp
@@ -505,7 +505,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);
@@ -519,6 +519,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/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index f2ffb1df759..460e1bac1b2 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -870,6 +870,13 @@ void goto_convertt::convert_loop_contracts(
     loop->condition_nonconst().add(ID_C_spec_assigns).swap(assigns.op());
   }
 
+  auto frees = static_cast<const unary_exprt &>(code.find(ID_C_spec_frees));
+  if(frees.is_not_nil())
+  {
+    PRECONDITION(loop->is_goto());
+    loop->condition_nonconst().add(ID_C_spec_frees).swap(frees.op());
+  }
+
   auto invariant =
     static_cast<const exprt &>(code.find(ID_C_spec_loop_invariant));
   if(!invariant.is_nil())
diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
index 5563b1b835c..09c3ab4f73c 100644
--- a/src/linking/remove_internal_symbols.cpp
+++ b/src/linking/remove_internal_symbols.cpp
@@ -151,6 +151,11 @@ void remove_internal_symbols(
   special.insert(INITIALIZE_FUNCTION);
   special.insert(CPROVER_PREFIX "deallocated");
   special.insert(CPROVER_PREFIX "dead_object");
+  special.insert(CPROVER_PREFIX "assignable_t");
+  special.insert(CPROVER_PREFIX "assignable");
+  special.insert(CPROVER_PREFIX "object_upto");
+  special.insert(CPROVER_PREFIX "object_from");
+  special.insert(CPROVER_PREFIX "whole_object");
   special.insert(rounding_mode_identifier());
   special.insert("__new");
   special.insert("__new_array");
diff --git a/src/util/c_types.h b/src/util/c_types.h
index e9b922a709f..59afc5885a3 100644
--- a/src/util/c_types.h
+++ b/src/util/c_types.h
@@ -370,7 +370,7 @@ class code_with_contract_typet : public code_typet
   {
     return !ensures().empty() || !ensures_contract().empty() ||
            !requires().empty() || !requires_contract().empty() ||
-           !assigns().empty();
+           !assigns().empty() || !frees().empty();
   }
 
   const exprt::operandst &assigns() const
@@ -383,6 +383,16 @@ class code_with_contract_typet : public code_typet
     return static_cast<exprt &>(add(ID_C_spec_assigns)).operands();
   }
 
+  const exprt::operandst &frees() const
+  {
+    return static_cast<const exprt &>(find(ID_C_spec_frees)).operands();
+  }
+
+  exprt::operandst &frees()
+  {
+    return static_cast<exprt &>(add(ID_C_spec_frees)).operands();
+  }
+
   const exprt::operandst &requires_contract() const
   {
     return static_cast<const exprt &>(find(ID_C_spec_requires_contract))
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 2f2a22bfb5b..b1a4d66eb03 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -577,6 +577,7 @@ IREP_ID_TWO(C_spec_requires, #spec_requires)
 IREP_ID_TWO(C_spec_ensures_contract, #spec_ensures_contract)
 IREP_ID_TWO(C_spec_ensures, #spec_ensures)
 IREP_ID_TWO(C_spec_assigns, #spec_assigns)
+IREP_ID_TWO(C_spec_frees, #spec_frees)
 IREP_ID_ONE(target_list)
 IREP_ID_ONE(conditional_target_group)
 IREP_ID_ONE(function_pointer_obeys_contract)
diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp
index 2c1cfebf36d..fee5550ae11 100644
--- a/src/util/rename_symbol.cpp
+++ b/src/util/rename_symbol.cpp
@@ -171,6 +171,14 @@ bool rename_symbolt::rename(typet &dest) const
       result = false;
     }
 
+    const exprt &spec_frees =
+      static_cast<const exprt &>(dest.find(ID_C_spec_frees));
+    if(spec_frees.is_not_nil() && have_to_rename(spec_frees))
+    {
+      rename(static_cast<exprt &>(dest.add(ID_C_spec_frees)));
+      result = false;
+    }
+
     const exprt &spec_ensures =
       static_cast<const exprt &>(dest.find(ID_C_spec_ensures));
     if(spec_ensures.is_not_nil() && have_to_rename(spec_ensures))
diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp
index 71cc2da13ed..5955eedb80f 100644
--- a/src/util/replace_symbol.cpp
+++ b/src/util/replace_symbol.cpp
@@ -237,6 +237,11 @@ bool replace_symbolt::replace(typet &dest) const
     if(spec_assigns.is_not_nil() && have_to_replace(spec_assigns))
       result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_assigns)));
 
+    const exprt &spec_frees =
+      static_cast<const exprt &>(dest.find(ID_C_spec_frees));
+    if(spec_frees.is_not_nil() && have_to_replace(spec_frees))
+      result &= replace(static_cast<exprt &>(dest.add(ID_C_spec_frees)));
+
     const exprt &spec_ensures =
       static_cast<const exprt &>(dest.find(ID_C_spec_ensures));
     if(spec_ensures.is_not_nil() && have_to_replace(spec_ensures))

From eeb0728e32bf9da9eb5e7331be5b81ba3084d9f7 Mon Sep 17 00:00:00 2001
From: Remi Delmas <delmasrd@amazon.com>
Date: Thu, 25 Aug 2022 18:13:12 -0400
Subject: [PATCH 2/2] CONTRACTS: Front-end: frees clause improvements

Add the following to the front-end:
- add `__CPROVER_freeable_t` built-in type
- add `__CPROVER_freeable` built-in function
- allow calls to `__CPROVER_freeable_t` functions
  in frees clauses
- add `__CPROVER_is_freeable` built-in predicate
- add `__CPROVER_is_freed` built-in predicate

The predicates are not yet supported in the back-end.
---
 doc/cprover-manual/contracts-frees.md         | 56 +++++++++++++++++++
 .../frees-clause-and-predicates-fail/main.c   | 46 +++++++++++++++
 .../test.desc                                 | 10 ++++
 .../frees-clause-and-predicates-fail2/main.c  | 43 ++++++++++++++
 .../test.desc                                 | 11 ++++
 .../frees-clause-and-predicates/main.c        | 44 +++++++++++++++
 .../frees-clause-and-predicates/test.desc     | 17 ++++++
 .../frees-clause-for-loop-fail/test.desc      |  2 +-
 .../frees-clause-function-fail/test.desc      |  2 +-
 .../frees-clause-while-loop-fail/test.desc    |  2 +-
 src/ansi-c/ansi_c_internal_additions.cpp      |  8 +++
 src/ansi-c/c_typecheck_base.cpp               | 22 +++++++-
 src/ansi-c/c_typecheck_code.cpp               | 34 ++++++++++-
 src/ansi-c/c_typecheck_expr.cpp               | 24 ++++++++
 src/ansi-c/cprover_builtin_headers.h          |  3 +
 src/ansi-c/library/cprover.h                  |  2 +
 src/linking/remove_internal_symbols.cpp       |  4 ++
 17 files changed, 324 insertions(+), 6 deletions(-)
 create mode 100644 regression/contracts/frees-clause-and-predicates-fail/main.c
 create mode 100644 regression/contracts/frees-clause-and-predicates-fail/test.desc
 create mode 100644 regression/contracts/frees-clause-and-predicates-fail2/main.c
 create mode 100644 regression/contracts/frees-clause-and-predicates-fail2/test.desc
 create mode 100644 regression/contracts/frees-clause-and-predicates/main.c
 create mode 100644 regression/contracts/frees-clause-and-predicates/test.desc

diff --git a/doc/cprover-manual/contracts-frees.md b/doc/cprover-manual/contracts-frees.md
index 7b8134ce5c8..f9d00c2b502 100644
--- a/doc/cprover-manual/contracts-frees.md
+++ b/doc/cprover-manual/contracts-frees.md
@@ -78,3 +78,59 @@ When replacing a function call or a loop by a contract, each pointer of the
 _frees_ clause is non-deterministically freed after the function call
 or after the loop.
 
+# Using functions to specify parametric sets of freeable pointers
+
+Users can define parametric sets of freeable pointers by writing functions that
+return the built-in type `__CPROVER_freeable_t` and call the built-in function
+`__CPROVER_freeable` or any user-defined function returning
+`__CPROVER_freeable_t`:
+
+```c
+__CPROVER_freeable_t my_freeable_set(char **arr, size_t size)
+{
+  if (arr && size > 3) {
+    __CPROVER_freeable(arr[0]);
+    __CPROVER_freeable(arr[1]);
+    __CPROVER_freeable(arr[2]);
+  }
+}
+```
+
+The built-in function:
+
+```c
+__CPROVER_freeable_t __CPROVER_freeable(void *ptr);
+```
+adds the given pointer to the freeable set described by the enclosing function.
+
+Calls to functions returning `__CPROVER_freeable_t` can then be used as targets
+in `__CPROVER_frees` clauses:
+
+```c
+void my_function(char **arr, size_t size)
+__CPROVER_frees(my_freeable_set(arr, size))
+{
+  ...
+}
+```
+
+# Frees clause related predicates
+
+The predicate:
+
+```c
+__CPROVER_bool __CPROVER_is_freeable(void *ptr);
+```
+can only be used in pre and post conditions, in contract checking or replacement
+modes. It returns `true` if and only if the pointer satisfies the preconditions
+of the `free` function from `stdlib.h`, that is if and only if the pointer
+points to a valid dynamically allocated object and has offset zero.
+
+The predicate:
+
+```c
+__CPROVER_bool __CPROVER_is_freed(void *ptr);
+```
+can only be used in post conditions and returns `true` if and only if the
+pointer was freed during the execution of the function or the loop under
+analysis.
diff --git a/regression/contracts/frees-clause-and-predicates-fail/main.c b/regression/contracts/frees-clause-and-predicates-fail/main.c
new file mode 100644
index 00000000000..7285a551e6d
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates-fail/main.c
@@ -0,0 +1,46 @@
+#include <stdlib.h>
+
+// A function defining a conditionally freeable target
+__CPROVER_freeable_t
+foo_frees(char *arr, const size_t size, const size_t new_size)
+{
+  __CPROVER_freeable(arr);
+}
+
+char *foo(char *arr, const size_t size, const size_t new_size)
+  // clang-format off
+ // error is_freed cannot be used in preconditions
+__CPROVER_requires(!__CPROVER_is_freed(arr))
+__CPROVER_requires(__CPROVER_is_freeable(arr))
+__CPROVER_assigns(__CPROVER_whole_object(arr))
+__CPROVER_frees(foo_frees(arr, size, new_size))
+__CPROVER_ensures(
+  (arr && new_size > size) ==>
+    __CPROVER_is_fresh(__CPROVER_return_value, new_size))
+__CPROVER_ensures(
+  (arr && new_size > size) ==>
+    __CPROVER_is_freed(__CPROVER_old(arr)))
+__CPROVER_ensures(
+    !(arr && new_size > size) ==>
+      __CPROVER_return_value == __CPROVER_old(arr))
+// clang-format on
+{
+  if(arr && new_size > size)
+  {
+    free(arr);
+    return malloc(new_size);
+  }
+  else
+  {
+    return arr;
+  }
+}
+
+int main()
+{
+  size_t size;
+  size_t new_size;
+  char *arr = malloc(size);
+  arr = foo(arr, size, new_size);
+  return 0;
+}
diff --git a/regression/contracts/frees-clause-and-predicates-fail/test.desc b/regression/contracts/frees-clause-and-predicates-fail/test.desc
new file mode 100644
index 00000000000..7c01104d8f6
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates-fail/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c.* error: __CPROVER_is_freed is not allowed in preconditions.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks that the front end rejects __CPROVER_is_freed in preconditions.
diff --git a/regression/contracts/frees-clause-and-predicates-fail2/main.c b/regression/contracts/frees-clause-and-predicates-fail2/main.c
new file mode 100644
index 00000000000..bf23353d665
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates-fail2/main.c
@@ -0,0 +1,43 @@
+#include <stdlib.h>
+
+// A function defining a conditionally freeable target
+void foo_frees(char *arr, const size_t size, const size_t new_size)
+{
+  __CPROVER_freeable(arr);
+}
+
+char *foo(char *arr, const size_t size, const size_t new_size)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_freeable(arr))
+__CPROVER_assigns(__CPROVER_whole_object(arr))
+__CPROVER_frees(foo_frees(arr, size, new_size))
+__CPROVER_ensures(
+  (arr && new_size > size) ==>
+    __CPROVER_is_fresh(__CPROVER_return_value, new_size))
+__CPROVER_ensures(
+  (arr && new_size > size) ==>
+    __CPROVER_is_freed(__CPROVER_old(arr)))
+__CPROVER_ensures(
+    !(arr && new_size > size) ==>
+      __CPROVER_return_value == __CPROVER_old(arr))
+// clang-format on
+{
+  if(arr && new_size > size)
+  {
+    free(arr);
+    return malloc(new_size);
+  }
+  else
+  {
+    return arr;
+  }
+}
+
+int main()
+{
+  size_t size;
+  size_t new_size;
+  char *arr = malloc(size);
+  arr = foo(arr, size, new_size);
+  return 0;
+}
diff --git a/regression/contracts/frees-clause-and-predicates-fail2/test.desc b/regression/contracts/frees-clause-and-predicates-fail2/test.desc
new file mode 100644
index 00000000000..57230e0a51c
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates-fail2/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c.* error: expecting __CPROVER_freeable_t return type for function foo_frees called in frees clause$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks that the front-end rejects non-__CPROVER_freeable_t-typed
+function calls in frees clauses.
diff --git a/regression/contracts/frees-clause-and-predicates/main.c b/regression/contracts/frees-clause-and-predicates/main.c
new file mode 100644
index 00000000000..71a1b84771d
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates/main.c
@@ -0,0 +1,44 @@
+#include <stdlib.h>
+
+// A function defining a conditionally freeable target
+__CPROVER_freeable_t
+foo_frees(char *arr, const size_t size, const size_t new_size)
+{
+  __CPROVER_freeable(arr);
+}
+
+char *foo(char *arr, const size_t size, const size_t new_size)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_freeable(arr))
+__CPROVER_assigns(__CPROVER_whole_object(arr))
+__CPROVER_frees(foo_frees(arr, size, new_size))
+__CPROVER_ensures(
+  (arr && new_size > size) ==>
+    __CPROVER_is_fresh(__CPROVER_return_value, new_size))
+__CPROVER_ensures(
+  (arr && new_size > size) ==>
+    __CPROVER_is_freed(__CPROVER_old(arr)))
+__CPROVER_ensures(
+    !(arr && new_size > size) ==>
+      __CPROVER_return_value == __CPROVER_old(arr))
+// clang-format on
+{
+  if(arr && new_size > size)
+  {
+    free(arr);
+    return malloc(new_size);
+  }
+  else
+  {
+    return arr;
+  }
+}
+
+int main()
+{
+  size_t size;
+  size_t new_size;
+  char *arr = malloc(size);
+  arr = foo(arr, size, new_size);
+  return 0;
+}
diff --git a/regression/contracts/frees-clause-and-predicates/test.desc b/regression/contracts/frees-clause-and-predicates/test.desc
new file mode 100644
index 00000000000..770c3f319e6
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-contract foo
+^\[foo.postcondition.\d+\] line \d+ Check ensures clause: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test checks that the front end parses and typchecks correct uses of:
+- __CPROVER_freeable_t function calls as frees clause targets
+- the predicate __CPROVER_freeable
+- the predicate __CPROVER_is_freeable
+- the predicate __CPROVER_is_freed
+
+The post condition of the contract is expected to fail because the predicates
+have no interpretation in the back-end yet.
diff --git a/regression/contracts/frees-clause-for-loop-fail/test.desc b/regression/contracts/frees-clause-for-loop-fail/test.desc
index e39b9ce3349..e2d39e5a965 100644
--- a/regression/contracts/frees-clause-for-loop-fail/test.desc
+++ b/regression/contracts/frees-clause-for-loop-fail/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --apply-loop-contracts
-^main.c.*: error: frees clause target must be a pointer-typed expression$
+^main.c.* error: frees clause target must be a pointer-typed expression or a call to a function returning __CPROVER_freeable_t$
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/contracts/frees-clause-function-fail/test.desc b/regression/contracts/frees-clause-function-fail/test.desc
index 6936f96e1ba..8c217f0a311 100644
--- a/regression/contracts/frees-clause-function-fail/test.desc
+++ b/regression/contracts/frees-clause-function-fail/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^main.c.*: error: frees clause target must be a pointer-typed expression$
+^main.c.* error: frees clause target must be a pointer-typed expression or a call to a function returning __CPROVER_freeable_t$
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/regression/contracts/frees-clause-while-loop-fail/test.desc b/regression/contracts/frees-clause-while-loop-fail/test.desc
index e39b9ce3349..e2d39e5a965 100644
--- a/regression/contracts/frees-clause-while-loop-fail/test.desc
+++ b/regression/contracts/frees-clause-while-loop-fail/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --apply-loop-contracts
-^main.c.*: error: frees clause target must be a pointer-typed expression$
+^main.c.* error: frees clause target must be a pointer-typed expression or a call to a function returning __CPROVER_freeable_t$
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index b9952f9a4d2..fabb546b528 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -231,6 +231,14 @@ void ansi_c_internal_additions(std::string &code)
     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"
+    // Type that describes sets of freeable pointers
+    "typedef void " CPROVER_PREFIX "freeable_t;\n"
+    // Declares a pointer as freeable
+    CPROVER_PREFIX "freeable_t " CPROVER_PREFIX "freeable(void *ptr);\n"
+    // True iff ptr satisfies the preconditions of the free stdlib function
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "is_freeable(void *ptr);\n"
+    // True iff ptr was freed during function execution or loop execution
+    CPROVER_PREFIX "bool " CPROVER_PREFIX "is_freed(void *ptr);\n"
     "\n";
   // clang-format on
 
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index b392f92ec0c..ef98f7890b9 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -791,7 +791,25 @@ void c_typecheck_baset::typecheck_declaration(
           return;
 
         error().source_location = expr.source_location();
-        error() << id2string(id) + "is not allowed in preconditions." << eom;
+        error() << id2string(id) + " is not allowed in preconditions." << eom;
+        throw 0;
+      };
+
+      auto check_is_freed = [&](const exprt &expr) {
+        const irep_idt id = CPROVER_PREFIX "is_freed";
+
+        auto pred = [&](const exprt &expr) {
+          if(!can_cast_expr<symbol_exprt>(expr))
+            return false;
+
+          return to_symbol_expr(expr).get_identifier() == id;
+        };
+
+        if(!has_subexpr(expr, pred))
+          return;
+
+        error().source_location = expr.source_location();
+        error() << id2string(id) + " is not allowed in preconditions." << eom;
         throw 0;
       };
 
@@ -852,7 +870,7 @@ void c_typecheck_baset::typecheck_declaration(
           implicit_typecast_bool(requires);
           check_history_expr(requires);
           check_return_value(requires);
-          check_return_value(requires);
+          check_is_freed(requires);
           lambda_exprt lambda{temporary_parameter_symbols, requires};
           lambda.add_source_location() = requires.source_location();
           requires.swap(lambda);
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 3855121db88..bdf46e56dac 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -1014,11 +1014,43 @@ void c_typecheck_baset::typecheck_spec_frees_target(exprt &target)
     // an expression with pointer-type without side effects
     throw_on_side_effects(target);
   }
+  else if(can_cast_expr<side_effect_expr_function_callt>(target))
+  {
+    // A call to a freeable_t function symbol without other side effects
+    const auto &funcall = to_side_effect_expr_function_call(target);
+
+    if(!can_cast_expr<symbol_exprt>(funcall.function()))
+    {
+      error().source_location = target.source_location();
+      error() << "function pointer calls not allowed in frees clauses" << eom;
+      throw 0;
+    }
+
+    bool has_freeable_type =
+      (type.id() == ID_empty) &&
+      (type.get(ID_C_typedef) == CPROVER_PREFIX "freeable_t");
+    if(!has_freeable_type)
+    {
+      error().source_location = target.source_location();
+      error() << "expecting " CPROVER_PREFIX
+                 "freeable_t return type for function " +
+                   id2string(
+                     to_symbol_expr(funcall.function()).get_identifier()) +
+                   " called in frees clause"
+              << eom;
+      throw 0;
+    }
+
+    for(const auto &argument : funcall.arguments())
+      throw_on_side_effects(argument);
+  }
   else
   {
     // anything else is rejected
     error().source_location = target.source_location();
-    error() << "frees clause target must be a pointer-typed expression" << eom;
+    error() << "frees clause target must be a pointer-typed expression or a "
+               "call to a function returning " CPROVER_PREFIX "freeable_t"
+            << eom;
     throw 0;
   }
 }
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 1e08f893e1b..f9ed14f93e5 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2248,6 +2248,30 @@ exprt c_typecheck_baset::do_special_functions(
     typecheck_function_call_arguments(expr);
     return nil_exprt();
   }
+  else if(identifier == CPROVER_PREFIX "is_freeable")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << CPROVER_PREFIX "is_freeable expects one operand; "
+              << expr.arguments().size() << "provided." << eom;
+      throw 0;
+    }
+    typecheck_function_call_arguments(expr);
+    return nil_exprt();
+  }
+  else if(identifier == CPROVER_PREFIX "is_freed")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << CPROVER_PREFIX "is_freed expects one operand; "
+              << expr.arguments().size() << "provided." << eom;
+      throw 0;
+    }
+    typecheck_function_call_arguments(expr);
+    return nil_exprt();
+  }
   else if(identifier == CPROVER_PREFIX "same_object")
   {
     if(expr.arguments().size()!=2)
diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h
index a8a4d8fe29e..5fabb85300d 100644
--- a/src/ansi-c/cprover_builtin_headers.h
+++ b/src/ansi-c/cprover_builtin_headers.h
@@ -37,6 +37,8 @@ void __CPROVER_atomic_end();
 void __CPROVER_fence(const char *kind, ...);
 
 // contract-related functions
+__CPROVER_bool __CPROVER_is_freeable(const void *mem);
+__CPROVER_bool __CPROVER_is_freed(const void *mem);
 __CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size);
 void __CPROVER_old(const void *);
 void __CPROVER_loop_entry(const void *);
@@ -129,4 +131,5 @@ __CPROVER_assignable_t __CPROVER_assignable(void *ptr, __CPROVER_size_t size,
 __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);
+__CPROVER_assignable_t __CPROVER_freeable(void *ptr);
 // clang-format on
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
index 61bf2687c68..e62818879f8 100644
--- a/src/ansi-c/library/cprover.h
+++ b/src/ansi-c/library/cprover.h
@@ -19,6 +19,8 @@ typedef __typeof__(sizeof(int)) __CPROVER_size_t;
 typedef signed long long __CPROVER_ssize_t;
 // NOLINTNEXTLINE(readability/identifiers)
 typedef void __CPROVER_assignable_t;
+// NOLINTNEXTLINE(readability/identifiers)
+typedef void __CPROVER_freeable_t;
 
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 void __CPROVER_deallocate(void *);
diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
index 09c3ab4f73c..7f634ec1f83 100644
--- a/src/linking/remove_internal_symbols.cpp
+++ b/src/linking/remove_internal_symbols.cpp
@@ -156,6 +156,10 @@ void remove_internal_symbols(
   special.insert(CPROVER_PREFIX "object_upto");
   special.insert(CPROVER_PREFIX "object_from");
   special.insert(CPROVER_PREFIX "whole_object");
+  special.insert(CPROVER_PREFIX "freeable_t");
+  special.insert(CPROVER_PREFIX "freeable");
+  special.insert(CPROVER_PREFIX "is_freeable");
+  special.insert(CPROVER_PREFIX "is_freed");
   special.insert(rounding_mode_identifier());
   special.insert("__new");
   special.insert("__new_array");