Skip to content

Commit b2fba97

Browse files
martinmartin
martin
authored and
martin
committed
Correct domain transformers so that they meet the preconditions.
This will eliminate issues with non-comparable iterators being compared and tidies a few things.
1 parent d447c26 commit b2fba97

6 files changed

+17
-16
lines changed

src/analyses/constant_propagator.cpp

+7-4
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,8 @@ void constant_propagator_domaint::transform(
9393
{
9494
exprt g;
9595

96+
// Comparing iterators is safe as the target must be within the same list
97+
// of instructions because this is a GOTO.
9698
if(from->get_target()==to)
9799
g=simplify_expr(from->guard, ns);
98100
else
@@ -121,15 +123,14 @@ void constant_propagator_domaint::transform(
121123
const code_function_callt &function_call=to_code_function_call(from->code);
122124
const exprt &function=function_call.function();
123125

124-
const locationt& next=std::next(from);
125-
126126
if(function.id()==ID_symbol)
127127
{
128128
// called function identifier
129129
const symbol_exprt &symbol_expr=to_symbol_expr(function);
130130
const irep_idt id=symbol_expr.get_identifier();
131131

132-
if(to==next)
132+
// Functions with no body
133+
if(from->function == to->function)
133134
{
134135
if(id==CPROVER_PREFIX "set_must" ||
135136
id==CPROVER_PREFIX "get_must" ||
@@ -177,7 +178,9 @@ void constant_propagator_domaint::transform(
177178
else
178179
{
179180
// unresolved call
180-
INVARIANT(to==next, "Unresolved call can only be approximated if a skip");
181+
INVARIANT(
182+
from->function == to->function,
183+
"Unresolved call can only be approximated if a skip");
181184

182185
if(have_dirty)
183186
values.set_dirty_to_top(cp->dirty, ns);

src/analyses/custom_bitvector_analysis.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -395,11 +395,8 @@ void custom_bitvector_domaint::transform(
395395
}
396396
else
397397
{
398-
goto_programt::const_targett next=from;
399-
++next;
400-
401398
// only if there is an actual call, i.e., we have a body
402-
if(next!=to)
399+
if(from->function != to->function)
403400
{
404401
const code_typet &code_type=
405402
to_code_type(ns.lookup(identifier).type);
@@ -522,6 +519,8 @@ void custom_bitvector_domaint::transform(
522519
{
523520
exprt guard=instruction.guard;
524521

522+
// Comparing iterators is safe as the target must be within the same list
523+
// of instructions because this is a GOTO.
525524
if(to!=from->get_target())
526525
guard.make_not();
527526

src/analyses/dependence_graph.cpp

+2-4
Original file line numberDiff line numberDiff line change
@@ -195,16 +195,14 @@ void dep_graph_domaint::transform(
195195
// propagate control dependencies across function calls
196196
if(from->is_function_call())
197197
{
198-
goto_programt::const_targett next=from;
199-
++next;
200-
201-
if(next==to)
198+
if(from->function == to->function)
202199
{
203200
control_dependencies(from, to, *dep_graph);
204201
}
205202
else
206203
{
207204
// edge to function entry point
205+
const goto_programt::const_targett next = std::next(from);
208206

209207
dep_graph_domaint *s=
210208
dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));

src/analyses/interval_domain.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,8 @@ void interval_domaint::transform(
7878

7979
case GOTO:
8080
{
81+
// Comparing iterators is safe as the target must be within the same list
82+
// of instructions because this is a GOTO.
8183
locationt next=from;
8284
next++;
8385
if(next==to)

src/analyses/invariant_set_domain.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,8 @@ void invariant_set_domaint::transform(
2323
{
2424
case GOTO:
2525
{
26+
// Comparing iterators is safe as the target must be within the same list
27+
// of instructions because this is a GOTO.
2628
exprt tmp(from_l->guard);
2729

2830
goto_programt::const_targett next=from_l;

src/analyses/reaching_definitions.cpp

+1-4
Original file line numberDiff line numberDiff line change
@@ -173,11 +173,8 @@ void rd_range_domaint::transform_function_call(
173173
{
174174
const code_function_callt &code=to_code_function_call(from->code);
175175

176-
goto_programt::const_targett next=from;
177-
++next;
178-
179176
// only if there is an actual call, i.e., we have a body
180-
if(next!=to)
177+
if(from->function != to->function)
181178
{
182179
for(valuest::iterator it=values.begin();
183180
it!=values.end();

0 commit comments

Comments
 (0)