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 const auto cit = cache.find({identifier.get_no(), &assign.read()});
79 if(cit != cache.end())
80 return cit->second;
81
82 std::string result;
83
84 if(assign.rhs().id() == ID_array_list)
85 {
86 const array_list_exprt &array_list = to_array_list_expr(assign.rhs());
87 const auto &ops = array_list.operands();
88
89 for(std::size_t listidx = 0; listidx != ops.size(); listidx += 2)
90 {
91 const index_exprt index{assign.lhs(), ops[listidx]};
92 if(!result.empty())
93 result += ' ';
94 result +=
95 convert_assign_rec(identifier, code_assignt{index, ops[listidx + 1]});
96 }
97 }
98 else if(assign.rhs().id() == ID_array)
99 {
100 const array_typet &type = to_array_type(assign.rhs().type());
101
102 unsigned i=0;
103 for(const auto &op : assign.rhs().operands())
104 {
105 index_exprt index(
106 assign.lhs(), from_integer(i++, c_index_type()), type.element_type());
107 if(!result.empty())
108 result+=' ';
109 result += convert_assign_rec(identifier, code_assignt(index, op));
110 }
111 }
112 else if(assign.rhs().id()==ID_struct ||
113 assign.rhs().id()==ID_union)
114 {
115 // dereferencing may have resulted in an lhs that is the first
116 // struct member; undo this
117 if(
118 assign.lhs().id() == ID_member &&
119 assign.lhs().type() != assign.rhs().type())
120 {
121 code_assignt tmp=assign;
122 tmp.lhs()=to_member_expr(assign.lhs()).struct_op();
123
124 return convert_assign_rec(identifier, tmp);
125 }
126 else if(assign.lhs().id()==ID_byte_extract_little_endian ||
127 assign.lhs().id()==ID_byte_extract_big_endian)
128 {
129 code_assignt tmp=assign;
130 tmp.lhs()=to_byte_extract_expr(assign.lhs()).op();
131
132 return convert_assign_rec(identifier, tmp);
133 }
134
135 const typet &lhs_type = assign.lhs().type();
136 const struct_union_typet::componentst &components =
137 (lhs_type.id() == ID_struct_tag || lhs_type.id() == ID_union_tag)
138 ? ns.follow_tag(to_struct_or_union_tag_type(lhs_type)).components()
139 : to_struct_union_type(lhs_type).components();
140
141 exprt::operandst::const_iterator it=
142 assign.rhs().operands().begin();
143 for(const auto &comp : components)
144 {
146 comp.type().id() != ID_code, "struct member must not be of code type");
147 if(
148 comp.get_is_padding() ||
149 // for some reason #is_padding gets lost in *some* cases
150 comp.get_name().starts_with("$pad"))
151 continue;
152
153 INVARIANT(
154 it != assign.rhs().operands().end(), "expression must have operands");
155
156 member_exprt member(
157 assign.lhs(),
158 comp.get_name(),
159 it->type());
160 if(!result.empty())
161 result+=' ';
162 result+=convert_assign_rec(identifier, code_assignt(member, *it));
163 ++it;
164
165 // for unions just assign to the first member
166 if(assign.rhs().id()==ID_union)
167 break;
168 }
169 }
170 else if(assign.rhs().id() == ID_with)
171 {
172 const with_exprt &with_expr = to_with_expr(assign.rhs());
173 const auto &ops = with_expr.operands();
174
175 for(std::size_t i = 1; i < ops.size(); i += 2)
176 {
177 if(!result.empty())
178 result += ' ';
179
180 if(ops[i].id() == ID_member_name)
181 {
182 const member_exprt member{
183 assign.lhs(), ops[i].get(ID_component_name), ops[i + 1].type()};
184 result +=
185 convert_assign_rec(identifier, code_assignt(member, ops[i + 1]));
186 }
187 else
188 {
189 const index_exprt index{assign.lhs(), ops[i]};
190 result +=
191 convert_assign_rec(identifier, code_assignt(index, ops[i + 1]));
192 }
193 }
194 }
195 else
196 {
197 exprt clean_rhs=assign.rhs();
198 remove_l0_l1(clean_rhs);
199
200 exprt clean_lhs = assign.lhs();
201 remove_l0_l1(clean_lhs);
202 std::string lhs = expr_to_string(ns, identifier, clean_lhs);
203
204 if(
205 lhs.find("#return_value") != std::string::npos ||
206 (lhs.find('$') != std::string::npos &&
207 has_prefix(lhs, "return_value___VERIFIER_nondet_")))
208 {
209 lhs="\\result";
210 }
211
212 result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";";
213 }
214
215 cache.insert({{identifier.get_no(), &assign.read()}, result});
216 return result;
217}
218
219static bool filter_out(
220 const goto_tracet &goto_trace,
221 const goto_tracet::stepst::const_iterator &prev_it,
222 goto_tracet::stepst::const_iterator &it)
223{
224 if(
225 it->hidden &&
226 (!it->pc->is_assign() || it->pc->assign_rhs().id() != ID_side_effect ||
227 it->pc->assign_rhs().get(ID_statement) != ID_nondet))
228 return true;
229
230 if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
231 return true;
232
233 // we filter out steps with the same source location
234 // TODO: if these are assignments we should accumulate them into
235 // a single edge
236 if(
237 prev_it != goto_trace.steps.end() &&
238 prev_it->pc->source_location() == it->pc->source_location())
239 return true;
240
241 if(it->is_goto() && it->pc->condition().is_true())
242 return true;
243
244 const source_locationt &source_location = it->pc->source_location();
245
246 if(source_location.is_nil() ||
247 source_location.get_file().empty() ||
248 source_location.is_built_in() ||
249 source_location.get_line().empty())
250 {
251 const irep_idt id = source_location.get_function();
252 // Do not filter out assertions in functions the name of which starts with
253 // CPROVER_PREFIX, because we need to maintain those as violation nodes:
254 // these are assertions generated, for examples, for memory leaks.
255 if(!id.starts_with(CPROVER_PREFIX) || !it->is_assert())
256 return true;
257 }
258
259 return false;
260}
261
262static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
263{
264 if(
265 expr.id() == ID_symbol &&
266 to_symbol_expr(expr).get_identifier().starts_with(prefix))
267 {
268 return true;
269 }
270
271 for(const auto &op : expr.operands())
272 {
273 if(contains_symbol_prefix(op, prefix))
274 return true;
275 }
276 return false;
277}
278
281{
282 unsigned int max_thread_idx = 0;
283 bool trace_has_violation = false;
284 for(goto_tracet::stepst::const_iterator it = goto_trace.steps.begin();
285 it != goto_trace.steps.end();
286 ++it)
287 {
288 if(it->thread_nr > max_thread_idx)
289 max_thread_idx = it->thread_nr;
290 if(it->is_assert() && !it->cond_value)
291 trace_has_violation = true;
292 }
293
294 graphml.key_values["sourcecodelang"]="C";
295
296 const graphmlt::node_indext sink=graphml.add_node();
297 graphml[sink].node_name="sink";
298 graphml[sink].is_violation=false;
299 graphml[sink].has_invariant=false;
300
301 if(max_thread_idx > 0 && trace_has_violation)
302 {
303 std::vector<graphmlt::node_indext> nodes;
304
305 for(unsigned int i = 0; i <= max_thread_idx + 1; ++i)
306 {
307 nodes.push_back(graphml.add_node());
308 graphml[nodes.back()].node_name = "N" + std::to_string(i);
309 graphml[nodes.back()].is_violation = i == max_thread_idx + 1;
310 graphml[nodes.back()].has_invariant = false;
311 }
312
313 for(auto it = nodes.cbegin(); std::next(it) != nodes.cend(); ++it)
314 {
315 xmlt edge("edge");
316 edge.set_attribute("source", graphml[*it].node_name);
317 edge.set_attribute("target", graphml[*std::next(it)].node_name);
318 const auto thread_id = std::distance(nodes.cbegin(), it);
319 xmlt &data = edge.new_element("data");
320 data.set_attribute("key", "createThread");
321 data.data = std::to_string(thread_id);
322 if(thread_id == 0)
323 {
324 xmlt &data = edge.new_element("data");
325 data.set_attribute("key", "enterFunction");
326 data.data = "main";
327 }
328 graphml[*std::next(it)].in[*it].xml_node = edge;
329 graphml[*it].out[*std::next(it)].xml_node = edge;
330 }
331
332 // we do not provide any further details as CPAchecker does not seem to
333 // handle more detailed concurrency witnesses
334 return;
335 }
336
337 // step numbers start at 1
338 std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
339
340 goto_tracet::stepst::const_iterator prev_it=goto_trace.steps.end();
341 for(goto_tracet::stepst::const_iterator
342 it=goto_trace.steps.begin();
343 it!=goto_trace.steps.end();
344 it++) // we cannot replace this by a ranged for
345 {
346 if(filter_out(goto_trace, prev_it, it))
347 {
348 step_to_node[it->step_nr]=sink;
349
350 continue;
351 }
352
353 // skip declarations followed by an immediate assignment
354 goto_tracet::stepst::const_iterator next=it;
355 ++next;
356 if(
357 next != goto_trace.steps.end() &&
359 it->full_lhs == next->full_lhs &&
360 it->pc->source_location() == next->pc->source_location())
361 {
362 step_to_node[it->step_nr]=sink;
363
364 continue;
365 }
366
367 prev_it=it;
368
369 const source_locationt &source_location = it->pc->source_location();
370
371 const graphmlt::node_indext node=graphml.add_node();
372 graphml[node].node_name=
373 std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr);
374 graphml[node].file=source_location.get_file();
375 graphml[node].line=source_location.get_line();
376 graphml[node].is_violation=
377 it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
378 graphml[node].has_invariant=false;
379
380 step_to_node[it->step_nr]=node;
381 }
382
383 unsigned thread_id = 0;
384
385 // build edges
386 for(goto_tracet::stepst::const_iterator
387 it=goto_trace.steps.begin();
388 it!=goto_trace.steps.end();
389 ) // no ++it
390 {
391 const std::size_t from=step_to_node[it->step_nr];
392
393 // no outgoing edges from sinks or violation nodes
394 if(from == sink || graphml[from].is_violation)
395 {
396 ++it;
397 continue;
398 }
399
400 auto next = std::next(it);
401 for(; next != goto_trace.steps.end() &&
402 (step_to_node[next->step_nr] == sink ||
403 pointee_address_equalt{}(it->pc, next->pc)); // NOLINT
404 ++next)
405 {
406 // advance
407 }
408 const std::size_t to=
409 next==goto_trace.steps.end()?
410 sink:step_to_node[next->step_nr];
411
412 switch(it->type)
413 {
418 {
419 xmlt edge(
420 "edge",
421 {{"source", graphml[from].node_name},
422 {"target", graphml[to].node_name}},
423 {});
424
425 {
426 xmlt &data_f = edge.new_element("data");
427 data_f.set_attribute("key", "originfile");
428 data_f.data = id2string(graphml[from].file);
429
430 xmlt &data_l = edge.new_element("data");
431 data_l.set_attribute("key", "startline");
432 data_l.data = id2string(graphml[from].line);
433
434 xmlt &data_t = edge.new_element("data");
435 data_t.set_attribute("key", "threadId");
436 data_t.data = std::to_string(it->thread_nr);
437 }
438
439 const auto lhs_object = it->get_lhs_object();
440 if(
442 lhs_object.has_value())
443 {
444 const std::string &lhs_id = id2string(lhs_object->get_identifier());
445 if(lhs_id.find("pthread_create::thread") != std::string::npos)
446 {
447 xmlt &data_t = edge.new_element("data");
448 data_t.set_attribute("key", "createThread");
449 data_t.data = std::to_string(++thread_id);
450 }
451 else if(
453 it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "::dynamic_object") &&
455 it->full_lhs, SYMEX_DYNAMIC_PREFIX "::dynamic_object") &&
456 lhs_id.find("thread") == std::string::npos &&
457 lhs_id.find("mutex") == std::string::npos &&
458 (!it->full_lhs_value.is_constant() ||
459 !it->full_lhs_value.has_operands() ||
460 !has_prefix(
461 id2string(
462 to_multi_ary_expr(it->full_lhs_value).op0().get(ID_value)),
463 "INVALID-")))
464 {
465 xmlt &val = edge.new_element("data");
466 val.set_attribute("key", "assumption");
467
468 code_assignt assign{it->full_lhs, it->full_lhs_value};
469 val.data = convert_assign_rec(lhs_id, assign);
470
471 if(!it->function_id.empty())
472 {
473 xmlt &val_s = edge.new_element("data");
474 val_s.set_attribute("key", "assumption.scope");
475 irep_idt function_id = it->function_id;
476 const symbolt *symbol_ptr = nullptr;
477 if(!ns.lookup(lhs_id, symbol_ptr) && symbol_ptr->is_parameter)
478 {
479 function_id = lhs_id.substr(0, lhs_id.find("::"));
480 }
481 val_s.data = id2string(function_id);
482 }
483
484 if(has_prefix(val.data, "\\result ="))
485 {
486 xmlt &val_f = edge.new_element("data");
487 val_f.set_attribute("key", "assumption.resultfunction");
488 val_f.data = id2string(it->function_id);
489 }
490 }
491 }
492 else if(it->type == goto_trace_stept::typet::GOTO && it->pc->is_goto())
493 {
494 }
495
496 graphml[to].in[from].xml_node = edge;
497 graphml[from].out[to].xml_node = edge;
498
499 break;
500 }
501
517 // ignore
518 break;
519 }
520
521 it=next;
522 }
523}
524
527{
528 graphml.key_values["sourcecodelang"]="C";
529
530 const graphmlt::node_indext sink=graphml.add_node();
531 graphml[sink].node_name="sink";
532 graphml[sink].is_violation=false;
533 graphml[sink].has_invariant=false;
534
535 // step numbers start at 1
536 std::vector<std::size_t> step_to_node(equation.SSA_steps.size()+1, 0);
537
538 std::size_t step_nr=1;
539 for(symex_target_equationt::SSA_stepst::const_iterator
540 it=equation.SSA_steps.begin();
541 it!=equation.SSA_steps.end();
542 it++, step_nr++) // we cannot replace this by a ranged for
543 {
544 const source_locationt &source_location = it->source.pc->source_location();
545
546 if(
547 it->hidden ||
548 (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
549 (it->is_goto() && it->source.pc->condition().is_true()) ||
550 source_location.is_nil() || source_location.is_built_in() ||
551 source_location.get_line().empty())
552 {
553 step_to_node[step_nr]=sink;
554
555 continue;
556 }
557
558 // skip declarations followed by an immediate assignment
559 symex_target_equationt::SSA_stepst::const_iterator next=it;
560 ++next;
561 if(
562 next != equation.SSA_steps.end() && next->is_assignment() &&
563 it->ssa_full_lhs == next->ssa_full_lhs &&
564 it->source.pc->source_location() == next->source.pc->source_location())
565 {
566 step_to_node[step_nr]=sink;
567
568 continue;
569 }
570
571 const graphmlt::node_indext node=graphml.add_node();
572 graphml[node].node_name=
573 std::to_string(it->source.pc->location_number)+"."+
574 std::to_string(step_nr);
575 graphml[node].file=source_location.get_file();
576 graphml[node].line=source_location.get_line();
577 graphml[node].is_violation=false;
578 graphml[node].has_invariant=false;
579
580 step_to_node[step_nr]=node;
581 }
582
583 // build edges
584 step_nr=1;
585 for(symex_target_equationt::SSA_stepst::const_iterator
586 it=equation.SSA_steps.begin();
587 it!=equation.SSA_steps.end();
588 ) // no ++it
589 {
590 const std::size_t from=step_to_node[step_nr];
591
592 if(from==sink)
593 {
594 ++it;
595 ++step_nr;
596 continue;
597 }
598
599 symex_target_equationt::SSA_stepst::const_iterator next=it;
600 std::size_t next_step_nr=step_nr;
601 for(++next, ++next_step_nr;
602 next!=equation.SSA_steps.end() &&
603 (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
604 ++next, ++next_step_nr)
605 {
606 // advance
607 }
608 const std::size_t to=
609 next==equation.SSA_steps.end()?
610 sink:step_to_node[next_step_nr];
611
612 switch(it->type)
613 {
618 {
619 xmlt edge(
620 "edge",
621 {{"source", graphml[from].node_name},
622 {"target", graphml[to].node_name}},
623 {});
624
625 {
626 xmlt &data_f = edge.new_element("data");
627 data_f.set_attribute("key", "originfile");
628 data_f.data = id2string(graphml[from].file);
629
630 xmlt &data_l = edge.new_element("data");
631 data_l.set_attribute("key", "startline");
632 data_l.data = id2string(graphml[from].line);
633 }
634
635 if(
636 (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
637 it->ssa_full_lhs.is_not_nil())
638 {
639 irep_idt identifier = it->ssa_lhs.get_object_name();
640
641 graphml[to].has_invariant = true;
642 code_assignt assign(it->ssa_lhs, it->ssa_rhs);
643 graphml[to].invariant = convert_assign_rec(identifier, assign);
644 graphml[to].invariant_scope = id2string(it->source.function_id);
645 }
646
647 graphml[to].in[from].xml_node = edge;
648 graphml[from].out[to].xml_node = edge;
649
650 break;
651 }
652
668 // ignore
669 break;
670 }
671
672 it=next;
673 step_nr=next_step_nr;
674 }
675}
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:1681
Arrays with given size.
Definition std_types.h:807
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
A goto_instruction_codet representing an assignment in the program.
bool empty() const
Definition dstring.h:89
unsigned get_no() const
Definition dstring.h:182
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)
nodet::node_indext node_indext
Definition graph.h:173
Array index operator.
Definition std_expr.h:1470
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Extract member of struct or union.
Definition std_expr.h:2849
const exprt & struct_op() const
Definition std_expr.h:2887
exprt & op0()
Definition std_expr.h:932
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
const dt & read() const
Definition irep.h:240
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
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:155
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 ...
The type of an expression, extends irept.
Definition type.h:29
Operator to update elements in structs and arrays.
Definition std_expr.h:2476
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:4155
#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:44
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:1716
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2941
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2538
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
Definition std_types.h:478
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
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)
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:52
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.
dstringt irep_idt