diff --git a/regression/cbmc/Void_Pointer_Init/main.c b/regression/cbmc/Void_Pointer_Init/main.c new file mode 100644 index 00000000000..c9165c09ce7 --- /dev/null +++ b/regression/cbmc/Void_Pointer_Init/main.c @@ -0,0 +1,6 @@ +#include + +void foo(void *arg) +{ + assert(*(unsigned *)(arg) == 5); +} diff --git a/regression/cbmc/Void_Pointer_Init/test.desc b/regression/cbmc/Void_Pointer_Init/test.desc new file mode 100644 index 00000000000..d39ab161cbf --- /dev/null +++ b/regression/cbmc/Void_Pointer_Init/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--function foo --pointer-check +^\[foo.assertion.1\] line \d+ assertion \*\(unsigned \*\)\(arg\) == 5: FAILURE$ +^\[foo.pointer_dereference.4\] line \d+ dereference failure: dead object in \*\(\(unsigned int \*\)arg\): FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 7880faae78e..35ad6550cb6 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1113,7 +1113,8 @@ void goto_checkt::pointer_validity_check( const exprt &pointer=expr.pointer(); auto size_of_expr_opt = size_of_expr(expr.type(), ns); - CHECK_RETURN(size_of_expr_opt.has_value()); + if(!size_of_expr_opt.has_value()) + return; // in the case of `void*` auto conditions = address_check(pointer, size_of_expr_opt.value()); diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 1868627547a..c8a44618f49 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -2214,6 +2214,10 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) convert_typecast(tmp); } } + else if(src_type.id() == ID_empty) + { + convert_expr(src); + } else { std::ostringstream e_str; @@ -4626,6 +4630,11 @@ void smt2_convt::convert_type(const typet &type) { convert_type(c_bit_field_replacement_type(to_c_bit_field_type(type), ns)); } + else if(type.id() == ID_empty) + { + // the NONDET(void) is in fact of type char + out << "(_ BitVec " << boolbv_width(char_type()) << " )"; + } else { UNEXPECTEDCASE("unsupported type: "+type.id_string());