Skip to content

Commit b06a880

Browse files
authored
Merge pull request #7117 from diffblue/is_cstring
add __CPROVER_is_cstring(p) and __CPROVER_cstrlen(p)
2 parents 40d4ab9 + 0f94b00 commit b06a880

File tree

4 files changed

+105
-0
lines changed

4 files changed

+105
-0
lines changed

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2316,6 +2316,52 @@ exprt c_typecheck_baset::do_special_functions(
23162316

23172317
return std::move(is_list_expr);
23182318
}
2319+
else if(identifier == CPROVER_PREFIX "is_cstring")
2320+
{
2321+
if(expr.arguments().size() != 1)
2322+
{
2323+
error().source_location = f_op.source_location();
2324+
error() << "is_cstring expects one operand" << eom;
2325+
throw 0;
2326+
}
2327+
2328+
typecheck_function_call_arguments(expr);
2329+
2330+
if(expr.arguments()[0].type().id() != ID_pointer)
2331+
{
2332+
error().source_location = expr.arguments()[0].source_location();
2333+
error() << "is_cstring expects a pointer operand" << eom;
2334+
throw 0;
2335+
}
2336+
2337+
is_cstring_exprt is_cstring_expr(expr.arguments()[0]);
2338+
is_cstring_expr.add_source_location() = source_location;
2339+
2340+
return std::move(is_cstring_expr);
2341+
}
2342+
else if(identifier == CPROVER_PREFIX "cstrlen")
2343+
{
2344+
if(expr.arguments().size() != 1)
2345+
{
2346+
error().source_location = f_op.source_location();
2347+
error() << "cstrlen expects one operand" << eom;
2348+
throw 0;
2349+
}
2350+
2351+
typecheck_function_call_arguments(expr);
2352+
2353+
if(expr.arguments()[0].type().id() != ID_pointer)
2354+
{
2355+
error().source_location = expr.arguments()[0].source_location();
2356+
error() << "cstrlen expects a pointer operand" << eom;
2357+
throw 0;
2358+
}
2359+
2360+
unary_exprt cstrlen_expr("cstrlen", expr.arguments()[0], size_type());
2361+
cstrlen_expr.add_source_location() = source_location;
2362+
2363+
return std::move(cstrlen_expr);
2364+
}
23192365
else if(identifier==CPROVER_PREFIX "is_zero_string")
23202366
{
23212367
if(expr.arguments().size()!=1)

src/ansi-c/cprover_builtin_headers.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@ _Bool __CPROVER_is_zero_string(const void *);
1313
// a singly-linked null-terminated dynamically-allocated list
1414
__CPROVER_bool __CPROVER_is_list();
1515
__CPROVER_size_t __CPROVER_zero_string_length(const void *);
16+
__CPROVER_bool __CPROVER_is_cstring(const char *);
17+
__CPROVER_size_t __CPROVER_cstrlen(const char *);
1618
__CPROVER_size_t __CPROVER_buffer_size(const void *);
1719
__CPROVER_bool __CPROVER_r_ok();
1820
__CPROVER_bool __CPROVER_w_ok();

src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -153,6 +153,7 @@ IREP_ID_TWO(C_default_value, #default_value)
153153
IREP_ID_ONE(base_name)
154154
IREP_ID_TWO(C_base_name, #base_name)
155155
IREP_ID_ONE(string)
156+
IREP_ID_ONE(is_cstring)
156157
IREP_ID_TWO(C_string_constant, #string_constant)
157158
IREP_ID_ONE(string_constant)
158159
IREP_ID_ONE(width)

src/util/pointer_expr.h

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1059,6 +1059,62 @@ inline void validate_expr(const object_size_exprt &value)
10591059
"Object size expression must have pointer typed operand.");
10601060
}
10611061

1062+
/// A predicate that indicates that a zero-terminated string
1063+
/// starts at the given address
1064+
class is_cstring_exprt : public unary_predicate_exprt
1065+
{
1066+
public:
1067+
explicit is_cstring_exprt(exprt address)
1068+
: unary_predicate_exprt(ID_is_cstring, std::move(address))
1069+
{
1070+
PRECONDITION(as_const(*this).address().type().id() == ID_pointer);
1071+
}
1072+
1073+
exprt &address()
1074+
{
1075+
return op0();
1076+
}
1077+
1078+
const exprt &address() const
1079+
{
1080+
return op0();
1081+
}
1082+
};
1083+
1084+
template <>
1085+
inline bool can_cast_expr<is_cstring_exprt>(const exprt &base)
1086+
{
1087+
return base.id() == ID_is_cstring;
1088+
}
1089+
1090+
inline void validate_expr(const is_cstring_exprt &value)
1091+
{
1092+
validate_operands(value, 1, "is_cstring must have one operand");
1093+
}
1094+
1095+
/// \brief Cast an exprt to a \ref is_cstring_exprt
1096+
///
1097+
/// \a expr must be known to be \ref is_cstring_exprt.
1098+
///
1099+
/// \param expr: Source expression
1100+
/// \return Object of type \ref is_cstring_exprt
1101+
inline const is_cstring_exprt &to_is_cstring_expr(const exprt &expr)
1102+
{
1103+
PRECONDITION(expr.id() == ID_is_cstring);
1104+
const is_cstring_exprt &ret = static_cast<const is_cstring_exprt &>(expr);
1105+
validate_expr(ret);
1106+
return ret;
1107+
}
1108+
1109+
/// \copydoc to_is_cstring_expr(const exprt &)
1110+
inline is_cstring_exprt &to_is_cstring_expr(exprt &expr)
1111+
{
1112+
PRECONDITION(expr.id() == ID_is_cstring);
1113+
is_cstring_exprt &ret = static_cast<is_cstring_exprt &>(expr);
1114+
validate_expr(ret);
1115+
return ret;
1116+
}
1117+
10621118
/// A predicate that indicates that the object pointed to is live
10631119
class live_object_exprt : public unary_predicate_exprt
10641120
{

0 commit comments

Comments
 (0)