cprover
Loading...
Searching...
No Matches
graphml_witness.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Witnesses for Traces and Proofs
4
5Author: Daniel Kroening
6
7\*******************************************************************/
8
11
12#include "graphml_witness.h"
13
14#include <util/arith_tools.h>
15#include <util/byte_operators.h>
16#include <util/c_types.h>
17#include <util/cprover_prefix.h>
19#include <util/prefix.h>
20#include <util/ssa_expr.h>
22#include <util/symbol_table.h>
23
25#include <langapi/mode.h>
26
28
29#include <ansi-c/expr2c.h>
30
31#include "goto_program.h"
32#include "goto_trace.h"
33
34static std::string
35expr_to_string(const namespacet &ns, const irep_idt &id, const exprt &expr)
36{
37 if(get_mode_from_identifier(ns, id) == ID_C)
39 else
40 return from_expr(ns, id, expr);
41}
42
44{
45 if(expr.id()==ID_symbol)
46 {
47 if(is_ssa_expr(expr))
48 expr=to_ssa_expr(expr).get_original_expr();
49 else
50 {
51 std::string identifier=
53
54 std::string::size_type l0_l1=identifier.find_first_of("!@");
55 if(l0_l1!=std::string::npos)
56 {
57 identifier.resize(l0_l1);
58 to_symbol_expr(expr).set_identifier(identifier);
59 }
60 }
61
62 return;
63 }
64 else if(expr.id() == ID_string_constant)
65 {
66 std::string output_string = expr_to_string(ns, "", expr);
67 if(!xmlt::is_printable_xml(output_string))
68 expr = to_string_constant(expr).to_array_expr();
69 }
70
71 Forall_operands(it, expr)
72 remove_l0_l1(*it);
73}
74
76 const irep_idt &identifier,
77 const code_assignt &assign)
78{
79#ifdef USE_DSTRING
80 const auto cit = cache.find({identifier.get_no(), &assign.read()});
81#else
82 const auto cit =
83 cache.find({get_string_container()[id2string(identifier)], &assign.read()});
84#endif
85 if(cit != cache.end())
86 return cit->second;
87
88 std::string result;
89
90 if(assign.rhs().id() == ID_array_list)
91 {
92 const array_list_exprt &array_list = to_array_list_expr(assign.rhs());
93 const auto &ops = array_list.operands();
94
95 for(std::size_t listidx = 0; listidx != ops.size(); listidx += 2)
96 {
97 const index_exprt index{assign.lhs(), ops[listidx]};
98 if(!result.empty())
99 result += ' ';
100 result +=
101 convert_assign_rec(identifier, code_assignt{index, ops[listidx + 1]});
102 }
103 }
104 else if(assign.rhs().id() == ID_array)
105 {
106 const array_typet &type = to_array_type(assign.rhs().type());
107
108 unsigned i=0;
109 forall_operands(it, assign.rhs())
110 {
111 index_exprt index(
112 assign.lhs(), from_integer(i++, c_index_type()), type.element_type());
113 if(!result.empty())
114 result+=' ';
115 result+=convert_assign_rec(identifier, code_assignt(index, *it));
116 }
117 }
118 else if(assign.rhs().id()==ID_struct ||
119 assign.rhs().id()==ID_union)
120 {
121 // dereferencing may have resulted in an lhs that is the first
122 // struct member; undo this
123 if(
124 assign.lhs().id() == ID_member &&
125 assign.lhs().type() != assign.rhs().type())
126 {
127 code_assignt tmp=assign;
128 tmp.lhs()=to_member_expr(assign.lhs()).struct_op();
129
130 return convert_assign_rec(identifier, tmp);
131 }
132 else if(assign.lhs().id()==ID_byte_extract_little_endian ||
133 assign.lhs().id()==ID_byte_extract_big_endian)
134 {
135 code_assignt tmp=assign;
136 tmp.lhs()=to_byte_extract_expr(assign.lhs()).op();
137
138 return convert_assign_rec(identifier, tmp);
139 }
140
141 const struct_union_typet &type=
143 const struct_union_typet::componentst &components=
144 type.components();
145
146 exprt::operandst::const_iterator it=
147 assign.rhs().operands().begin();
148 for(const auto &comp : components)
149 {
150 if(comp.type().id()==ID_code ||
151 comp.get_is_padding() ||
152 // for some reason #is_padding gets lost in *some* cases
153 has_prefix(id2string(comp.get_name()), "$pad"))
154 continue;
155
156 INVARIANT(
157 it != assign.rhs().operands().end(), "expression must have operands");
158
159 member_exprt member(
160 assign.lhs(),
161 comp.get_name(),
162 it->type());
163 if(!result.empty())
164 result+=' ';
165 result+=convert_assign_rec(identifier, code_assignt(member, *it));
166 ++it;
167
168 // for unions just assign to the first member
169 if(assign.rhs().id()==ID_union)
170 break;
171 }
172 }
173 else if(assign.rhs().id() == ID_with)
174 {
175 const with_exprt &with_expr = to_with_expr(assign.rhs());
176 const auto &ops = with_expr.operands();
177
178 for(std::size_t i = 1; i < ops.size(); i += 2)
179 {
180 if(!result.empty())
181 result += ' ';
182
183 if(ops[i].id() == ID_member_name)
184 {
185 const member_exprt member{
186 assign.lhs(), ops[i].get(ID_component_name), ops[i + 1].type()};
187 result +=
188 convert_assign_rec(identifier, code_assignt(member, ops[i + 1]));
189 }
190 else
191 {
192 const index_exprt index{assign.lhs(), ops[i]};
193 result +=
194 convert_assign_rec(identifier, code_assignt(index, ops[i + 1]));
195 }
196 }
197 }
198 else
199 {
200 exprt clean_rhs=assign.rhs();
201 remove_l0_l1(clean_rhs);
202
203 exprt clean_lhs = assign.lhs();
204 remove_l0_l1(clean_lhs);
205 std::string lhs = expr_to_string(ns, identifier, clean_lhs);
206
207 if(
208 lhs.find("#return_value") != std::string::npos ||
209 (lhs.find('$') != std::string::npos &&
210 has_prefix(lhs, "return_value___VERIFIER_nondet_")))
211 {
212 lhs="\\result";
213 }
214
215 result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";";
216 }
217
218#ifdef USE_DSTRING
219 cache.insert({{identifier.get_no(), &assign.read()}, result});
220#else
221 cache.insert(
222 {{get_string_container()[id2string(identifier)], &assign.read()}, result});
223#endif
224 return result;
225}
226
227static bool filter_out(
228 const goto_tracet &goto_trace,
229 const goto_tracet::stepst::const_iterator &prev_it,
230 goto_tracet::stepst::const_iterator &it)
231{
232 if(
233 it->hidden &&
234 (!it->pc->is_assign() || it->pc->assign_rhs().id() != ID_side_effect ||
235 it->pc->assign_rhs().get(ID_statement) != ID_nondet))
236 return true;
237
238 if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
239 return true;
240
241 // we filter out steps with the same source location
242 // TODO: if these are assignments we should accumulate them into
243 // a single edge
244 if(
245 prev_it != goto_trace.steps.end() &&
246 prev_it->pc->source_location() == it->pc->source_location())
247 return true;
248
249 if(it->is_goto() && it->pc->get_condition().is_true())
250 return true;
251
252 const source_locationt &source_location = it->pc->source_location();
253
254 if(source_location.is_nil() ||
255 source_location.get_file().empty() ||
256 source_location.is_built_in() ||
257 source_location.get_line().empty())
258 {
259 const irep_idt id = source_location.get_function();
260 // Do not filter out assertions in functions the name of which starts with
261 // CPROVER_PREFIX, because we need to maintain those as violation nodes:
262 // these are assertions generated, for examples, for memory leaks.
263 if(!has_prefix(id2string(id), CPROVER_PREFIX) || !it->is_assert())
264 return true;
265 }
266
267 return false;
268}
269
270static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
271{
272 if(
273 expr.id() == ID_symbol &&
275 {
276 return true;
277 }
278
279 forall_operands(it, expr)
280 {
281 if(contains_symbol_prefix(*it, prefix))
282 return true;
283 }
284 return false;
285}
286
289{
290 unsigned int max_thread_idx = 0;
291 bool trace_has_violation = false;
292 for(goto_tracet::stepst::const_iterator it = goto_trace.steps.begin();
293 it != goto_trace.steps.end();
294 ++it)
295 {
296 if(it->thread_nr > max_thread_idx)
297 max_thread_idx = it->thread_nr;
298 if(it->is_assert() && !it->cond_value)
299 trace_has_violation = true;
300 }
301
302 graphml.key_values["sourcecodelang"]="C";
303
305 graphml[sink].node_name="sink";
306 graphml[sink].is_violation=false;
307 graphml[sink].has_invariant=false;
308
309 if(max_thread_idx > 0 && trace_has_violation)
310 {
311 std::vector<graphmlt::node_indext> nodes;
312
313 for(unsigned int i = 0; i <= max_thread_idx + 1; ++i)
314 {
315 nodes.push_back(graphml.add_node());
316 graphml[nodes.back()].node_name = "N" + std::to_string(i);
317 graphml[nodes.back()].is_violation = i == max_thread_idx + 1;
318 graphml[nodes.back()].has_invariant = false;
319 }
320
321 for(auto it = nodes.cbegin(); std::next(it) != nodes.cend(); ++it)
322 {
323 xmlt edge("edge");
324 edge.set_attribute("source", graphml[*it].node_name);
325 edge.set_attribute("target", graphml[*std::next(it)].node_name);
326 const auto thread_id = std::distance(nodes.cbegin(), it);
327 xmlt &data = edge.new_element("data");
328 data.set_attribute("key", "createThread");
329 data.data = std::to_string(thread_id);
330 if(thread_id == 0)
331 {
332 xmlt &data = edge.new_element("data");
333 data.set_attribute("key", "enterFunction");
334 data.data = "main";
335 }
336 graphml[*std::next(it)].in[*it].xml_node = edge;
337 graphml[*it].out[*std::next(it)].xml_node = edge;
338 }
339
340 // we do not provide any further details as CPAchecker does not seem to
341 // handle more detailed concurrency witnesses
342 return;
343 }
344
345 // step numbers start at 1
346 std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
347
348 goto_tracet::stepst::const_iterator prev_it=goto_trace.steps.end();
349 for(goto_tracet::stepst::const_iterator
350 it=goto_trace.steps.begin();
351 it!=goto_trace.steps.end();
352 it++) // we cannot replace this by a ranged for
353 {
354 if(filter_out(goto_trace, prev_it, it))
355 {
356 step_to_node[it->step_nr]=sink;
357
358 continue;
359 }
360
361 // skip declarations followed by an immediate assignment
362 goto_tracet::stepst::const_iterator next=it;
363 ++next;
364 if(
365 next != goto_trace.steps.end() &&
367 it->full_lhs == next->full_lhs &&
368 it->pc->source_location() == next->pc->source_location())
369 {
370 step_to_node[it->step_nr]=sink;
371
372 continue;
373 }
374
375 prev_it=it;
376
377 const source_locationt &source_location = it->pc->source_location();
378
380 graphml[node].node_name=
381 std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr);
382 graphml[node].file=source_location.get_file();
383 graphml[node].line=source_location.get_line();
384 graphml[node].is_violation=
385 it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
386 graphml[node].has_invariant=false;
387
388 step_to_node[it->step_nr]=node;
389 }
390
391 unsigned thread_id = 0;
392
393 // build edges
394 for(goto_tracet::stepst::const_iterator
395 it=goto_trace.steps.begin();
396 it!=goto_trace.steps.end();
397 ) // no ++it
398 {
399 const std::size_t from=step_to_node[it->step_nr];
400
401 // no outgoing edges from sinks or violation nodes
402 if(from == sink || graphml[from].is_violation)
403 {
404 ++it;
405 continue;
406 }
407
408 auto next = std::next(it);
409 for(; next != goto_trace.steps.end() &&
410 (step_to_node[next->step_nr] == sink ||
411 pointee_address_equalt{}(it->pc, next->pc)); // NOLINT
412 ++next)
413 {
414 // advance
415 }
416 const std::size_t to=
417 next==goto_trace.steps.end()?
418 sink:step_to_node[next->step_nr];
419
420 switch(it->type)
421 {
426 {
427 xmlt edge(
428 "edge",
429 {{"source", graphml[from].node_name},
430 {"target", graphml[to].node_name}},
431 {});
432
433 {
434 xmlt &data_f = edge.new_element("data");
435 data_f.set_attribute("key", "originfile");
436 data_f.data = id2string(graphml[from].file);
437
438 xmlt &data_l = edge.new_element("data");
439 data_l.set_attribute("key", "startline");
440 data_l.data = id2string(graphml[from].line);
441
442 xmlt &data_t = edge.new_element("data");
443 data_t.set_attribute("key", "threadId");
444 data_t.data = std::to_string(it->thread_nr);
445 }
446
447 const auto lhs_object = it->get_lhs_object();
448 if(
450 lhs_object.has_value())
451 {
452 const std::string &lhs_id = id2string(lhs_object->get_identifier());
453 if(lhs_id.find("pthread_create::thread") != std::string::npos)
454 {
455 xmlt &data_t = edge.new_element("data");
456 data_t.set_attribute("key", "createThread");
457 data_t.data = std::to_string(++thread_id);
458 }
459 else if(
461 it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
463 it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
464 lhs_id.find("thread") == std::string::npos &&
465 lhs_id.find("mutex") == std::string::npos &&
466 (!it->full_lhs_value.is_constant() ||
467 !it->full_lhs_value.has_operands() ||
468 !has_prefix(
469 id2string(
470 to_multi_ary_expr(it->full_lhs_value).op0().get(ID_value)),
471 "INVALID-")))
472 {
473 xmlt &val = edge.new_element("data");
474 val.set_attribute("key", "assumption");
475
476 code_assignt assign{it->full_lhs, it->full_lhs_value};
477 val.data = convert_assign_rec(lhs_id, assign);
478
479 xmlt &val_s = edge.new_element("data");
480 val_s.set_attribute("key", "assumption.scope");
481 irep_idt function_id = it->function_id;
482 const symbolt *symbol_ptr = nullptr;
483 if(!ns.lookup(lhs_id, symbol_ptr) && symbol_ptr->is_parameter)
484 {
485 function_id = lhs_id.substr(0, lhs_id.find("::"));
486 }
487 val_s.data = id2string(function_id);
488
489 if(has_prefix(val.data, "\\result ="))
490 {
491 xmlt &val_f = edge.new_element("data");
492 val_f.set_attribute("key", "assumption.resultfunction");
493 val_f.data = id2string(it->function_id);
494 }
495 }
496 }
497 else if(it->type == goto_trace_stept::typet::GOTO && it->pc->is_goto())
498 {
499 }
500
501 graphml[to].in[from].xml_node = edge;
502 graphml[from].out[to].xml_node = edge;
503
504 break;
505 }
506
522 // ignore
523 break;
524 }
525
526 it=next;
527 }
528}
529
532{
533 graphml.key_values["sourcecodelang"]="C";
534
536 graphml[sink].node_name="sink";
537 graphml[sink].is_violation=false;
538 graphml[sink].has_invariant=false;
539
540 // step numbers start at 1
541 std::vector<std::size_t> step_to_node(equation.SSA_steps.size()+1, 0);
542
543 std::size_t step_nr=1;
544 for(symex_target_equationt::SSA_stepst::const_iterator
545 it=equation.SSA_steps.begin();
546 it!=equation.SSA_steps.end();
547 it++, step_nr++) // we cannot replace this by a ranged for
548 {
549 const source_locationt &source_location = it->source.pc->source_location();
550
551 if(
552 it->hidden ||
553 (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
554 (it->is_goto() && it->source.pc->get_condition().is_true()) ||
555 source_location.is_nil() || source_location.is_built_in() ||
556 source_location.get_line().empty())
557 {
558 step_to_node[step_nr]=sink;
559
560 continue;
561 }
562
563 // skip declarations followed by an immediate assignment
564 symex_target_equationt::SSA_stepst::const_iterator next=it;
565 ++next;
566 if(
567 next != equation.SSA_steps.end() && next->is_assignment() &&
568 it->ssa_full_lhs == next->ssa_full_lhs &&
569 it->source.pc->source_location() == next->source.pc->source_location())
570 {
571 step_to_node[step_nr]=sink;
572
573 continue;
574 }
575
577 graphml[node].node_name=
578 std::to_string(it->source.pc->location_number)+"."+
579 std::to_string(step_nr);
580 graphml[node].file=source_location.get_file();
581 graphml[node].line=source_location.get_line();
582 graphml[node].is_violation=false;
583 graphml[node].has_invariant=false;
584
585 step_to_node[step_nr]=node;
586 }
587
588 // build edges
589 step_nr=1;
590 for(symex_target_equationt::SSA_stepst::const_iterator
591 it=equation.SSA_steps.begin();
592 it!=equation.SSA_steps.end();
593 ) // no ++it
594 {
595 const std::size_t from=step_to_node[step_nr];
596
597 if(from==sink)
598 {
599 ++it;
600 ++step_nr;
601 continue;
602 }
603
604 symex_target_equationt::SSA_stepst::const_iterator next=it;
605 std::size_t next_step_nr=step_nr;
606 for(++next, ++next_step_nr;
607 next!=equation.SSA_steps.end() &&
608 (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
609 ++next, ++next_step_nr)
610 {
611 // advance
612 }
613 const std::size_t to=
614 next==equation.SSA_steps.end()?
615 sink:step_to_node[next_step_nr];
616
617 switch(it->type)
618 {
623 {
624 xmlt edge(
625 "edge",
626 {{"source", graphml[from].node_name},
627 {"target", graphml[to].node_name}},
628 {});
629
630 {
631 xmlt &data_f = edge.new_element("data");
632 data_f.set_attribute("key", "originfile");
633 data_f.data = id2string(graphml[from].file);
634
635 xmlt &data_l = edge.new_element("data");
636 data_l.set_attribute("key", "startline");
637 data_l.data = id2string(graphml[from].line);
638 }
639
640 if(
641 (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
642 it->ssa_full_lhs.is_not_nil())
643 {
644 irep_idt identifier = it->ssa_lhs.get_object_name();
645
646 graphml[to].has_invariant = true;
647 code_assignt assign(it->ssa_lhs, it->ssa_rhs);
648 graphml[to].invariant = convert_assign_rec(identifier, assign);
649 graphml[to].invariant_scope = id2string(it->source.function_id);
650 }
651
652 graphml[to].in[from].xml_node = edge;
653 graphml[from].out[to].xml_node = edge;
654
655 break;
656 }
657
673 // ignore
674 break;
675 }
676
677 it=next;
678 step_nr=next_step_nr;
679 }
680}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet c_index_type()
Definition: c_types.cpp:16
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1522
Arrays with given size.
Definition: std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
A codet representing an assignment in the program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
unsigned get_no() const
Definition: dstring.h:165
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Trace of a GOTO program.
Definition: goto_trace.h:175
stepst steps
Definition: goto_trace.h:178
const namespacet & ns
void operator()(const goto_tracet &goto_trace)
counterexample witness
std::unordered_map< std::pair< unsigned int, const irept::dt * >, std::string, pair_hash< unsigned int, const irept::dt * > > cache
void remove_l0_l1(exprt &expr)
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
key_valuest key_values
Definition: graphml.h:65
nodet::node_indext node_indext
Definition: graph.h:173
const edgest & out(node_indext n) const
Definition: graph.h:227
node_indext add_node(arguments &&... values)
Definition: graph.h:180
const edgest & in(node_indext n) const
Definition: graph.h:222
Array index operator.
Definition: std_expr.h:1328
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & struct_op() const
Definition: std_expr.h:2697
exprt & op0()
Definition: std_expr.h:844
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
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().
Definition: namespace.cpp:138
const dt & read() const
Definition: irep.h:248
const irep_idt & get_function() const
const irep_idt & get_file() const
const irep_idt & get_line() const
static bool is_built_in(const std::string &s)
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
array_exprt to_array_expr() const
convert string into array constant
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:104
Symbol table entry.
Definition: symbol.h:28
bool is_parameter
Definition: symbol.h:67
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
Definition: xml.h:21
xmlt & new_element(const std::string &key)
Definition: xml.h:95
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
std::string data
Definition: xml.h:39
static bool is_printable_xml(const std::string &s)
Determine whether s does not contain any characters that cannot be escaped in XML 1....
Definition: xml.cpp:160
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4011
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
Concrete Goto Program.
Traces of GOTO Programs.
static std::string expr_to_string(const namespacet &ns, const irep_idt &id, const exprt &expr)
static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
static bool filter_out(const goto_tracet &goto_trace, const goto_tracet::stepst::const_iterator &prev_it, goto_tracet::stepst::const_iterator &it)
Witnesses for Traces and Proofs.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
const std::string thread_id
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_mode_from_identifier(const namespacet &ns, const irep_idt &identifier)
Get the mode of the given identifier's symbol.
Definition: mode.cpp:66
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition: std_expr.h:1557
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2374
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const string_constantt & to_string_constant(const exprt &expr)
string_containert & get_string_container()
Get a reference to the global string container.
Definition: kdev_t.h:24
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
Definition: expr2c.h:75
Definition: kdev_t.h:19
Functor to check whether iterators from different collections point at the same object.
Author: Diffblue Ltd.
Generate Equation using Symbolic Execution.