Skip to content

Commit 03d1517

Browse files
author
Daniel Kroening
committed
introduce non-const instructiont::get_condition()
This will eventually allow us to protect the guard data member.
1 parent f34ad06 commit 03d1517

File tree

2 files changed

+10
-2
lines changed

2 files changed

+10
-2
lines changed

src/analyses/constant_propagator.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -756,11 +756,12 @@ void constant_propagator_ait::replace(
756756
continue;
757757

758758
replace_types_rec(d.values.replace_const, it->code);
759-
replace_types_rec(d.values.replace_const, it->guard);
760759

761760
if(it->is_goto() || it->is_assume() || it->is_assert())
762761
{
763-
constant_propagator_domaint::partial_evaluate(d.values, it->guard, ns);
762+
replace_types_rec(d.values.replace_const, it->get_condition());
763+
constant_propagator_domaint::partial_evaluate(
764+
d.values, it->get_condition(), ns);
764765
}
765766
else if(it->is_assign())
766767
{

src/goto-programs/goto_program.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -287,6 +287,13 @@ class goto_programt
287287
return guard;
288288
}
289289

290+
/// Get the condition of gotos, assume, assert
291+
exprt &get_condition()
292+
{
293+
PRECONDITION(has_condition());
294+
return guard;
295+
}
296+
290297
// The below will eventually become a single target only.
291298
/// The target for gotos and for start_thread nodes
292299
typedef std::list<instructiont>::iterator targett;

0 commit comments

Comments
 (0)