Skip to content

add comments to warn about experimental predicates #7136

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Sep 16, 2022
+21 −10
Merged

add comments to warn about experimental predicates #7136

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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();
Expand All @@ -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();
Expand Down
15 changes: 8 additions & 7 deletions src/ansi-c/cprover_builtin_headers.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *);
Expand Down
10 changes: 7 additions & 3 deletions src/util/pointer_expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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:
Expand Down