diff --git a/doc/cprover-manual/contracts-frees.md b/doc/cprover-manual/contracts-frees.md
new file mode 100644
index 00000000000..95351c65905
--- /dev/null
+++ b/doc/cprover-manual/contracts-frees.md
@@ -0,0 +1,125 @@
+[CPROVER Manual TOC](../../)
+
+# Frees Clauses
+
+A _frees clause_ allows the user to specify a set of pointers that may be freed
+by a function or by the function it calls, transitively.
+A function contract may have zero or more frees clauses.
+When no clause is provided the empty set is used as default.
+Contracts can also have an empty frees clause.
+When more than one frees clause is given, the sets of pointers they contain are
+unioned together to yield a single set of pointers.
+
+## Syntax
+
+The clause has the following syntax (square brackets denote optional expressions
+`[` `]` ):
+```c
+__CPROVER_frees([targets])
+```
+
+Where `targets` has the following syntax:
+```
+          targets ::= cond-target-group (';' cond-target-group)* ';'?
+cond-target-group ::= (condition ':')? target (',' target)*
+           target ::= lvalue-expr
+                    | __CPROVER_freeable(lvalue-expr)
+```
+
+A frees clause target must be either:
+- an lvalue expression with a pointer type,
+- a call to the built-in function `__CPROVER_freeable`
+- a call to a user-defined side effect free and deterministic function returning
+  the type `void` (itself containing direct or indirect calls to
+  `__CPROVER_freeable` or to functions that call `__CPROVER_freeable`);
+
+### Example
+
+```c
+int foo(char *arr1, char *arr2, size_t size)
+__CPROVER_frees(
+    // `arr1` is freeable only if the condition `size > 0 && arr1` holds
+    size > 0 && arr1: arr1;
+
+    // `arr2` is always freeable
+    arr2;
+)
+{
+  if(size > 0 && arr1)
+    free(arr1);
+  free(arr2);
+  return 0;
+}
+```
+
+## Semantics
+
+The set of pointers specified by the frees clause of the contract is interpreted
+at the function call-site where the contract is being checked or used to abstract
+a function call.
+
+### For contract checking
+
+When checking a contract against a function, each pointer that the
+function attempts to free gets checked for membership in the set of
+pointers specified by the _frees clause_.
+
+### For replacement of function calls by contracts
+
+When replacing a function call by a contract, each pointer of the
+_frees clause_ is non-deterministically freed after the function call.
+
+## Specifying parametric sets of freeable pointers using C functions
+
+Users can define parametric sets of freeable pointers by writing functions that
+return the built-in type void and call the built-in function
+`__CPROVER_freeable` (directly or indirectly through some other user-defined
+function). The functions must be side-effect free and deterministic,
+as well as loop-free and recursion-free.
+
+```c
+void my_freeable_set(char **arr, size_t size)
+{
+  // The first 3 pointers are freeable
+  // if the array is at least of size 3.
+  if (arr && size > 3) {
+    __CPROVER_freeable(arr[0]);
+    __CPROVER_freeable(arr[1]);
+    __CPROVER_freeable(arr[2]);
+  }
+}
+```
+
+The built-in function:
+```c
+void __CPROVER_freeable(void *ptr);
+```
+adds the given pointer to the freeable set described by the enclosing function.
+
+Calls to such functions can 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`
+([see here](https://github.com/diffblue/cbmc/blob/cf00a53bbcc388748be9668f393276f6d84b1a60/src/ansi-c/library/stdlib.c#L269)),
+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_was_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 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..b15195d2ec9
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates-fail/main.c
@@ -0,0 +1,45 @@
+#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
+ // error was_freed cannot be used in preconditions
+__CPROVER_requires(!__CPROVER_was_freed(arr))
+__CPROVER_requires(__CPROVER_is_freeable(arr))
+__CPROVER_assigns(__CPROVER_object_whole(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_was_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..a6edf9e399c
--- /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_was_freed is not allowed in preconditions.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks that the front end rejects __CPROVER_was_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..b10cb56d486
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates-fail2/main.c
@@ -0,0 +1,44 @@
+#include <stdlib.h>
+
+// A function defining a conditionally freeable target
+int foo_frees(char *arr, const size_t size, const size_t new_size)
+{
+  __CPROVER_freeable(arr);
+  return 0;
+}
+
+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_object_whole(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_was_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..b1484cf2b62
--- /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 void 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-void-typed
+function calls in frees clauses.
diff --git a/regression/contracts/frees-clause-and-predicates-is_freeable-bad-arity/main.c b/regression/contracts/frees-clause-and-predicates-is_freeable-bad-arity/main.c
new file mode 100644
index 00000000000..10d45ca3c87
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates-is_freeable-bad-arity/main.c
@@ -0,0 +1,13 @@
+#include <stdlib.h>
+
+void foo(char *arr) __CPROVER_requires(__CPROVER_is_freeable(arr, 1))
+{
+}
+
+int main()
+{
+  size_t size;
+  char arr[size];
+  foo(arr);
+  return 0;
+}
diff --git a/regression/contracts/frees-clause-and-predicates-is_freeable-bad-arity/test.desc b/regression/contracts/frees-clause-and-predicates-is_freeable-bad-arity/test.desc
new file mode 100644
index 00000000000..cfea1068a38
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates-is_freeable-bad-arity/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c.*error: wrong number of function arguments: expected 1, but got 2$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks bad uses of __CPROVER_is_freeable are rejected.
diff --git a/regression/contracts/frees-clause-and-predicates-is_freed-bad-arity/main.c b/regression/contracts/frees-clause-and-predicates-is_freed-bad-arity/main.c
new file mode 100644
index 00000000000..51209b124a2
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates-is_freed-bad-arity/main.c
@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+void foo(char *arr) __CPROVER_requires(__CPROVER_is_freeable(arr))
+  __CPROVER_ensures(__CPROVER_was_freed(__CPROVER_old(arr), 1))
+{
+  free(arr);
+}
+
+int main()
+{
+  size_t size;
+  char arr[size];
+  foo(arr);
+  return 0;
+}
diff --git a/regression/contracts/frees-clause-and-predicates-is_freed-bad-arity/test.desc b/regression/contracts/frees-clause-and-predicates-is_freed-bad-arity/test.desc
new file mode 100644
index 00000000000..845d8bdde01
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates-is_freed-bad-arity/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^main.c.*error: wrong number of function arguments: expected 1, but got 2$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test checks bad uses of __CPROVER_was_freed are rejected.
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..3ab70076981
--- /dev/null
+++ b/regression/contracts/frees-clause-and-predicates/main.c
@@ -0,0 +1,44 @@
+#include <stdlib.h>
+
+// A function defining freeable pointers
+void foo_frees(char *arr, const size_t size, const size_t new_size)
+{
+  __CPROVER_freeable(arr);
+}
+
+// Function that resizes the array
+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_object_whole(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_was_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..2aa4d4b15ed
--- /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 typechecks correct uses of
+- void function calls as frees clause targets
+- the predicate __CPROVER_freeable
+- the predicate __CPROVER_is_freeable
+- the predicate __CPROVER_was_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/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index cb5beb98a2c..270daf1da2a 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 17c0dc34752..804adf9db67 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -227,8 +227,14 @@ void ansi_c_internal_additions(std::string &code)
     "  " CPROVER_PREFIX "size_t size);\n"
     // Declares bytes from ptr to the end of the object as assignable
     "void " CPROVER_PREFIX "object_from(void *ptr);\n"
-    // Declares the whole object pointer to by ptr
+    // Declares the whole object pointed to by ptr as assignable
     "void " CPROVER_PREFIX "object_whole(void *ptr);\n"
+    // Declares a pointer as freeable
+    "void " 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 "was_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 b91b168b256..6ef3bfb6451 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -701,6 +701,27 @@ void c_typecheck_baset::check_history_expr_return_value(
     expr.source_location());
 }
 
+void c_typecheck_baset::check_was_freed(
+  const exprt &expr,
+  std::string &clause_type)
+{
+  const irep_idt id = CPROVER_PREFIX "was_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))
+  {
+    throw invalid_source_file_exceptiont(
+      id2string(id) + " is not allowed in " + clause_type + ".",
+      expr.source_location());
+  }
+}
+
 void c_typecheck_baset::typecheck_declaration(
   ansi_c_declarationt &declaration)
 {
@@ -853,6 +874,7 @@ void c_typecheck_baset::typecheck_declaration(
           implicit_typecast_bool(requires);
           std::string clause_type = "preconditions";
           check_history_expr_return_value(requires, clause_type);
+          check_was_freed(requires, clause_type);
           lambda_exprt lambda{temporary_parameter_symbols, requires};
           lambda.add_source_location() = requires.source_location();
           requires.swap(lambda);
@@ -868,6 +890,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);
@@ -920,6 +950,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 09c3ef78da3..17369bdc287 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -151,14 +151,20 @@ class c_typecheck_baset:
   /// Checks that no history expr or return_value exists in expr
   virtual void
   check_history_expr_return_value(const exprt &expr, std::string &clause_type);
+  /// Checks that no occurence of the `CPROVER_PREFIX was_freed` predicate
+  /// is found in expr.
+  virtual void check_was_freed(const exprt &expr, std::string &clause_type);
+
   virtual void typecheck_spec_function_pointer_obeys_contract(exprt &expr);
   virtual void typecheck_spec_assigns(exprt::operandst &targets);
+  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);
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 8365e4216a0..8b2ec6450ad 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,6 +857,12 @@ 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::throw_on_side_effects(const exprt &expr)
@@ -971,6 +989,14 @@ void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
   typecheck_conditional_targets(targets, typecheck_target, "assigns");
 }
 
+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_target(exprt &target)
 {
   // compute type
@@ -1025,6 +1051,51 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target)
     target.source_location());
 }
 
+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 if(can_cast_expr<side_effect_expr_function_callt>(target))
+  {
+    // A call to a void function symbol without other side effects
+    const auto &funcall = to_side_effect_expr_function_call(target);
+
+    if(!can_cast_expr<symbol_exprt>(funcall.function()))
+    {
+      throw invalid_source_file_exceptiont(
+        "function pointer calls not allowed in frees clauses",
+        target.source_location());
+    }
+
+    if(type.id() != ID_empty)
+    {
+      throw invalid_source_file_exceptiont(
+        "expecting void return type for function '" +
+          id2string(to_symbol_expr(funcall.function()).get_identifier()) +
+          "' called in frees clause",
+        target.source_location());
+    }
+
+    for(const auto &argument : funcall.arguments())
+      throw_on_side_effects(argument);
+  }
+  else
+  {
+    // anything else is rejected
+    throw invalid_source_file_exceptiont(
+      "frees clause target must be a pointer-typed expression or a call to a "
+      "function returning void",
+      target.source_location());
+  }
+}
+
 void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract(
   exprt &expr)
 {
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 0550e3e1ee0..56e30600810 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
   }
diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h
index f3cdc86732a..96e1dbaa2f9 100644
--- a/src/ansi-c/cprover_builtin_headers.h
+++ b/src/ansi-c/cprover_builtin_headers.h
@@ -46,6 +46,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_was_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 *);
@@ -141,4 +143,5 @@ void __CPROVER_assignable(void *ptr, __CPROVER_size_t size,
 void __CPROVER_object_whole(void *ptr);
 void __CPROVER_object_from(void *ptr);
 void __CPROVER_object_upto(void *ptr, __CPROVER_size_t size);
+void __CPROVER_freeable(void *ptr);
 // clang-format on
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index b8f187e3050..f4f3a9fed1c 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      "^^"
@@ -3319,6 +3320,7 @@ cprover_function_contract:
           parser_stack($$).add_to_operands(std::move(tmp));
         }
         | cprover_contract_assigns
+        | cprover_contract_frees
         ;
 
 unary_expression_list:
@@ -3396,6 +3398,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/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
index db359a9e116..5518376d011 100644
--- a/src/linking/remove_internal_symbols.cpp
+++ b/src/linking/remove_internal_symbols.cpp
@@ -155,6 +155,9 @@ void remove_internal_symbols(
   special.insert(CPROVER_PREFIX "object_upto");
   special.insert(CPROVER_PREFIX "object_from");
   special.insert(CPROVER_PREFIX "object_whole");
+  special.insert(CPROVER_PREFIX "freeable");
+  special.insert(CPROVER_PREFIX "is_freeable");
+  special.insert(CPROVER_PREFIX "was_freed");
   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 b0754e1121a..50c3bfa306d 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -586,6 +586,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 41755fdb049..9b950c0d013 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 2d2cf061482..dd53c6ad3e4 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))