CBMC
Loading...
Searching...
No Matches
constant_propagator.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Constant propagation
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "constant_propagator.h"
13
15
16#ifdef DEBUG
17#include <iostream>
18#include <util/format_expr.h>
19#endif
20
21#include <util/arith_tools.h>
22#include <util/c_types.h>
23#include <util/cprover_prefix.h>
24#include <util/expr_util.h>
25#include <util/ieee_float.h>
27#include <util/simplify_expr.h>
28#include <util/std_code.h>
29
31
32#include <array>
33
54 const exprt &lhs,
55 const exprt &rhs,
56 const namespacet &ns,
58 bool is_assignment)
59{
60 if(lhs.id() == ID_dereference)
61 {
62 exprt eval_lhs = lhs;
64 {
65 if(is_assignment)
66 {
67 const bool have_dirty = (cp != nullptr);
68
69 if(have_dirty)
70 dest_values.set_dirty_to_top(cp->dirty, ns);
71 else
72 dest_values.set_to_top();
73 }
74 // Otherwise disregard this unknown deref in a read-only context.
75 }
76 else
77 assign_rec(dest_values, eval_lhs, rhs, ns, cp, is_assignment);
78 }
79 else if(lhs.id() == ID_index)
80 {
82 with_exprt new_rhs(index_expr.array(), index_expr.index(), rhs);
83 assign_rec(dest_values, index_expr.array(), new_rhs, ns, cp, is_assignment);
84 }
85 else if(lhs.id() == ID_member)
86 {
89 new_rhs.where().set(ID_component_name, member_expr.get_component_name());
91 dest_values, member_expr.compound(), new_rhs, ns, cp, is_assignment);
92 }
93 else if(lhs.id() == ID_symbol)
94 {
95 if(cp && !cp->should_track_value(lhs, ns))
96 return;
97
98 const symbol_exprt &s = to_symbol_expr(lhs);
99
100 exprt tmp = rhs;
102
103 if(dest_values.is_constant(tmp, ns))
104 {
106 ns.lookup(s).type == tmp.type(),
107 "type of constant to be replaced should match");
108 dest_values.set_to(s, tmp);
109 }
110 else
111 {
112 if(is_assignment)
113 dest_values.set_to_top(s);
114 }
115 }
116 else if(is_assignment)
117 {
118 // it's an assignment, but we don't really know what object is being written
119 // to: assume it may write to anything.
120 dest_values.set_to_top();
121 }
122}
123
125 const irep_idt &function_from,
127 const irep_idt &function_to,
129 ai_baset &ai,
130 const namespacet &ns)
131{
132 locationt from{trace_from->current_location()};
133 locationt to{trace_to->current_location()};
134
135#ifdef DEBUG
136 std::cout << "Transform from/to:\n";
137 std::cout << from->location_number << " --> "
138 << to->location_number << '\n';
139#endif
140
141#ifdef DEBUG
142 std::cout << "Before:\n";
143 output(std::cout, ai, ns);
144#endif
145
146 // When the domain is used with constant_propagator_ait,
147 // information about dirty variables and config flags are
148 // available. Otherwise, the below will be null and we use default
149 // values
151 dynamic_cast<constant_propagator_ait *>(&ai);
152 bool have_dirty=(cp!=nullptr);
153
154 // Transform on a domain that is bottom is possible
155 // if a branch is impossible the target can still wind
156 // up on the work list.
157 if(values.is_bottom)
158 return;
159
160 if(from->is_decl())
161 {
162 const symbol_exprt &symbol = from->decl_symbol();
163 values.set_to_top(symbol);
164 }
165 else if(from->is_assign())
166 {
167 const exprt &lhs = from->assign_lhs();
168 const exprt &rhs = from->assign_rhs();
169 assign_rec(values, lhs, rhs, ns, cp, true);
170 }
171 else if(from->is_assume())
172 {
173 two_way_propagate_rec(from->condition(), ns, cp);
174 }
175 else if(from->is_goto())
176 {
177 exprt g;
178
179 // Comparing iterators is safe as the target must be within the same list
180 // of instructions because this is a GOTO.
181 if(from->get_target()==to)
182 g = from->condition();
183 else
184 g = not_exprt(from->condition());
186 if(g.is_false())
188 else
190 }
191 else if(from->is_dead())
192 {
193 values.set_to_top(from->dead_symbol());
194 }
195 else if(from->is_function_call())
196 {
197 const exprt &function = from->call_function();
198
199 if(function.id()==ID_symbol)
200 {
201 // called function identifier
202 const symbol_exprt &symbol_expr=to_symbol_expr(function);
203 const irep_idt id=symbol_expr.get_identifier();
204
205 // Functions with no body
207 {
208 if(id==CPROVER_PREFIX "set_must" ||
209 id==CPROVER_PREFIX "get_must" ||
210 id==CPROVER_PREFIX "set_may" ||
211 id==CPROVER_PREFIX "get_may" ||
212 id==CPROVER_PREFIX "cleanup" ||
213 id==CPROVER_PREFIX "clear_may" ||
214 id==CPROVER_PREFIX "clear_must")
215 {
216 // no effect on constants
217 }
218 else
219 {
220 if(have_dirty)
221 values.set_dirty_to_top(cp->dirty, ns);
222 else
224 }
225 }
226 else
227 {
228 // we have an actual call
229
230 // parameters of called function
231 const symbolt &symbol=ns.lookup(id);
232 const code_typet &code_type=to_code_type(symbol.type);
233 const code_typet::parameterst &parameters=code_type.parameters();
234
235 const code_function_callt::argumentst &arguments =
236 from->call_arguments();
237
238 code_typet::parameterst::const_iterator p_it=parameters.begin();
239 for(const auto &arg : arguments)
240 {
241 if(p_it==parameters.end())
242 break;
243
244 const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
245 assign_rec(values, parameter_expr, arg, ns, cp, true);
246
247 ++p_it;
248 }
249 }
250 }
251 else
252 {
253 // unresolved call
254 INVARIANT(
256 "Unresolved call can only be approximated if a skip");
257
258 if(have_dirty)
259 values.set_dirty_to_top(cp->dirty, ns);
260 else
262 }
263 }
264 else if(from->is_end_function())
265 {
266 // erase parameters
267
268 const irep_idt id = function_from;
269 const symbolt &symbol=ns.lookup(id);
270
271 const code_typet &type=to_code_type(symbol.type);
272
273 for(const auto &param : type.parameters())
274 values.set_to_top(symbol_exprt(param.get_identifier(), param.type()));
275 }
276
277 INVARIANT(from->is_goto() || !values.is_bottom,
278 "Transform only sets bottom by using branch conditions");
279
280#ifdef DEBUG
281 std::cout << "After:\n";
282 output(std::cout, ai, ns);
283#endif
284}
285
286static void
288{
289 // (int)var xx 0 ==> var xx (_Bool)0 or similar (xx is == or !=)
290 // Note this is restricted to bools because in general turning a widening
291 // into a narrowing typecast is not correct.
292 if(lhs.id() != ID_typecast)
293 return;
294
295 const exprt &lhs_underlying = to_typecast_expr(lhs).op();
296 if(
297 lhs_underlying.type() == bool_typet() ||
298 lhs_underlying.type() == c_bool_type())
299 {
300 rhs = typecast_exprt(rhs, lhs_underlying.type());
301 simplify(rhs, ns);
302
303 lhs = lhs_underlying;
304 }
305}
306
309 const exprt &expr,
310 const namespacet &ns,
312{
313#ifdef DEBUG
314 std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
315#endif
316
317 bool change=false;
318
319 if(expr.id()==ID_and)
320 {
321 // need a fixed point here to get the most out of it
322 bool change_this_time;
323 do
324 {
325 change_this_time = false;
326
327 for(const auto &op : expr.operands())
328 {
331 change = true;
332 }
333 } while(change_this_time);
334 }
335 else if(expr.id() == ID_not)
336 {
337 const auto &op = to_not_expr(expr).op();
338
339 if(op.id() == ID_equal || op.id() == ID_notequal)
340 {
341 exprt subexpr = op;
344 }
345 else if(op.id() == ID_symbol && expr.type() == bool_typet())
346 {
347 // Treat `IF !x` like `IF x == FALSE`:
349 }
350 }
351 else if(expr.id() == ID_symbol)
352 {
353 if(expr.type() == bool_typet())
354 {
355 // Treat `IF x` like `IF x == TRUE`:
357 }
358 }
359 else if(expr.id() == ID_notequal)
360 {
361 // Treat "symbol != constant" like "symbol == !constant" when the constant
362 // is a boolean.
363 exprt lhs = to_notequal_expr(expr).lhs();
364 exprt rhs = to_notequal_expr(expr).rhs();
365
366 if(lhs.is_constant() && !rhs.is_constant())
367 std::swap(lhs, rhs);
368
369 if(lhs.is_constant() || !rhs.is_constant())
370 return false;
371
372 replace_typecast_of_bool(lhs, rhs, ns);
373
374 if(lhs.type() != bool_typet() && lhs.type() != c_bool_type())
375 return false;
376
377 // x != FALSE ==> x == TRUE
378
379 if(rhs.is_zero() || rhs.is_false())
380 rhs = from_integer(1, rhs.type());
381 else
382 rhs = from_integer(0, rhs.type());
383
384 change = two_way_propagate_rec(equal_exprt(lhs, rhs), ns, cp);
385 }
386 else if(expr.id() == ID_equal)
387 {
388 exprt lhs = to_equal_expr(expr).lhs();
389 exprt rhs = to_equal_expr(expr).rhs();
390
391 replace_typecast_of_bool(lhs, rhs, ns);
392
393 // two-way propagation
395 assign_rec(copy_values, lhs, rhs, ns, cp, false);
396 if(!values.is_constant(rhs, ns) || values.is_constant(lhs, ns))
397 assign_rec(values, rhs, lhs, ns, cp, false);
399 }
400
401#ifdef DEBUG
402 std::cout << "two_way_propagate_rec: " << change << '\n';
403#endif
404
405 return change;
406}
407
413 exprt &condition,
414 const namespacet &ns) const
415{
416 return partial_evaluate(values, condition, ns);
417}
418
420{
421public:
428
429 bool is_constant(const irep_idt &id) const
430 {
431 return replace_const.replaces_symbol(id);
432 }
433
434protected:
435 bool is_constant(const exprt &expr) const override
436 {
437 if(expr.id() == ID_symbol)
438 return is_constant(to_symbol_expr(expr).get_identifier());
439
441 }
442
444};
445
447 const exprt &expr,
448 const namespacet &ns) const
449{
451}
452
454 const irep_idt &id,
455 const namespacet &ns) const
456{
457 return constant_propagator_can_forward_propagatet(replace_const, ns)
458 .is_constant(id);
459}
460
463 const symbol_exprt &symbol_expr)
464{
465 const auto n_erased = replace_const.erase(symbol_expr.get_identifier());
466
467 INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all");
468
469 return n_erased>0;
470}
471
472
474 const dirtyt &dirty,
475 const namespacet &ns)
476{
478 expr_mapt &expr_map = replace_const.get_expr_map();
479
480 for(expr_mapt::iterator it=expr_map.begin();
481 it!=expr_map.end();)
482 {
483 const irep_idt id=it->first;
484
485 const symbolt &symbol=ns.lookup(id);
486
487 if(
488 (symbol.is_static_lifetime || dirty(id)) &&
489 !symbol.type.get_bool(ID_C_constant))
490 {
491 it = replace_const.erase(it);
492 }
493 else
494 it++;
495 }
496}
497
499 std::ostream &out,
500 const namespacet &ns) const
501{
502 out << "const map:\n";
503
504 if(is_bottom)
505 {
506 out << " bottom\n";
508 "If the domain is bottom, the map must be empty");
509 return;
510 }
511
512 INVARIANT(!is_bottom, "Have handled bottom");
513 if(is_empty())
514 {
515 out << "top\n";
516 return;
517 }
518
519 for(const auto &p : replace_const.get_expr_map())
520 {
521 out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n';
522 }
523}
524
526 std::ostream &out,
527 const ai_baset &,
528 const namespacet &ns) const
529{
530 values.output(out, ns);
531}
532
536{
537 // nothing to do
538 if(src.is_bottom)
539 return false;
540
541 // just copy
542 if(is_bottom)
543 {
545 replace_const=src.replace_const; // copy
546 is_bottom=false;
547 return true;
548 }
549
550 INVARIANT(!is_bottom && !src.is_bottom, "Case handled");
551
552 bool changed=false;
553
554 // handle top
555 if(src.is_empty())
556 {
557 // change if it was not top
558 changed = !is_empty();
559
560 set_to_top();
561
562 return changed;
563 }
564
565 replace_symbolt::expr_mapt &expr_map = replace_const.get_expr_map();
568
569 // remove those that are
570 // - different in src
571 // - do not exist in src
572 for(replace_symbolt::expr_mapt::iterator it=expr_map.begin();
573 it!=expr_map.end();)
574 {
575 const irep_idt id=it->first;
576 const exprt &expr=it->second;
577
578 replace_symbolt::expr_mapt::const_iterator s_it;
579 s_it=src_expr_map.find(id);
580
581 if(s_it!=src_expr_map.end())
582 {
583 // check value
584 const exprt &src_expr=s_it->second;
585
586 if(expr!=src_expr)
587 {
588 it = replace_const.erase(it);
589 changed=true;
590 }
591 else
592 it++;
593 }
594 else
595 {
596 it = replace_const.erase(it);
597 changed=true;
598 }
599 }
600
601 return changed;
602}
603
607 const valuest &src,
608 const namespacet &ns)
609{
610 if(src.is_bottom || is_bottom)
611 return false;
612
613 bool changed=false;
614
615 for(const auto &m : src.replace_const.get_expr_map())
616 {
617 replace_symbolt::expr_mapt::const_iterator c_it =
618 replace_const.get_expr_map().find(m.first);
619
620 if(c_it != replace_const.get_expr_map().end())
621 {
622 if(c_it->second!=m.second)
623 {
624 set_to_bottom();
625 changed=true;
626 break;
627 }
628 }
629 else
630 {
631 const typet &m_id_type = ns.lookup(m.first).type;
633 m_id_type == m.second.type(),
634 "type of constant to be stored should match");
635 set_to(symbol_exprt(m.first, m_id_type), m.second);
636 changed=true;
637 }
638 }
639
640 return changed;
641}
642
645 const constant_propagator_domaint &other,
648{
649 return values.merge(other.values);
650}
651
659 const valuest &known_values,
660 exprt &expr,
661 const namespacet &ns)
662{
663 // if the current rounding mode is top we can
664 // still get a non-top result by trying all rounding
665 // modes and checking if the results are all the same
666 if(!known_values.is_constant(rounding_mode_identifier(), ns))
668
670}
671
680 const valuest &known_values,
681 exprt &expr,
682 const namespacet &ns)
683{ // NOLINTNEXTLINE (whitespace/braces)
684 auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
685 // NOLINTNEXTLINE (whitespace/braces)
689 // NOLINTNEXTLINE (whitespace/braces)
692 for(std::size_t i = 0; i < rounding_modes.size(); ++i)
693 {
695 tmp_values.set_to(
697 from_integer(rounding_modes[i], integer_typet()));
698 exprt result = expr;
700 {
701 return true;
702 }
703 else if(i == 0)
704 {
705 first_result = result;
706 }
707 else if(result != first_result)
708 {
709 return true;
710 }
711 }
712 expr = first_result;
713 return false;
714}
715
717 const valuest &known_values,
718 exprt &expr,
719 const namespacet &ns)
720{
721 bool did_not_change_anything = true;
722
723 // iterate constant propagation and simplification until we cannot
724 // constant-propagate any further - a prime example is pointer dereferencing,
725 // where constant propagation may have a value of the pointer, the simplifier
726 // takes care of evaluating dereferencing, and we might then have the value of
727 // the resulting symbol known to constant propagation and thus replace the
728 // dereferenced expression by a constant
729 while(!known_values.replace_const.replace(expr))
730 {
732 simplify(expr, ns);
733 }
734
735 // even if we haven't been able to constant-propagate anything, run the
736 // simplifier on the expression
739
741}
742
744 goto_functionst &goto_functions,
745 const namespacet &ns)
746{
747 for(auto &gf_entry : goto_functions.function_map)
748 replace(gf_entry.second, ns);
749}
750
751
753 goto_functionst::goto_functiont &goto_function,
754 const namespacet &ns)
755{
756 Forall_goto_program_instructions(it, goto_function.body)
757 {
758 auto const current_domain_ptr =
759 std::dynamic_pointer_cast<const constant_propagator_domaint>(
760 this->abstract_state_before(it));
762
763 if(d.is_bottom())
764 continue;
765
766 replace_types_rec(d.values.replace_const, it->code_nonconst());
767
768 if(it->is_goto() || it->is_assume() || it->is_assert())
769 {
770 exprt c = it->condition();
771 replace_types_rec(d.values.replace_const, c);
773 it->condition_nonconst() = c;
774 }
775 else if(it->is_assign())
776 {
777 exprt &rhs = it->assign_rhs_nonconst();
778
780 {
781 if(rhs.is_constant())
782 rhs.add_source_location() = it->assign_lhs().source_location();
783 }
784 }
785 else if(it->is_function_call())
786 {
788 d.values, it->call_function(), ns);
789
790 for(auto &arg : it->call_arguments())
792 }
793 else if(it->is_other())
794 {
795 if(it->get_other().get_statement() == ID_expression)
796 {
797 auto c = to_code_expression(it->get_other());
799 d.values, c.expression(), ns))
800 {
801 it->set_other(c);
802 }
803 }
804 }
805 }
806}
807
809 const replace_symbolt &replace_const,
810 exprt &expr)
811{
812 replace_const(expr.type());
813
814 Forall_operands(it, expr)
815 replace_types_rec(replace_const, *it);
816}
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
typet c_bool_type()
Definition c_types.cpp:100
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:73
goto_programt::const_targett locationt
Definition ai_domain.h:72
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
The Boolean type.
Definition std_types.h:36
Determine whether an expression is constant.
Definition expr_util.h:87
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
const namespacet & ns
Definition expr_util.h:100
Base type of functions.
Definition std_types.h:583
std::vector< parametert > parameterst
Definition std_types.h:586
const parameterst & parameters() const
Definition std_types.h:699
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
void replace(goto_functionst::goto_functiont &, const namespacet &)
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
constant_propagator_can_forward_propagatet(const replace_symbolt &replace_const, const namespacet &ns)
static void assign_rec(valuest &dest_values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp, bool is_assignment)
Assign value rhs to lhs, recording any newly-known constants in dest_values.
virtual bool is_bottom() const final override
static bool partial_evaluate(const valuest &known_values, exprt &expr, const namespacet &ns)
Attempt to evaluate expression using domain knowledge This function changes the expression that is pa...
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const final override
Simplify the condition given context-sensitive knowledge from the abstract state.
static bool partial_evaluate_with_all_rounding_modes(const valuest &known_values, exprt &expr, const namespacet &ns)
Attempt to evaluate an expression in all rounding modes.
virtual void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai_base, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
static bool replace_constants_and_simplify(const valuest &known_values, exprt &expr, const namespacet &ns)
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
bool merge(const constant_propagator_domaint &other, trace_ptrt from, trace_ptrt to)
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition dirty.h:28
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
source_locationt & add_source_location()
Definition expr.h:236
The Boolean constant false.
Definition std_expr.h:3200
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
Array index operator.
Definition std_expr.h:1470
Unbounded, signed integers (mathematical integers, not bitvectors)
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irep_idt & id() const
Definition irep.h:388
Extract member of struct or union.
Definition std_expr.h:2972
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Boolean negation.
Definition std_expr.h:2459
Replace a symbol expression by a given expression.
const expr_mapt & get_expr_map() const
std::unordered_map< irep_idt, exprt > expr_mapt
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
typet type
Type of symbol.
Definition symbol.h:31
The Boolean constant true.
Definition std_expr.h:3191
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
Operator to update elements in structs and arrays.
Definition std_expr.h:2603
static void replace_typecast_of_bool(exprt &lhs, exprt &rhs, const namespacet &ns)
Constant propagation.
#define CPROVER_PREFIX
#define Forall_operands(it, expr)
Definition expr.h:27
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition format.h:37
static bool is_empty(const goto_programt &goto_program)
#define Forall_goto_program_instructions(it, program)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Mathematical types.
bool simplify(exprt &expr, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
code_expressiont & to_code_expression(codet &code)
Definition std_code.h:1428
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition std_expr.h:1450
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2484
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1407
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
bool is_constant(const exprt &expr, const namespacet &ns) const
bool meet(const valuest &src, const namespacet &ns)
meet
void output(std::ostream &out, const namespacet &ns) const
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
address_of_aware_replace_symbolt replace_const