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