diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index ff1ed05c120..6f0a52a79c3 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2316,6 +2316,90 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(is_list_expr);
   }
+  else if(identifier == CPROVER_PREFIX "is_dll")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << "is_dll expects one operand" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    if(
+      expr.arguments()[0].type().id() != ID_pointer ||
+      to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
+        ID_struct_tag)
+    {
+      error().source_location = expr.arguments()[0].source_location();
+      error() << "is_dll expects a struct-pointer operand" << eom;
+      throw 0;
+    }
+
+    predicate_exprt is_dll_expr("is_dll");
+    is_dll_expr.operands() = expr.arguments();
+    is_dll_expr.add_source_location() = source_location;
+
+    return std::move(is_dll_expr);
+  }
+  else if(identifier == CPROVER_PREFIX "is_cyclic_dll")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << "is_cyclic_dll expects one operand" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    if(
+      expr.arguments()[0].type().id() != ID_pointer ||
+      to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
+        ID_struct_tag)
+    {
+      error().source_location = expr.arguments()[0].source_location();
+      error() << "is_cyclic_dll expects a struct-pointer operand" << eom;
+      throw 0;
+    }
+
+    predicate_exprt is_cyclic_dll_expr("is_cyclic_dll");
+    is_cyclic_dll_expr.operands() = expr.arguments();
+    is_cyclic_dll_expr.add_source_location() = source_location;
+
+    return std::move(is_cyclic_dll_expr);
+  }
+  else if(identifier == CPROVER_PREFIX "is_sentinel_dll")
+  {
+    if(expr.arguments().size() != 2 && expr.arguments().size() != 3)
+    {
+      error().source_location = f_op.source_location();
+      error() << "is_sentinel_dll expects two or three operands" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    for(const auto &argument : expr.arguments())
+    {
+      if(
+        argument.type().id() != ID_pointer ||
+        to_pointer_type(argument.type()).base_type().id() != ID_struct_tag)
+      {
+        error().source_location = expr.arguments()[0].source_location();
+        error() << "is_sentinel_dll_node expects struct-pointer operands"
+                << eom;
+        throw 0;
+      }
+    }
+
+    predicate_exprt is_sentinel_dll_expr("is_sentinel_dll");
+    is_sentinel_dll_expr.operands() = expr.arguments();
+    is_sentinel_dll_expr.add_source_location() = source_location;
+
+    return std::move(is_sentinel_dll_expr);
+  }
   else if(identifier == CPROVER_PREFIX "is_cstring")
   {
     if(expr.arguments().size() != 1)
@@ -2414,6 +2498,38 @@ exprt c_typecheck_baset::do_special_functions(
 
     return is_dynamic_object_expr;
   }
+  else if(identifier == CPROVER_PREFIX "LIVE_OBJECT")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << "live_object expects one argument" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    exprt live_object_expr = live_object_exprt(expr.arguments()[0]);
+    live_object_expr.add_source_location() = source_location;
+
+    return live_object_expr;
+  }
+  else if(identifier == CPROVER_PREFIX "WRITEABLE_OBJECT")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << "writeable_object expects one argument" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    exprt writeable_object_expr = writeable_object_exprt(expr.arguments()[0]);
+    writeable_object_expr.add_source_location() = source_location;
+
+    return writeable_object_expr;
+  }
   else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
   {
     if(expr.arguments().size()!=1)
diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h
index 3d0d56aa9a0..ac6a07311eb 100644
--- a/src/ansi-c/cprover_builtin_headers.h
+++ b/src/ansi-c/cprover_builtin_headers.h
@@ -12,6 +12,9 @@ __CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
 _Bool __CPROVER_is_zero_string(const void *);
 // a singly-linked null-terminated dynamically-allocated list
 __CPROVER_bool __CPROVER_is_list();
+__CPROVER_bool __CPROVER_is_dll();
+__CPROVER_bool __CPROVER_is_cyclic_dll();
+__CPROVER_bool __CPROVER_is_sentinel_dll();
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_bool __CPROVER_is_cstring(const char *);
 __CPROVER_size_t __CPROVER_cstrlen(const char *);
@@ -46,6 +49,8 @@ void __CPROVER_old(const void *);
 void __CPROVER_loop_entry(const void *);
 
 // pointers
+__CPROVER_bool __CPROVER_LIVE_OBJECT(const void *);
+__CPROVER_bool __CPROVER_WRITEABLE_OBJECT(const void *);
 __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
 __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
 __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 05988997e4d..6c9dd590420 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -3988,6 +3988,8 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
     {ID_count_leading_zeros, "__builtin_clz"},
     {ID_count_trailing_zeros, "__builtin_ctz"},
     {ID_dynamic_object, "DYNAMIC_OBJECT"},
+    {ID_live_object, "LIVE_OBJECT"},
+    {ID_writeable_object, "WRITEABLE_OBJECT"},
     {ID_floatbv_div, "FLOAT/"},
     {ID_floatbv_minus, "FLOAT-"},
     {ID_floatbv_mult, "FLOAT*"},