Skip to content

Replace use of deprecated nil_typet in acceleration [blocks: #3800] #3942

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
Jan 28, 2019
Merged

Replace use of deprecated nil_typet in acceleration [blocks: #3800] #3942

Show file tree
Hide file tree
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
12 changes: 6 additions & 6 deletions src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -653,19 +653,19 @@ void disjunctive_polynomial_accelerationt::assert_for_values(
exprt &target)
{
// First figure out what the appropriate type for this expression is.
typet expr_type=nil_typet();
optionalt<typet> expr_type;

for(std::map<exprt, exprt>::iterator it=values.begin();
it!=values.end();
++it)
{
if(expr_type==nil_typet())
if(!expr_type.has_value())
{
expr_type=it->first.type();
}
else
{
expr_type=join_types(expr_type, it->first.type());
expr_type = join_types(*expr_type, it->first.type());
}
}

Expand All @@ -690,7 +690,7 @@ void disjunctive_polynomial_accelerationt::assert_for_values(
it!=coefficients.end();
++it)
{
exprt concrete_value=from_integer(1, expr_type);
exprt concrete_value = from_integer(1, *expr_type);

for(expr_listt::const_iterator e_it=it->first.begin();
e_it!=it->first.end();
Expand All @@ -701,7 +701,7 @@ void disjunctive_polynomial_accelerationt::assert_for_values(
if(e==loop_counter)
{
mult_exprt mult(
from_integer(num_unwindings, expr_type), concrete_value);
from_integer(num_unwindings, *expr_type), concrete_value);
mult.swap(concrete_value);
}
else
Expand All @@ -718,7 +718,7 @@ void disjunctive_polynomial_accelerationt::assert_for_values(
// OK, concrete_value now contains the value of all the relevant variables
// multiplied together. Create the term concrete_value*coefficient and add
// it into the polynomial.
typecast_exprt cast(it->second, expr_type);
typecast_exprt cast(it->second, *expr_type);
const mult_exprt term(concrete_value, cast);

if(rhs.is_nil())
Expand Down
12 changes: 6 additions & 6 deletions src/goto-instrument/accelerate/polynomial.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ Author: Matt Lewis
exprt polynomialt::to_expr()
{
exprt ret=nil_exprt();
typet itype=nil_typet();
optionalt<typet> itype;

// Figure out the appropriate type to do all the intermediate calculations
// in.
Expand All @@ -35,13 +35,13 @@ exprt polynomialt::to_expr()
t_it!=m_it->terms.end();
++t_it)
{
if(itype==nil_typet())
if(itype.has_value())
{
itype=t_it->var.type();
}
else
{
itype=join_types(itype, t_it->var.type());
itype = join_types(*itype, t_it->var.type());
}
}
}
Expand All @@ -59,23 +59,23 @@ exprt polynomialt::to_expr()
coeff=-coeff;
}

exprt mon_expr=from_integer(coeff, itype);
exprt mon_expr = from_integer(coeff, *itype);

for(std::vector<monomialt::termt>::iterator t_it=m_it->terms.begin();
t_it!=m_it->terms.end();
++t_it)
{
for(unsigned int i=0; i < t_it->exp; i++)
{
mon_expr=mult_exprt(mon_expr, typecast_exprt(t_it->var, itype));
mon_expr = mult_exprt(mon_expr, typecast_exprt(t_it->var, *itype));
}
}

if(ret.id()==ID_nil)
{
if(neg)
{
ret=unary_minus_exprt(mon_expr, itype);
ret = unary_minus_exprt(mon_expr, *itype);
}
else
{
Expand Down
17 changes: 9 additions & 8 deletions src/goto-instrument/accelerate/polynomial_accelerator.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -508,7 +508,7 @@ void polynomial_acceleratort::assert_for_values(
overflow_instrumentert &overflow)
{
// First figure out what the appropriate type for this expression is.
typet expr_type=nil_typet();
optionalt<typet> expr_type;

for(std::map<exprt, int>::iterator it=values.begin();
it!=values.end();
Expand All @@ -523,25 +523,26 @@ void polynomial_acceleratort::assert_for_values(
this_type=size_type();
}

if(expr_type==nil_typet())
if(!expr_type.has_value())
{
expr_type=this_type;
}
else
{
expr_type=join_types(expr_type, this_type);
expr_type = join_types(*expr_type, this_type);
}
}

assert(to_bitvector_type(expr_type).get_width()>0);

INVARIANT(
to_bitvector_type(*expr_type).get_width() > 0,
"joined types must be non-empty bitvector types");

// Now set the initial values of the all the variables...
for(std::map<exprt, int>::iterator it=values.begin();
it!=values.end();
++it)
{
program.assign(it->first, from_integer(it->second, expr_type));
program.assign(it->first, from_integer(it->second, *expr_type));
}

// Now unwind the loop as many times as we need to.
Expand Down Expand Up @@ -583,8 +584,8 @@ void polynomial_acceleratort::assert_for_values(
// OK, concrete_value now contains the value of all the relevant variables
// multiplied together. Create the term concrete_value*coefficient and add
// it into the polynomial.
typecast_exprt cast(it->second, expr_type);
const mult_exprt term(from_integer(concrete_value, expr_type), cast);
typecast_exprt cast(it->second, *expr_type);
const mult_exprt term(from_integer(concrete_value, *expr_type), cast);

if(rhs.is_nil())
{
Expand Down