Skip to content

Commit bc174f3

Browse files
committed
Clean-up and test __CPROVER_{r,w,rw}_ok type checking failure cases
1. Avoid `throw 0` 2. size_of_expr cannot fail at this point given all prior type checking. 3. Test all the failure handling.
1 parent dde7cf4 commit bc174f3

File tree

5 files changed

+45
-19
lines changed

5 files changed

+45
-19
lines changed
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int *p = (int *)0;
6+
#ifdef TOO_MANY_ARGS
7+
assert(!__CPROVER_r_ok(p, sizeof(int), 42));
8+
#elif defined(NOT_A_POINTER)
9+
assert(!__CPROVER_r_ok(*p, sizeof(int)));
10+
#elif defined(VOID_POINTER_NO_SIZE)
11+
assert(!__CPROVER_r_ok((void *)p));
12+
#endif
13+
}
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
-DNOT_A_POINTER
4+
__CPROVER_r_ok expects a pointer as first argument$
5+
^CONVERSION ERROR$
6+
^EXIT=(64|1)$
7+
^SIGNAL=0$
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
-DTOO_MANY_ARGS
4+
__CPROVER_r_ok expects one or two operands$
5+
^CONVERSION ERROR$
6+
^EXIT=(64|1)$
7+
^SIGNAL=0$
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
-DVOID_POINTER_NO_SIZE
4+
__CPROVER_r_ok expects a size when given a void pointer$
5+
^CONVERSION ERROR$
6+
^EXIT=(64|1)$
7+
^SIGNAL=0$

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 11 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -2225,9 +2225,9 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
22252225
{
22262226
if(expr.arguments().size() != 1 && expr.arguments().size() != 2)
22272227
{
2228-
error().source_location = f_op.source_location();
2229-
error() << identifier << " expects one or two operands" << eom;
2230-
throw 0;
2228+
throw invalid_source_file_exceptiont{
2229+
id2string(identifier) + " expects one or two operands",
2230+
f_op.source_location()};
22312231
}
22322232

22332233
// the first argument must be a pointer
@@ -2240,10 +2240,9 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
22402240
}
22412241
else if(pointer_expr.type().id() != ID_pointer)
22422242
{
2243-
error().source_location = f_op.source_location();
2244-
error() << identifier << " expects a pointer as first argument"
2245-
<< eom;
2246-
throw 0;
2243+
throw invalid_source_file_exceptiont{
2244+
id2string(identifier) + " expects a pointer as first argument",
2245+
f_op.source_location()};
22472246
}
22482247

22492248
// The second argument, when given, is a size_t.
@@ -2262,21 +2261,14 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
22622261
to_pointer_type(pointer_expr.type()).base_type();
22632262
if(subtype.id() == ID_empty)
22642263
{
2265-
error().source_location = f_op.source_location();
2266-
error() << identifier << " expects a size when given a void pointer"
2267-
<< eom;
2268-
throw 0;
2264+
throw invalid_source_file_exceptiont{
2265+
id2string(identifier) +
2266+
" expects a size when given a void pointer",
2267+
f_op.source_location()};
22692268
}
22702269

22712270
auto size_expr_opt = size_of_expr(subtype, *this);
2272-
if(!size_expr_opt.has_value())
2273-
{
2274-
error().source_location = f_op.source_location();
2275-
error() << identifier << " was given object pointer without size"
2276-
<< eom;
2277-
throw 0;
2278-
}
2279-
2271+
CHECK_RETURN(size_expr_opt.has_value());
22802272
size_expr = std::move(size_expr_opt.value());
22812273
}
22822274

0 commit comments

Comments
 (0)