CBMC
Loading...
Searching...
No Matches
format_hooks.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
9#include "format_hooks.h"
10
11#include <util/format_expr.h>
12#include <util/format_type.h>
13#include <util/pointer_expr.h>
14#include <util/std_code.h>
15
16#include "state.h"
17
18void format_hooks()
19{
20 add_format_hook(
21 ID_object_address,
22 [](std::ostream &os, const exprt &expr) -> std::ostream & {
23 const auto &object_address_expr = to_object_address_expr(expr);
24 os << u8"\u275d" << object_address_expr.object_identifier() << u8"\u275e";
25 return os;
26 });
27
28 add_format_hook(
29 ID_object_size, [](std::ostream &os, const exprt &expr) -> std::ostream & {
30 const auto &object_size_expr = to_object_size_expr(expr);
31 os << "object_size(" << format(object_size_expr.op()) << ')';
32 return os;
33 });
34
35 add_format_hook(
36 ID_pointer_offset,
37 [](std::ostream &os, const exprt &expr) -> std::ostream & {
38 const auto &pointer_offset_expr = to_pointer_offset_expr(expr);
39 os << "pointer_offset(" << format(pointer_offset_expr.op()) << ')';
40 return os;
41 });
42
43 add_format_hook(
44 ID_state_object_size,
45 [](std::ostream &os, const exprt &expr) -> std::ostream & {
46 const auto &object_size_expr = to_binary_expr(expr);
47 os << "object_size(" << format(object_size_expr.op0()) << ", "
48 << format(object_size_expr.op1()) << ')';
49 return os;
50 });
51
52 add_format_hook(
53 ID_field_address,
54 [](std::ostream &os, const exprt &expr) -> std::ostream & {
55 const auto &field_address_expr = to_field_address_expr(expr);
56 os << format(field_address_expr.base()) << u8".\u275d"
57 << field_address_expr.component_name() << u8"\u275e";
58 return os;
59 });
60
61 add_format_hook(
62 ID_evaluate, [](std::ostream &os, const exprt &expr) -> std::ostream & {
63 const auto &evaluate_expr = to_evaluate_expr(expr);
64 if(evaluate_expr.op0().id() == ID_symbol)
65 os << format(evaluate_expr.op0());
66 else
67 os << '(' << format(evaluate_expr.op0()) << ')';
68 os << '(' << format(evaluate_expr.op1()) << ')';
69 return os;
70 });
71
72 add_format_hook(
73 ID_update_state, [](std::ostream &os, const exprt &expr) -> std::ostream & {
74 const auto &update_state_expr = to_update_state_expr(expr);
75 os << format(update_state_expr.state()) << '['
76 << format(update_state_expr.address())
77 << ":=" << format(update_state_expr.new_value()) << ']';
78 return os;
79 });
80
81 add_format_hook(
82 ID_is_cstring, [](std::ostream &os, const exprt &expr) -> std::ostream & {
83 const auto &is_cstring_expr = to_unary_expr(expr);
84 return os << "is_cstring(" << format(is_cstring_expr.op()) << ')';
85 });
86
87 add_format_hook(
88 ID_state_is_cstring,
89 [](std::ostream &os, const exprt &expr) -> std::ostream & {
90 const auto &is_cstring_expr = to_state_is_cstring_expr(expr);
91 return os << "is_cstring(" << format(is_cstring_expr.state()) << ", "
92 << format(is_cstring_expr.address()) << ')';
93 });
94
95 add_format_hook(
96 ID_state_is_dynamic_object,
97 [](std::ostream &os, const exprt &expr) -> std::ostream & {
98 const auto &is_dynamic_object_expr =
99 to_state_is_dynamic_object_expr(expr);
100 return os << "is_dynamic_object("
101 << format(is_dynamic_object_expr.state()) << ", "
102 << format(is_dynamic_object_expr.address()) << ')';
103 });
104
105 add_format_hook(
106 ID_state_r_ok, [](std::ostream &os, const exprt &expr) -> std::ostream & {
107 const auto &r_ok_expr = to_ternary_expr(expr);
108 return os << "r_ok(" << format(r_ok_expr.op0()) << ", "
109 << format(r_ok_expr.op1()) << ", " << format(r_ok_expr.op2())
110 << ')';
111 });
112
113 add_format_hook(
114 ID_state_live_object,
115 [](std::ostream &os, const exprt &expr) -> std::ostream & {
116 const auto &live_object_expr = to_binary_expr(expr);
117 return os << "live_object(" << format(live_object_expr.op0()) << ", "
118 << format(live_object_expr.op1()) << ')';
119 });
120
121 add_format_hook(
122 ID_state_writeable_object,
123 [](std::ostream &os, const exprt &expr) -> std::ostream & {
124 const auto &writeable_object_expr = to_binary_expr(expr);
125 return os << "writeable_object(" << format(writeable_object_expr.op0())
126 << ", " << format(writeable_object_expr.op1()) << ')';
127 });
128
129 add_format_hook(
130 ID_state_type_compatible,
131 [](std::ostream &os, const exprt &expr) -> std::ostream & {
132 const auto &type_compatible_expr = to_state_type_compatible_expr(expr);
133 return os << "type_compatible(" << format(type_compatible_expr.state())
134 << ", " << format(type_compatible_expr.address()) << ')';
135 });
136
137 add_format_hook(
138 ID_side_effect, [](std::ostream &os, const exprt &expr) -> std::ostream & {
139 const auto &side_effect_expr = to_side_effect_expr(expr);
140 if(side_effect_expr.get_statement() == ID_nondet)
141 return os << "nondet " << format(side_effect_expr.type());
142 else
143 return os << "side-effect-" << side_effect_expr.get_statement();
144 });
145}
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
exprt
Base class for all expressions.
Definition expr.h:56
format
static format_containert< T > format(const T &o)
Definition format.h:37
add_format_hook
void add_format_hook(irep_idt id, format_expr_configt::formattert formatter)
Definition format_expr.cpp:640
format_expr.h
format_hooks
void format_hooks()
Definition format_hooks.cpp:18
format_hooks.h
format_type.h
pointer_expr.h
API to expression classes for Pointers.
to_object_address_expr
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
Definition pointer_expr.h:643
to_pointer_offset_expr
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
Definition pointer_expr.h:1320
to_field_address_expr
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
Definition pointer_expr.h:727
to_object_size_expr
const object_size_exprt & to_object_size_expr(const exprt &expr)
Cast an exprt to a object_size_exprt.
Definition pointer_expr.h:1423
to_state_type_compatible_expr
const state_type_compatible_exprt & to_state_type_compatible_expr(const exprt &expr)
Cast an exprt to a state_type_compatible_exprt.
Definition state.h:958
to_state_is_cstring_expr
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
to_state_is_dynamic_object_expr
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
to_update_state_expr
const update_state_exprt & to_update_state_expr(const exprt &expr)
Cast an exprt to a update_state_exprt.
Definition state.h:200
to_evaluate_expr
const evaluate_exprt & to_evaluate_expr(const exprt &expr)
Cast an exprt to a evaluate_exprt.
Definition state.h:130
std_code.h
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
to_ternary_expr
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
Definition std_expr.h:116
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426