CBMC
Loading...
Searching...
No Matches
axioms.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Axioms
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#include "axioms.h"
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/format_expr.h>
17#include <util/namespace.h>
21#include <util/symbol.h>
22
24
25#include "simplify_state_expr.h"
26
27#include <iostream>
28
30{
31 constraints.push_back(std::move(src));
32}
33
38
40{
41 if(src.id() == ID_array)
42 {
43 auto &array_type = to_array_type(src);
44 array_type.element_type() = replace(array_type.element_type());
45 array_type.size() = replace(array_type.size());
46 return src;
47 }
48 else if(src.id() == ID_pointer)
49 {
50 to_pointer_type(src).base_type() =
51 replace(to_pointer_type(src).base_type());
52 return src;
53 }
54 else
55 return src;
56}
57
59{
60 // quadratic
61 for(auto a_it = evaluate_exprs.begin(); a_it != evaluate_exprs.end(); a_it++)
62 {
63 for(auto b_it = std::next(a_it); b_it != evaluate_exprs.end(); b_it++)
64 {
65 if(a_it->state() != b_it->state())
66 continue;
67
68 auto a_op = a_it->address();
70 b_it->address(), a_it->address().type());
76#if 0
77 if(verbose)
78 std::cout << "EVALUATE: " << format(implication) << '\n';
79#endif
81 }
82 }
83}
84
86{
87 // quadratic
88 for(auto a_it = is_cstring_exprs.begin(); a_it != is_cstring_exprs.end();
89 a_it++)
90 {
91 for(auto b_it = std::next(a_it); b_it != is_cstring_exprs.end(); b_it++)
92 {
93 if(a_it->state() != b_it->state())
94 continue;
95 auto a_op = a_it->address();
97 b_it->address(), a_it->address().type());
99 auto implication =
101 if(verbose)
102 std::cout << "IS_CSTRING: " << format(implication) << '\n';
104 }
105 }
106}
107
109{
110 // p = &"string_literal" -> live_object(ς, p)
111 for(auto a_it = live_object_exprs.begin(); a_it != live_object_exprs.end();
112 a_it++)
113 {
114 for(auto b_it = address_of_exprs.begin(); b_it != address_of_exprs.end();
115 b_it++)
116 {
117 auto pointers_equal = same_object(a_it->address(), *b_it);
119 if(verbose)
120 std::cout << "LIVE_OBJECT2: " << format(implication) << '\n';
122 }
123 }
124}
125
127{
128 // quadratic
129 for(auto a_it = live_object_exprs.begin(); a_it != live_object_exprs.end();
130 a_it++)
131 {
132 for(auto b_it = std::next(a_it); b_it != live_object_exprs.end(); b_it++)
133 {
134 if(a_it->state() != b_it->state())
135 continue;
136 auto operands_equal = same_object(a_it->address(), b_it->address());
137 auto implication =
139 if(verbose)
140 std::cout << "LIVE_OBJECT1: " << format(implication) << '\n';
142 }
143 }
144}
145
147{
148 // p = &"string_literal" -> !writeable_object(ς, p)
149 for(auto a_it = writeable_object_exprs.begin();
151 a_it++)
152 {
153 for(auto b_it = address_of_exprs.begin(); b_it != address_of_exprs.end();
154 b_it++)
155 {
156 auto pointers_equal = same_object(a_it->address(), *b_it);
158 if(verbose)
159 std::cout << "WRITEABLE_OBJECT2: " << format(implication) << '\n';
161 }
162 }
163
164 // p = &some_object -> writeable_object(ς, p) as applicable
165 for(auto a_it = object_address_exprs.begin();
166 a_it != object_address_exprs.end();
167 a_it++)
168 {
169 if(a_it->object_identifier() == "return_value")
170 continue;
171 else if(a_it->object_identifier().starts_with("va_args::"))
172 continue;
173 else if(a_it->object_identifier().starts_with("va_arg::"))
174 continue;
175 else if(a_it->object_identifier().starts_with("va_arg_array::"))
176 continue;
177 else if(a_it->object_identifier().starts_with("old::"))
178 continue;
179
180 auto &symbol = ns.lookup(a_it->object_expr());
181 bool is_const = symbol.type.get_bool(ID_C_constant);
182 for(auto b_it = writeable_object_exprs.begin();
184 b_it++)
185 {
186 auto pointers_equal = same_object(*a_it, b_it->address());
187 auto rhs = is_const ? static_cast<exprt>(not_exprt(*b_it))
188 : static_cast<exprt>(*b_it);
190 if(verbose)
191 std::cout << "WRITEABLE_OBJECT3: " << format(implication) << '\n';
193 }
194 }
195}
196
198{
199 // quadratic
200 for(auto a_it = writeable_object_exprs.begin();
202 a_it++)
203 {
204 for(auto b_it = std::next(a_it); b_it != writeable_object_exprs.end();
205 b_it++)
206 {
207 if(a_it->state() != b_it->state())
208 continue;
209 auto operands_equal = same_object(a_it->address(), b_it->address());
210 auto implication =
212 if(verbose)
213 std::cout << "WRITEABLE_OBJECT1: " << format(implication) << '\n';
215 }
216 }
217}
218
220{
221 // quadratic
222 for(auto a_it = is_dynamic_object_exprs.begin();
224 a_it++)
225 {
226 for(auto b_it = std::next(a_it); b_it != is_dynamic_object_exprs.end();
227 b_it++)
228 {
229 if(a_it->state() != b_it->state())
230 continue;
231 auto operands_equal = same_object(a_it->address(), b_it->address());
232 auto implication =
234 if(verbose)
235 std::cout << "IS_DYNAMIC_OBJECT: " << format(implication) << '\n';
237 }
238 }
239}
240
242{
243 for(const auto &src : object_size_exprs)
244 {
246 if(src_simplified != src)
247 {
248 auto equal = equal_exprt(src, src_simplified);
249 if(verbose)
250 std::cout << "OBJECT_SIZE1: " << format(equal) << '\n';
251 dest << replace(equal);
252 }
253 }
254
255 // p = &"string_literal" -> object_size(ς, p) = strlen("string_literal")+1
256 for(auto a_it = object_size_exprs.begin(); a_it != object_size_exprs.end();
257 a_it++)
258 {
259 for(auto b_it = address_of_exprs.begin(); b_it != address_of_exprs.end();
260 b_it++)
261 {
262 if(b_it->object().id() == ID_string_constant)
263 {
264 auto &string_constant = to_string_constant(b_it->object());
265 auto pointers_equal = same_object(a_it->address(), *b_it);
266 auto size_equal = equal_exprt(
267 *a_it,
268 from_integer(string_constant.value().size() + 1, a_it->type()));
270 if(verbose)
271 std::cout << "OBJECT_SIZE2: " << format(implication) << '\n';
273 }
274 }
275 }
276}
277
279{
280 // quadratic
281 for(auto a_it = object_size_exprs.begin(); a_it != object_size_exprs.end();
282 a_it++)
283 {
284 for(auto b_it = std::next(a_it); b_it != object_size_exprs.end(); b_it++)
285 {
286 if(a_it->state() != b_it->state())
287 continue;
288 auto operands_equal = same_object(a_it->address(), b_it->address());
289 auto implication =
291 if(verbose)
292 std::cout << "OBJECT_SIZE: " << format(implication) << '\n';
294 }
295 }
296}
297
299{
300 // quadratic
301 for(auto a_it = ok_exprs.begin(); a_it != ok_exprs.end(); a_it++)
302 {
303 for(auto b_it = std::next(a_it); b_it != ok_exprs.end(); b_it++)
304 {
305 if(a_it->id() != b_it->id())
306 continue;
307 if(a_it->state() != b_it->state())
308 continue;
309 if(a_it->size() != b_it->size())
310 continue;
311 auto a_op = a_it->address();
313 b_it->address(), a_it->address().type());
315 auto implication =
317 if(verbose)
318 std::cout << "OK: " << format(implication) << '\n';
320 }
321 }
322}
323
325{
326 for(const auto &initial_state_expr : initial_state_exprs)
327 {
328 // initial_state(ς) -> ¬live_object(ς, o) for any stack-allocated object o
329 for(const auto &object : address_taken)
330 {
331 const symbolt *symbol;
332 if(ns.lookup(object.get_identifier(), symbol))
333 continue;
334
335 if(symbol->is_static_lifetime || !symbol->is_lvalue)
336 continue;
337
341 auto implication =
343 if(verbose)
344 std::cout << "INITIAL_STATE: " << format(implication) << '\n';
346 }
347 }
348}
349
351{
352 auto r = replacement_map.find(src);
353 if(r == replacement_map.end())
354 return src;
355 else
356 return r->second;
357}
358
360{
361 src.type() = replace(src.type());
362
363 if(
364 src.id() == ID_initial_state || src.id() == ID_evaluate ||
365 src.id() == ID_state_is_cstring || src.id() == ID_state_cstrlen ||
366 src.id() == ID_state_is_sentinel_dll ||
368 src.id() == ID_state_object_size || src.id() == ID_state_live_object ||
369 src.id() == ID_state_writeable_object || src.id() == ID_state_r_ok ||
370 src.id() == ID_state_w_ok || src.id() == ID_state_rw_ok ||
371 src.id() == ID_allocate || src.id() == ID_reallocate)
372 {
373 auto r = replacement_map.find(src);
374 if(r == replacement_map.end())
375 {
376 auto counter = ++counters[src.id()];
377 auto s =
378 symbol_exprt(src.id_string() + std::to_string(counter), src.type());
379 replacement_map.emplace(src, s);
380
381 if(src.id() == ID_state_is_cstring)
382 {
383 if(verbose)
384 std::cout << "R " << format(s) << " --> " << format(src) << '\n';
385 }
386
387 return std::move(s);
388 }
389 else
390 return r->second;
391 }
392
393 for(auto &op : src.operands())
394 op = replace(op);
395
396 return src;
397}
398
399void axiomst::node(const exprt &src)
400{
401 if(src.id() == ID_state_is_cstring)
402 {
403 add(to_state_is_cstring_expr(src), false);
404 }
405 else if(src.id() == ID_state_is_sentinel_dll)
406 {
409
411 to_pointer_type(is_sentinel_dll_expr.head().type()).base_type(), ns);
412
415 is_sentinel_dll_expr.state(),
418
420 to_pointer_type(is_sentinel_dll_expr.tail().type()).base_type(), ns);
421
424 is_sentinel_dll_expr.state(),
427
428 {
429 // is_sentinel_dll(ς, h, t) ⇒ rw_ok(ς, h) ∧ rw_ok(ς, t)
430 auto instance1 =
432 if(verbose)
433 std::cout << "AXIOM-is-sentinel-dll-1: " << format(instance1) << "\n";
434 dest << instance1;
435 }
436
437 {
438 // rw_ok(h) ∧ rw_ok(t) ∧ ς(h->n)=t ∧ ς(t->p)=h ⇒ is_sentinel_dll(ς, h, t)
441
444
445 if(head_next.has_value() && tail_prev.has_value())
446 {
447 auto head_next_is_tail =
449
450 auto tail_prev_is_head =
452
454 and_exprt(
455 ok_expr_h, ok_expr_t /*, head_next_is_tail, tail_prev_is_head*/),
456 src));
457
458 if(verbose)
459 std::cout << "AXIOM-is-sentinel-dll-2: " << format(instance2) << "\n";
460 dest << instance2;
461 }
462 }
463 }
464 else if(src.id() == ID_evaluate)
465 {
466 const auto &evaluate_expr = to_evaluate_expr(src);
467 evaluate_exprs.insert(evaluate_expr);
468 }
469 else if(src.id() == ID_state_live_object)
470 {
473
474 {
475 // live_object(ς, p) --> p!=0
476 auto instance = replace(
478 if(verbose)
479 std::cout << "AXIOMc: " << format(instance) << "\n";
480 dest << instance;
481 }
482 }
483 else if(src.id() == ID_state_writeable_object)
484 {
487 }
488 else if(src.id() == ID_state_is_dynamic_object)
489 {
492 }
493 else if(src.id() == ID_allocate)
494 {
495 const auto &allocate_expr = to_allocate_expr(src);
496
497 // May need to consider failure.
498 // live_object(ς, allocate(ς, s))
499 auto live_object_expr =
503 if(verbose)
504 std::cout << "ALLOCATE1: " << format(instance1) << "\n";
505 dest << instance1;
506
507 // writeable_object(ς, allocate(ς, s))
512 if(verbose)
513 std::cout << "ALLOCATE2: " << format(instance2) << "\n";
514 dest << instance2;
515
516 // object_size(ς, allocate(ς, s)) = s
518 allocate_expr.state(), allocate_expr, allocate_expr.size().type());
520 auto instance3 =
522 if(verbose)
523 std::cout << "ALLOCATE3: " << format(instance3) << "\n";
524 dest << instance3;
525
526 // pointer_offset(allocate(ς, s)) = 0
528 // pointer_offset_exprs.insert(pointer_offset_expr);
531 if(verbose)
532 std::cout << "ALLOCATE4: " << format(instance4) << "\n";
533 dest << instance4;
534
535 // is_dynamic_object(ς, allocate(ς, s))
540 if(verbose)
541 std::cout << "ALLOCATE5: " << format(instance5) << "\n";
542 dest << instance5;
543 }
544 else if(src.id() == ID_reallocate)
545 {
546 const auto &reallocate_expr = to_reallocate_expr(src);
547
548 // May need to consider failure.
549 // live_object(ς, reallocate(ς, a, s))
550 auto live_object_expr =
554 if(verbose)
555 std::cout << "REALLOCATE1: " << format(instance1) << "\n";
556 dest << instance1;
557
558 // object_size(ς, reallocate(ς, a, s)) = s
560 reallocate_expr.state(), reallocate_expr, reallocate_expr.size().type());
562 auto instance2 =
564 if(verbose)
565 std::cout << "REALLOCATE2: " << format(instance2) << "\n";
566 dest << instance2;
567
568 // pointer_offset(reallocate(ς, a, s)) = 0
570 // pointer_offset_exprs.insert(pointer_offset_expr);
573 if(verbose)
574 std::cout << "REALLOCATE3: " << format(instance3) << "\n";
575 dest << instance3;
576
577 // is_dynamic_object(ς, reallocate(ς, s))
582 if(verbose)
583 std::cout << "REALLOCATE4: " << format(instance4) << "\n";
584 dest << instance4;
585 }
586 else if(src.id() == ID_deallocate_state)
587 {
588#if 0
589 // Disabled since any other thread may have reclaimed
590 // the memory.
592
593 // ¬live_object(deallocate(ς, p), p)
598 if(verbose)
599 std::cout << "DEALLOCATE1: " << format(instance1) << "\n";
600 dest << instance1;
601#endif
602 }
603 else if(src.id() == ID_address_of)
604 {
606 }
607 else if(src.id() == ID_object_address)
608 {
610 }
611 else if(src.id() == ID_state_object_size)
612 {
615 }
616 else if(src.id() == ID_initial_state)
617 {
619 }
620 else if(
621 src.id() == ID_state_r_ok || src.id() == ID_state_w_ok ||
622 src.id() == ID_state_rw_ok)
623 {
624 add(to_state_ok_expr(src));
625 }
626}
627
629{
630 if(!ok_exprs.insert(ok_expr).second)
631 return; // already there
632
633 const auto &state = ok_expr.state();
634 const auto &pointer = ok_expr.address();
635 const auto &size = ok_expr.size();
636
637 {
638 // X_ok(p, s) <-->
639 // live_object(p)
640 // ∧ offset(p)+s≤object_size(p)
641 // ∧ writeable_object(p) if applicable
642 auto live_object = state_live_object_exprt(state, pointer);
646
647 auto writeable_object = state_writeable_object_exprt(state, pointer);
649
652
654 auto offset = pointer_offset_exprt(pointer, ssize_type);
655 auto offset_simplified =
657 // auto lower = binary_relation_exprt(
658 // offset_simplified, ID_ge, from_integer(0, ssize_type));
659
660 auto size_type = ::size_type();
661
662 // extend one bit, to cover overflow case
663 auto size_type_ext = unsignedbv_typet(size_type.get_width() + 1);
664
665 auto object_size = state_object_size_exprt(state, pointer, size_type);
667
669
675 auto upper = binary_relation_exprt(
677
679
680 if(ok_expr.id() == ID_state_w_ok || ok_expr.id() == ID_state_rw_ok)
682
684
685 if(verbose)
686 std::cout << "AXIOMd: " << format(instance) << "\n";
687 dest << instance;
688 }
689
690 {
691 // X_ok(ς, p) --> p!=0
692 auto instance =
694 if(verbose)
695 std::cout << "AXIOMe: " << format(instance) << "\n";
696 dest << instance;
697 }
698}
699
701{
702 if(!is_cstring_exprs.insert(is_cstring_expr).second)
703 return; // already there
704
705 {
706 // is_cstring(ς, p) ⇒ r_ok(ς, p, 1)
707 auto ok_expr = ternary_exprt(
709 is_cstring_expr.state(),
710 is_cstring_expr.address(),
712 bool_typet());
713
715 if(verbose)
716 std::cout << "AXIOMa1: " << format(instance1) << "\n";
717 dest << instance1;
718
720 ok_simplified.visit_pre([this](const exprt &src) { node(src); });
722 if(verbose)
723 std::cout << "AXIOMa2: " << format(instance2) << "\n";
724 dest << instance2;
725 }
726
727 if(!recursive)
728 {
729 // is_cstring(ς, p) --> is_cstring(ς, p + 1) ∨ ς(p)=0
730 auto state = is_cstring_expr.state();
731 auto p = is_cstring_expr.address();
732 auto one = from_integer(1, signed_size_type());
733 auto p_plus_one = plus_exprt(p, one, is_cstring_expr.op1().type());
735 auto char_type = to_pointer_type(p.type()).base_type();
736 auto zero = from_integer(0, char_type);
737 auto star_p = evaluate_exprt(state, p, char_type);
738 auto is_zero = equal_exprt(star_p, zero);
739 auto instance = replace(
741 if(verbose)
742 std::cout << "AXIOMb: " << format(instance) << "\n";
743 dest << instance;
744 evaluate_exprs.insert(star_p);
745 add(is_cstring_plus_one, true); // rec. call
746 }
747}
748
750{
751 for(auto &constraint : constraints)
752 {
753 constraint.visit_pre([this](const exprt &src) { node(src); });
754
755 auto constraint_replaced = replace(constraint);
756#if 0
757 if(verbose)
758 {
759 std::cout << "CONSTRAINT1: " << format(constraint) << "\n";
760 std::cout << "CONSTRAINT2: " << format(constraint_replaced) << "\n";
761 }
762#endif
764 }
765
766 object_size();
767 live_object();
770
771 // functional consistency is done last
772 evaluate_fc();
774 ok_fc();
779}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Axioms.
signedbv_typet signed_size_type()
Definition c_types.cpp:66
bitvector_typet char_type()
Definition c_types.cpp:106
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Boolean AND.
Definition std_expr.h:2125
void is_dynamic_object_fc()
Definition axioms.cpp:219
std::set< address_of_exprt > address_of_exprs
Definition axioms.h:61
std::set< state_ok_exprt > ok_exprs
Definition axioms.h:65
std::unordered_map< exprt, symbol_exprt, irep_hash > replacement_map
Definition axioms.h:56
std::set< object_address_exprt > object_address_exprs
Definition axioms.h:63
std::set< state_live_object_exprt > live_object_exprs
Definition axioms.h:79
std::set< evaluate_exprt > evaluate_exprs
Definition axioms.h:69
void object_size()
Definition axioms.cpp:241
bool verbose
Definition axioms.h:49
void object_size_fc()
Definition axioms.cpp:278
std::set< state_is_dynamic_object_exprt > is_dynamic_object_exprs
Definition axioms.h:76
std::set< state_is_sentinel_dll_exprt > is_sentinel_dll_exprs
Definition axioms.h:91
std::set< initial_state_exprt > initial_state_exprs
Definition axioms.h:94
std::set< state_writeable_object_exprt > writeable_object_exprs
Definition axioms.h:83
void live_object_fc()
Definition axioms.cpp:126
void emit()
Definition axioms.cpp:749
const namespacet & ns
Definition axioms.h:50
void live_object()
Definition axioms.cpp:108
void ok_fc()
Definition axioms.cpp:298
std::map< irep_idt, std::size_t > counters
Definition axioms.h:57
exprt translate(exprt) const
Definition axioms.cpp:350
void set_to_true(exprt)
Definition axioms.cpp:29
void is_cstring_fc()
Definition axioms.cpp:85
void evaluate_fc()
Definition axioms.cpp:58
void set_to_false(exprt)
Definition axioms.cpp:34
void initial_state()
Definition axioms.cpp:324
std::set< state_is_cstring_exprt > is_cstring_exprs
Definition axioms.h:72
void writeable_object()
Definition axioms.cpp:146
const std::unordered_set< symbol_exprt, irep_hash > & address_taken
Definition axioms.h:48
decision_proceduret & dest
Definition axioms.h:47
std::set< state_object_size_exprt > object_size_exprs
Definition axioms.h:87
std::vector< exprt > constraints
Definition axioms.h:52
exprt replace(exprt)
Definition axioms.cpp:359
void add(const state_ok_exprt &)
Definition axioms.cpp:628
void writeable_object_fc()
Definition axioms.cpp:197
void node(const exprt &)
Definition axioms.cpp:399
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
The Boolean type.
Definition std_types.h:36
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
Boolean implication.
Definition std_expr.h:2230
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
Boolean negation.
Definition std_expr.h:2459
Operator to return the address of an object.
Boolean OR.
Definition std_expr.h:2275
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The offset (in bytes) of a pointer relative to the object.
Expression to hold a symbol (variable)
Definition std_expr.h:131
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
bool is_lvalue
Definition symbol.h:72
An expression with three operands.
Definition std_expr.h:67
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
Decision Procedure Interface.
static format_containert< T > format(const T &o)
Definition format.h:37
static exprt implication(exprt lhs, exprt rhs)
static int8_t r
Definition irep_hash.h:60
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(const exprt &pointer)
Various predicates over pointers in programs.
exprt simplify_state_expr_node(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
exprt simplify_state_expr(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
std::optional< exprt > sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &ns)
std::optional< exprt > sentinel_dll_next(const exprt &state, const exprt &node, const namespacet &ns)
const state_is_sentinel_dll_exprt & to_state_is_sentinel_dll_expr(const exprt &expr)
Cast an exprt to a state_is_sentinel_dll_exprt.
Simplify State Expression.
const state_ok_exprt & to_state_ok_expr(const exprt &expr)
Cast an exprt to a state_ok_exprt.
Definition state.h:882
const state_is_cstring_exprt & to_state_is_cstring_expr(const exprt &expr)
Cast an exprt to a state_is_cstring_exprt.
Definition state.h:615
const reallocate_exprt & to_reallocate_expr(const exprt &expr)
Cast an exprt to a reallocate_exprt.
Definition state.h:353
const state_writeable_object_exprt & to_state_writeable_object_expr(const exprt &expr)
Cast an exprt to a state_writeable_object_exprt.
Definition state.h:553
const state_is_dynamic_object_exprt & to_state_is_dynamic_object_expr(const exprt &expr)
Cast an exprt to a state_is_dynamic_object_exprt.
Definition state.h:739
const state_object_size_exprt & to_state_object_size_expr(const exprt &expr)
Cast an exprt to a state_object_size_exprt.
Definition state.h:804
const deallocate_state_exprt & to_deallocate_state_expr(const exprt &expr)
Cast an exprt to a deallocate_state_exprt.
Definition state.h:446
const initial_state_exprt & to_initial_state_expr(const exprt &expr)
Cast an exprt to a initial_state_exprt.
Definition state.h:59
const allocate_exprt & to_allocate_expr(const exprt &expr)
Cast an exprt to a allocate_exprt.
Definition state.h:260
const evaluate_exprt & to_evaluate_expr(const exprt &expr)
Cast an exprt to a evaluate_exprt.
Definition state.h:130
const state_live_object_exprt & to_state_live_object_expr(const exprt &expr)
Cast an exprt to a state_live_object_exprt.
Definition state.h:499
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:83
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const string_constantt & to_string_constant(const exprt &expr)
Symbol table entry.
#define size_type
Definition unistd.c:186