Merge pull request #7136 from diffblue/deterrent

add comments to warn about experimental predicates

Author: tautschnig

src/ansi-c/c_typecheck_expr.cpp

@@ -2291,6 +2291,7 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier == CPROVER_PREFIX "is_list")
   {
+    // experimental feature for CHC encodings -- do not use
     if(expr.arguments().size() != 1)
     {
       error().source_location = f_op.source_location();
@@ -2318,6 +2319,7 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier == CPROVER_PREFIX "is_dll")
   {
+    // experimental feature for CHC encodings -- do not use
     if(expr.arguments().size() != 1)
     {
       error().source_location = f_op.source_location();
@@ -2345,6 +2347,7 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier == CPROVER_PREFIX "is_cyclic_dll")
   {
+    // experimental feature for CHC encodings -- do not use
     if(expr.arguments().size() != 1)
     {
       error().source_location = f_op.source_location();
@@ -2372,6 +2375,7 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier == CPROVER_PREFIX "is_sentinel_dll")
   {
+    // experimental feature for CHC encodings -- do not use
     if(expr.arguments().size() != 2 && expr.arguments().size() != 3)
     {
       error().source_location = f_op.source_location();
@@ -2402,6 +2406,7 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier == CPROVER_PREFIX "is_cstring")
   {
+    // experimental feature for CHC encodings -- do not use
     if(expr.arguments().size() != 1)
     {
       error().source_location = f_op.source_location();
@@ -2425,6 +2430,7 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier == CPROVER_PREFIX "cstrlen")
   {
+    // experimental feature for CHC encodings -- do not use
     if(expr.arguments().size() != 1)
     {
       error().source_location = f_op.source_location();

src/ansi-c/cprover_builtin_headers.h

@@ -10,19 +10,20 @@ __CPROVER_bool __CPROVER_equal();
 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
 __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 *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
 __CPROVER_bool __CPROVER_r_ok();
 __CPROVER_bool __CPROVER_w_ok();
 __CPROVER_bool __CPROVER_rw_ok();
 
+// experimental features for CHC encodings -- do not use
+__CPROVER_bool __CPROVER_is_list(); // a singly-linked null-terminated dynamically-allocated list
+__CPROVER_bool __CPROVER_is_dll();
+__CPROVER_bool __CPROVER_is_cyclic_dll();
+__CPROVER_bool __CPROVER_is_sentinel_dll();
+__CPROVER_bool __CPROVER_is_cstring(const char *);
+__CPROVER_size_t __CPROVER_cstrlen(const char *);
+
 // bitvector analysis
 __CPROVER_bool __CPROVER_get_flag(const void *, const char *);
 void __CPROVER_set_must(const void *, const char *);

src/util/pointer_expr.h

@@ -1060,7 +1060,8 @@ inline void validate_expr(const object_size_exprt &value)
 }
 
 /// A predicate that indicates that a zero-terminated string
-/// starts at the given address
+/// starts at the given address.
+/// This is an experimental feature for CHC encodings -- do not use.
 class is_cstring_exprt : public unary_predicate_exprt
 {
 public:
@@ -1118,6 +1119,7 @@ inline is_cstring_exprt &to_is_cstring_expr(exprt &expr)
 /// An expression, akin to ISO C's strlen, that denotes the
 /// length of a zero-terminated string that starts at the
 /// given address. The trailing zero is not included in the count.
+/// This is an experimental feature for CHC encodings -- do not use.
 class cstrlen_exprt : public unary_exprt
 {
 public:
@@ -1172,7 +1174,8 @@ inline cstrlen_exprt &to_cstrlen_expr(exprt &expr)
   return ret;
 }
 
-/// A predicate that indicates that the object pointed to is live
+/// A predicate that indicates that the object pointed to is live.
+/// This is an experimental feature for CHC encodings -- do not use.
 class live_object_exprt : public unary_predicate_exprt
 {
 public:
@@ -1227,7 +1230,8 @@ inline live_object_exprt &to_live_object_expr(exprt &expr)
   return ret;
 }
 
-/// A predicate that indicates that the object pointed to is writeable
+/// A predicate that indicates that the object pointed to is writeable.
+/// This is an experimental feature for CHC encodings -- do not use.
 class writeable_object_exprt : public unary_predicate_exprt
 {
 public: