Skip to content

Cleanup asserts & throws - replace with invariants #3013

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 21, 2018
Merged

Cleanup asserts & throws - replace with invariants #3013

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
59 changes: 37 additions & 22 deletions src/goto-programs/string_abstraction.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]

#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/exception_utils.h>
#include <util/pointer_predicates.h>
#include <util/type_eq.h>

Expand Down Expand Up @@ -379,7 +380,9 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest,
++it2;
}

assert(components.size()==seen);
INVARIANT(
components.size() == seen,
"some of the symbol's component names were not found in the source");
}

return nil_exprt();
Expand Down Expand Up @@ -549,8 +552,8 @@ void string_abstractiont::abstract_function_call(

if(it1==arguments.end())
{
error() << "function call: not enough arguments" << eom;
throw 0;
throw incorrect_goto_program_exceptiont(
"function call: not enough arguments", target->source_location);
}

str_args.push_back(exprt());
Expand All @@ -562,8 +565,9 @@ void string_abstractiont::abstract_function_call(
if(str_args.back().type().id()==ID_array &&
abstract_type.id()==ID_pointer)
{
assert(type_eq(str_args.back().type().subtype(),
abstract_type.subtype(), ns));
INVARIANT(
type_eq(str_args.back().type().subtype(), abstract_type.subtype(), ns),
"argument array type differs from formal parameter pointer type");

index_exprt idx(str_args.back(), from_integer(0, index_type()));
// disable bounds check on that one
Expand Down Expand Up @@ -600,19 +604,19 @@ void string_abstractiont::replace_string_macros(
{
if(expr.id()=="is_zero_string")
{
assert(expr.operands().size()==1);
PRECONDITION(expr.operands().size() == 1);
exprt tmp=build(expr.op0(), whatt::IS_ZERO, lhs, source_location);
expr.swap(tmp);
}
else if(expr.id()=="zero_string_length")
{
assert(expr.operands().size()==1);
PRECONDITION(expr.operands().size() == 1);
exprt tmp=build(expr.op0(), whatt::LENGTH, lhs, source_location);
expr.swap(tmp);
}
else if(expr.id()=="buffer_size")
{
assert(expr.operands().size()==1);
PRECONDITION(expr.operands().size() == 1);
exprt tmp=build(expr.op0(), whatt::SIZE, false, source_location);
expr.swap(tmp);
}
Expand All @@ -631,8 +635,10 @@ exprt string_abstractiont::build(
if(pointer.id()==ID_typecast)
{
// cast from another pointer type?
assert(pointer.operands().size()==1);
if(pointer.op0().type().id()!=ID_pointer)
INVARIANT(
pointer.operands().size() == 1,
"pointer typecast takes exactly 1 argument");
if(pointer.op0().type().id() != ID_pointer)
return build_unknown(what, write);

// recursive call
Expand Down Expand Up @@ -669,7 +675,7 @@ const typet &string_abstractiont::build_abstraction_type(const typet &type)

abstraction_types_map.swap(tmp);
map_entry=tmp.find(eff_type);
assert(map_entry!=tmp.end());
CHECK_RETURN(map_entry != tmp.end());
return abstraction_types_map.insert(
std::make_pair(eff_type, map_entry->second)).first->second;
}
Expand Down Expand Up @@ -836,7 +842,7 @@ bool string_abstractiont::build_if(const if_exprt &o_if,
bool string_abstractiont::build_array(const array_exprt &object,
exprt &dest, bool write)
{
assert(is_char_type(object.type().subtype()));
PRECONDITION(is_char_type(object.type().subtype()));

// writing is invalid
if(write)
Expand All @@ -847,7 +853,8 @@ bool string_abstractiont::build_array(const array_exprt &object,
// don't do anything, if we cannot determine the size
if(to_integer(a_size, size))
return true;
assert(size==object.operands().size());
INVARIANT(
size == object.operands().size(), "wrong number of array object arguments");

exprt::operandst::const_iterator it=object.operands().begin();
for(mp_integer i=0; i<size; ++i, ++it)
Expand All @@ -860,7 +867,7 @@ bool string_abstractiont::build_array(const array_exprt &object,
bool string_abstractiont::build_pointer(const exprt &object,
exprt &dest, bool write)
{
assert(object.type().id()==ID_pointer);
PRECONDITION(object.type().id() == ID_pointer);

pointer_arithmetict ptr(object);
if(ptr.pointer.id()==ID_address_of)
Expand Down Expand Up @@ -945,7 +952,7 @@ bool string_abstractiont::build_symbol(const symbol_exprt &sym, exprt &dest)
const symbolt &symbol=ns.lookup(sym.get_identifier());

const typet &abstract_type=build_abstraction_type(symbol.type);
assert(!abstract_type.is_nil());
CHECK_RETURN(!abstract_type.is_nil());

irep_idt identifier="";

Expand Down Expand Up @@ -1125,7 +1132,9 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
if(!build_wrap(i_lhs.array(), new_lhs, true))
{
exprt i2=member(new_lhs, whatt::LENGTH);
assert(i2.is_not_nil());
INVARIANT(
i2.is_not_nil(),
"failed to create length-component for the left-hand-side");

exprt new_length=i_lhs.index();
make_type(new_length, i2.type());
Expand All @@ -1143,7 +1152,9 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
if(!build_wrap(ptr.pointer, new_lhs, true))
{
const exprt i2=member(new_lhs, whatt::LENGTH);
assert(i2.is_not_nil());
INVARIANT(
i2.is_not_nil(),
"failed to create length-component for the left-hand-side");

make_type(ptr.offset, build_type(whatt::LENGTH));
return
Expand Down Expand Up @@ -1171,7 +1182,9 @@ goto_programt::targett string_abstractiont::char_assign(
goto_programt tmp;

const exprt i1=member(new_lhs, whatt::IS_ZERO);
assert(i1.is_not_nil());
INVARIANT(
i1.is_not_nil(),
"failed to create is_zero-component for the left-hand-side");

goto_programt::targett assignment1=tmp.add_instruction();
assignment1->make_assignment();
Expand Down Expand Up @@ -1207,7 +1220,7 @@ goto_programt::targett string_abstractiont::value_assignments(
if(rhs.id()==ID_if)
return value_assignments_if(dest, target, lhs, to_if_expr(rhs));

assert(type_eq(lhs.type(), rhs.type(), ns));
PRECONDITION(type_eq(lhs.type(), rhs.type(), ns));

if(lhs.type().id()==ID_array)
{
Expand All @@ -1234,7 +1247,8 @@ goto_programt::targett string_abstractiont::value_assignments(

for(const auto &comp : struct_union_type.components())
{
assert(!comp.get_name().empty());
INVARIANT(
!comp.get_name().empty(), "struct/union components must have a name");

target=value_assignments(dest, target,
member_exprt(lhs, comp.get_name(), comp.type()),
Expand Down Expand Up @@ -1334,8 +1348,9 @@ exprt string_abstractiont::member(const exprt &a, whatt what)
if(a.is_nil())
return a;

assert(type_eq(a.type(), string_struct, ns) ||
is_ptr_string_struct(a.type()));
PRECONDITION_WITH_DIAGNOSTICS(
type_eq(a.type(), string_struct, ns) || is_ptr_string_struct(a.type()),
"either the expression is not a string or it is not a pointer to one");

exprt struct_op=
a.type().id()==ID_pointer?
Expand Down