Merge pull request #4963 from diffblue/analyses-opX

fix exprt::opX accesses in analyses
This commit is contained in:
Daniel Kroening 2019-08-04 08:19:42 +01:00 committed by GitHub
commit b20cf69e6b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 46 additions and 35 deletions

View File

@ -704,10 +704,10 @@ exprt custom_bitvector_domaint::eval(
{
if(src.operands().size()==2)
{
unsigned bit_nr=
custom_bitvector_analysis.get_bit_nr(src.op1());
unsigned bit_nr =
custom_bitvector_analysis.get_bit_nr(to_binary_expr(src).op1());
exprt pointer=src.op0();
exprt pointer = to_binary_expr(src).op0();
if(pointer.type().id()!=ID_pointer)
return src;

View File

@ -790,7 +790,7 @@ void goto_checkt::integer_overflow_check(
exprt tmp;
if(i==1)
tmp=expr.op0();
tmp = to_multi_ary_expr(expr).op0();
else
{
tmp=expr;
@ -1732,7 +1732,8 @@ optionalt<exprt> goto_checkt::rw_ok_check(exprt expr)
DATA_INVARIANT(
expr.operands().size() == 2, "r/w_ok must have two operands");
const auto conditions = address_check(expr.op0(), expr.op1());
const auto conditions =
address_check(to_binary_expr(expr).op0(), to_binary_expr(expr).op1());
exprt::operandst conjuncts;
@ -1964,7 +1965,7 @@ void goto_checkt::goto_check(
{
// must not throw NULL
exprt pointer=i.code.op0().op0();
exprt pointer = to_unary_expr(i.code.op0()).op();
const notequal_exprt not_eq_null(
pointer, null_pointer_exprt(to_pointer_type(pointer.type())));

View File

@ -176,23 +176,26 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
}
else if(rhs.id()==ID_plus)
{
if(rhs.operands().size()>=3)
const auto &plus_expr = to_plus_expr(rhs);
if(plus_expr.operands().size() >= 3)
{
assert(rhs.op0().type().id()==ID_pointer);
return get_rec(rhs.op0(), loc_info_src) |
flagst::mk_uses_offset();
DATA_INVARIANT(
plus_expr.op0().type().id() == ID_pointer,
"pointer in pointer-typed sum must be op0");
return get_rec(plus_expr.op0(), loc_info_src) | flagst::mk_uses_offset();
}
else if(rhs.operands().size()==2)
else if(plus_expr.operands().size() == 2)
{
// one must be pointer, one an integer
if(rhs.op0().type().id()==ID_pointer)
if(plus_expr.op0().type().id() == ID_pointer)
{
return get_rec(rhs.op0(), loc_info_src) |
return get_rec(plus_expr.op0(), loc_info_src) |
flagst::mk_uses_offset();
}
else if(rhs.op1().type().id()==ID_pointer)
else if(plus_expr.op1().type().id() == ID_pointer)
{
return get_rec(rhs.op1(), loc_info_src) |
return get_rec(plus_expr.op1(), loc_info_src) |
flagst::mk_uses_offset();
}
else
@ -203,10 +206,11 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
}
else if(rhs.id()==ID_minus)
{
if(rhs.op0().type().id()==ID_pointer)
const auto &op0 = to_minus_expr(rhs).op0();
if(op0.type().id() == ID_pointer)
{
return get_rec(rhs.op0(), loc_info_src) |
flagst::mk_uses_offset();
return get_rec(op0, loc_info_src) | flagst::mk_uses_offset();
}
else
return flagst::mk_unknown();

View File

@ -250,21 +250,25 @@ void local_may_aliast::get_rec(
}
else if(rhs.id()==ID_plus)
{
if(rhs.operands().size()>=3)
const auto &plus_expr = to_plus_expr(rhs);
if(plus_expr.operands().size() >= 3)
{
assert(rhs.op0().type().id()==ID_pointer);
get_rec(dest, rhs.op0(), loc_info_src);
DATA_INVARIANT(
plus_expr.op0().type().id() == ID_pointer,
"pointer in pointer-typed sum must be op0");
get_rec(dest, plus_expr.op0(), loc_info_src);
}
else if(rhs.operands().size()==2)
else if(plus_expr.operands().size() == 2)
{
// one must be pointer, one an integer
if(rhs.op0().type().id()==ID_pointer)
if(plus_expr.op0().type().id() == ID_pointer)
{
get_rec(dest, rhs.op0(), loc_info_src);
get_rec(dest, plus_expr.op0(), loc_info_src);
}
else if(rhs.op1().type().id()==ID_pointer)
else if(plus_expr.op1().type().id() == ID_pointer)
{
get_rec(dest, rhs.op1(), loc_info_src);
get_rec(dest, plus_expr.op1(), loc_info_src);
}
else
dest.insert(unknown_object);
@ -274,9 +278,11 @@ void local_may_aliast::get_rec(
}
else if(rhs.id()==ID_minus)
{
if(rhs.op0().type().id()==ID_pointer)
const auto &op0 = to_minus_expr(rhs).op0();
if(op0.type().id() == ID_pointer)
{
get_rec(dest, rhs.op0(), loc_info_src);
get_rec(dest, op0, loc_info_src);
}
else
dest.insert(unknown_object);

View File

@ -43,7 +43,7 @@ static optionalt<goto_null_checkt> get_null_checked_expr(const exprt &expr)
// Reduce some roundabout ways of saying "x != null", e.g. "!(x == null)".
while(normalized_expr.id() == ID_not)
{
normalized_expr = normalized_expr.op0();
normalized_expr = to_not_expr(normalized_expr).op();
checked_when_taken = !checked_when_taken;
}
@ -55,8 +55,8 @@ static optionalt<goto_null_checkt> get_null_checked_expr(const exprt &expr)
if(normalized_expr.id() == ID_notequal)
{
const exprt &op0 = skip_typecast(normalized_expr.op0());
const exprt &op1 = skip_typecast(normalized_expr.op1());
const exprt &op0 = skip_typecast(to_notequal_expr(normalized_expr).op0());
const exprt &op1 = skip_typecast(to_notequal_expr(normalized_expr).op1());
if(op0.type().id() == ID_pointer &&
op0 == null_pointer_exprt(to_pointer_type(op0.type())))

View File

@ -370,7 +370,7 @@ void static_analysis_baset::do_function_call_rec(
calling_function,
l_call,
l_return,
function.op1(),
to_if_expr(function).true_case(),
arguments,
new_state,
goto_functions);
@ -379,7 +379,7 @@ void static_analysis_baset::do_function_call_rec(
calling_function,
l_call,
l_return,
function.op2(),
to_if_expr(function).false_case(),
arguments,
*n2,
goto_functions);

View File

@ -28,8 +28,8 @@ irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type)
/// Returns the symbol corresponding to an exception
exprt uncaught_exceptions_domaint::get_exception_symbol(const exprt &expr)
{
if(expr.id()!=ID_symbol && expr.has_operands())
return get_exception_symbol(expr.op0());
if(expr.id() != ID_symbol && expr.operands().size() >= 1)
return get_exception_symbol(to_multi_ary_expr(expr).op0());
return expr;
}