cprover
custom_bitvector_analysis.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-insensitive, location-sensitive bitvector analysis
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <util/expr_util.h>
15#include <util/pointer_expr.h>
16#include <util/simplify_expr.h>
18#include <util/xml_irep.h>
19
21
22#include <iostream>
23
25 const irep_idt &identifier,
26 unsigned bit_nr,
27 modet mode)
28{
29 switch(mode)
30 {
31 case modet::SET_MUST:
32 set_bit(must_bits[identifier], bit_nr);
33 break;
34
36 clear_bit(must_bits[identifier], bit_nr);
37 break;
38
39 case modet::SET_MAY:
40 set_bit(may_bits[identifier], bit_nr);
41 break;
42
44 clear_bit(may_bits[identifier], bit_nr);
45 break;
46 }
47}
48
50 const exprt &lhs,
51 unsigned bit_nr,
52 modet mode)
53{
54 irep_idt id=object2id(lhs);
55 if(!id.empty())
56 set_bit(id, bit_nr, mode);
57}
58
60{
61 if(src.id()==ID_symbol)
62 {
63 return to_symbol_expr(src).get_identifier();
64 }
65 else if(src.id()==ID_dereference)
66 {
67 const exprt &op=to_dereference_expr(src).pointer();
68
69 if(op.id()==ID_address_of)
70 {
71 return object2id(to_address_of_expr(op).object());
72 }
73 else if(op.id()==ID_typecast)
74 {
75 irep_idt op_id=object2id(to_typecast_expr(op).op());
76
77 if(op_id.empty())
78 return irep_idt();
79 else
80 return '*'+id2string(op_id);
81 }
82 else
83 {
84 irep_idt op_id=object2id(op);
85
86 if(op_id.empty())
87 return irep_idt();
88 else
89 return '*'+id2string(op_id);
90 }
91 }
92 else if(src.id()==ID_member)
93 {
94 const auto &m=to_member_expr(src);
95 const exprt &op=m.compound();
96
97 irep_idt op_id=object2id(op);
98
99 if(op_id.empty())
100 return irep_idt();
101 else
102 return id2string(op_id)+'.'+
103 id2string(m.get_component_name());
104 }
105 else if(src.id()==ID_typecast)
106 return object2id(to_typecast_expr(src).op());
107 else
108 return irep_idt();
109}
110
112 const exprt &lhs,
113 const vectorst &vectors)
114{
115 irep_idt id=object2id(lhs);
116 if(!id.empty())
117 assign_lhs(id, vectors);
118}
119
121 const irep_idt &identifier,
122 const vectorst &vectors)
123{
124 // we erase blank ones to avoid noise
125
126 if(vectors.must_bits==0)
127 must_bits.erase(identifier);
128 else
129 must_bits[identifier]=vectors.must_bits;
130
131 if(vectors.may_bits==0)
132 may_bits.erase(identifier);
133 else
134 may_bits[identifier]=vectors.may_bits;
135}
136
139{
140 vectorst vectors;
141
142 bitst::const_iterator may_it=may_bits.find(identifier);
143 if(may_it!=may_bits.end())
144 vectors.may_bits=may_it->second;
145
146 bitst::const_iterator must_it=must_bits.find(identifier);
147 if(must_it!=must_bits.end())
148 vectors.must_bits=must_it->second;
149
150 return vectors;
151}
152
155{
156 if(rhs.id()==ID_symbol ||
157 rhs.id()==ID_dereference)
158 {
159 const irep_idt identifier=object2id(rhs);
160 return get_rhs(identifier);
161 }
162 else if(rhs.id()==ID_typecast)
163 {
164 return get_rhs(to_typecast_expr(rhs).op());
165 }
166 else if(rhs.id()==ID_if)
167 {
168 // need to merge both
169 vectorst v_true=get_rhs(to_if_expr(rhs).true_case());
170 vectorst v_false=get_rhs(to_if_expr(rhs).false_case());
171 return merge(v_true, v_false);
172 }
173
174 return vectorst();
175}
176
178 const exprt &string_expr)
179{
180 if(string_expr.id()==ID_typecast)
181 return get_bit_nr(to_typecast_expr(string_expr).op());
182 else if(string_expr.id()==ID_address_of)
183 return get_bit_nr(to_address_of_expr(string_expr).object());
184 else if(string_expr.id()==ID_index)
185 return get_bit_nr(to_index_expr(string_expr).array());
186 else if(string_expr.id()==ID_string_constant)
187 return bits.number(to_string_constant(string_expr).get_value());
188 else
189 return bits.number("(unknown)");
190}
191
193 const exprt &src,
194 locationt loc)
195{
196 if(src.id()==ID_symbol)
197 {
198 std::set<exprt> result;
199 result.insert(src);
200 return result;
201 }
202 else if(src.id()==ID_dereference)
203 {
204 exprt pointer=to_dereference_expr(src).pointer();
205
206 const std::set<exprt> alias_set =
207 local_may_alias_factory(loc).get(loc, pointer);
208
209 std::set<exprt> result;
210
211 for(const auto &alias : alias_set)
212 if(alias.type().id() == ID_pointer)
213 result.insert(dereference_exprt(alias));
214
215 result.insert(src);
216
217 return result;
218 }
219 else if(src.id()==ID_typecast)
220 {
221 return aliases(to_typecast_expr(src).op(), loc);
222 }
223 else
224 return std::set<exprt>();
225}
226
228 locationt from,
229 const exprt &lhs,
230 const exprt &rhs,
232 const namespacet &ns)
233{
234 if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
235 {
236 const struct_typet &struct_type=
237 to_struct_type(ns.follow(lhs.type()));
238
239 // assign member-by-member
240 for(const auto &c : struct_type.components())
241 {
242 member_exprt lhs_member(lhs, c),
243 rhs_member(rhs, c);
244 assign_struct_rec(from, lhs_member, rhs_member, cba, ns);
245 }
246 }
247 else
248 {
249 // may alias other stuff
250 std::set<exprt> lhs_set=cba.aliases(lhs, from);
251
252 vectorst rhs_vectors=get_rhs(rhs);
253
254 for(const auto &lhs_alias : lhs_set)
255 {
256 assign_lhs(lhs_alias, rhs_vectors);
257 }
258
259 // is it a pointer?
260 if(lhs.type().id()==ID_pointer)
261 {
262 dereference_exprt lhs_deref(lhs);
263 dereference_exprt rhs_deref(rhs);
264 assign_lhs(lhs_deref, get_rhs(rhs_deref));
265 }
266 }
267}
268
270 const irep_idt &function_from,
271 trace_ptrt trace_from,
272 const irep_idt &function_to,
273 trace_ptrt trace_to,
274 ai_baset &ai,
275 const namespacet &ns)
276{
277 locationt from{trace_from->current_location()};
278 locationt to{trace_to->current_location()};
279
280 // upcast of ai
282 static_cast<custom_bitvector_analysist &>(ai);
283
284 const goto_programt::instructiont &instruction=*from;
285
286 switch(instruction.type())
287 {
288 case ASSIGN:
290 from, instruction.assign_lhs(), instruction.assign_rhs(), cba, ns);
291 break;
292
293 case DECL:
294 {
295 const auto &decl_symbol = instruction.decl_symbol();
296 assign_lhs(decl_symbol, vectorst());
297
298 // is it a pointer?
299 if(decl_symbol.type().id() == ID_pointer)
300 assign_lhs(dereference_exprt(decl_symbol), vectorst());
301 }
302 break;
303
304 case DEAD:
305 assign_lhs(instruction.dead_symbol(), vectorst());
306
307 // is it a pointer?
308 if(instruction.dead_symbol().type().id() == ID_pointer)
310 break;
311
312 case FUNCTION_CALL:
313 {
314 const exprt &function = instruction.call_function();
315
316 if(function.id()==ID_symbol)
317 {
318 const irep_idt &identifier=to_symbol_expr(function).get_identifier();
319
320 if(
321 identifier == CPROVER_PREFIX "set_must" ||
322 identifier == CPROVER_PREFIX "clear_must" ||
323 identifier == CPROVER_PREFIX "set_may" ||
324 identifier == CPROVER_PREFIX "clear_may")
325 {
326 if(instruction.call_arguments().size() == 2)
327 {
328 unsigned bit_nr = cba.get_bit_nr(instruction.call_arguments()[1]);
329
330 // initialize to make Visual Studio happy
331 modet mode = modet::SET_MUST;
332
333 if(identifier == CPROVER_PREFIX "set_must")
334 mode=modet::SET_MUST;
335 else if(identifier == CPROVER_PREFIX "clear_must")
337 else if(identifier == CPROVER_PREFIX "set_may")
338 mode=modet::SET_MAY;
339 else if(identifier == CPROVER_PREFIX "clear_may")
340 mode=modet::CLEAR_MAY;
341 else
343
344 exprt lhs = instruction.call_arguments()[0];
345
346 if(lhs.type().id()==ID_pointer)
347 {
348 if(lhs.is_constant() &&
349 to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
350 {
351 if(mode==modet::CLEAR_MAY)
352 {
353 for(auto &bit : may_bits)
354 clear_bit(bit.second, bit_nr);
355
356 // erase blank ones
358 }
359 else if(mode==modet::CLEAR_MUST)
360 {
361 for(auto &bit : must_bits)
362 clear_bit(bit.second, bit_nr);
363
364 // erase blank ones
366 }
367 }
368 else
369 {
370 dereference_exprt deref(lhs);
371
372 // may alias other stuff
373 std::set<exprt> lhs_set=cba.aliases(deref, from);
374
375 for(const auto &l : lhs_set)
376 {
377 set_bit(l, bit_nr, mode);
378 }
379 }
380 }
381 }
382 }
383 else if(identifier=="memcpy" ||
384 identifier=="memmove")
385 {
386 if(instruction.call_arguments().size() == 3)
387 {
388 // we copy all tracked bits from op1 to op0
389 // we do not consider any bits attached to the size op2
390 dereference_exprt lhs_deref(instruction.call_arguments()[0]);
391 dereference_exprt rhs_deref(instruction.call_arguments()[1]);
392
393 assign_struct_rec(from, lhs_deref, rhs_deref, cba, ns);
394 }
395 }
396 else
397 {
398 // only if there is an actual call, i.e., we have a body
399 if(function_from != function_to)
400 {
401 const code_typet &code_type=
402 to_code_type(ns.lookup(identifier).type);
403
404 code_function_callt::argumentst::const_iterator arg_it =
405 instruction.call_arguments().begin();
406 for(const auto &param : code_type.parameters())
407 {
408 const irep_idt &p_identifier=param.get_identifier();
409 if(p_identifier.empty())
410 continue;
411
412 // there may be a mismatch in the number of arguments
413 if(arg_it == instruction.call_arguments().end())
414 break;
415
416 // assignments arguments -> parameters
417 symbol_exprt p=ns.lookup(p_identifier).symbol_expr();
418 // may alias other stuff
419 std::set<exprt> lhs_set=cba.aliases(p, from);
420
421 vectorst rhs_vectors=get_rhs(*arg_it);
422
423 for(const auto &lhs : lhs_set)
424 {
425 assign_lhs(lhs, rhs_vectors);
426 }
427
428 // is it a pointer?
429 if(p.type().id()==ID_pointer)
430 {
431 dereference_exprt lhs_deref(p);
432 dereference_exprt rhs_deref(*arg_it);
433 assign_lhs(lhs_deref, get_rhs(rhs_deref));
434 }
435
436 ++arg_it;
437 }
438 }
439 }
440 }
441 }
442 break;
443
444 case OTHER:
445 {
446 const auto &code = instruction.get_other();
447 const irep_idt &statement = code.get_statement();
448
449 if(
450 statement == ID_set_may || statement == ID_set_must ||
451 statement == ID_clear_may || statement == ID_clear_must)
452 {
454 code.operands().size() == 2, "set/clear_may/must has two operands");
455
456 unsigned bit_nr = cba.get_bit_nr(code.op1());
457
458 // initialize to make Visual Studio happy
459 modet mode = modet::SET_MUST;
460
461 if(statement == ID_set_must)
462 mode=modet::SET_MUST;
463 else if(statement == ID_clear_must)
465 else if(statement == ID_set_may)
466 mode=modet::SET_MAY;
467 else if(statement == ID_clear_may)
468 mode=modet::CLEAR_MAY;
469 else
471
472 exprt lhs = code.op0();
473
474 if(lhs.type().id()==ID_pointer)
475 {
476 if(lhs.is_constant() &&
477 to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
478 {
479 if(mode==modet::CLEAR_MAY)
480 {
481 for(bitst::iterator b_it=may_bits.begin();
482 b_it!=may_bits.end();
483 b_it++)
484 clear_bit(b_it->second, bit_nr);
485
486 // erase blank ones
488 }
489 else if(mode==modet::CLEAR_MUST)
490 {
491 for(bitst::iterator b_it=must_bits.begin();
492 b_it!=must_bits.end();
493 b_it++)
494 clear_bit(b_it->second, bit_nr);
495
496 // erase blank ones
498 }
499 }
500 else
501 {
502 dereference_exprt deref(lhs);
503
504 // may alias other stuff
505 std::set<exprt> lhs_set=cba.aliases(deref, from);
506
507 for(const auto &l : lhs_set)
508 {
509 set_bit(l, bit_nr, mode);
510 }
511 }
512 }
513 }
514 }
515 break;
516
517 case GOTO:
518 if(has_get_must_or_may(instruction.get_condition()))
519 {
520 exprt guard = instruction.get_condition();
521
522 // Comparing iterators is safe as the target must be within the same list
523 // of instructions because this is a GOTO.
524 if(to!=from->get_target())
525 guard = boolean_negate(guard);
526
527 const exprt result2 = simplify_expr(eval(guard, cba), ns);
528
529 if(result2.is_false())
530 make_bottom();
531 }
532 break;
533
534 case CATCH:
535 case THROW:
536 DATA_INVARIANT(false, "Exceptions must be removed before analysis");
537 break;
538 case SET_RETURN_VALUE:
539 DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
540 break;
541 case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
542 case ATOMIC_END: // Ignoring is a valid over-approximation
543 case END_FUNCTION: // No action required
544 case LOCATION: // No action required
545 case START_THREAD: // Require a concurrent analysis at higher level
546 case END_THREAD: // Require a concurrent analysis at higher level
547 case SKIP: // No action required
548 case ASSERT: // No action required
549 case ASSUME: // Ignoring is a valid over-approximation
550 break;
551 case INCOMPLETE_GOTO:
553 DATA_INVARIANT(false, "Only complete instructions can be analyzed");
554 break;
555 }
556}
557
559 std::ostream &out,
560 const ai_baset &ai,
561 const namespacet &) const
562{
563 if(has_values.is_known())
564 {
565 out << has_values.to_string() << '\n';
566 return;
567 }
568
570 static_cast<const custom_bitvector_analysist &>(ai);
571
572 for(const auto &bit : may_bits)
573 {
574 out << bit.first << " MAY:";
575 bit_vectort b=bit.second;
576
577 for(unsigned i=0; b!=0; i++, b>>=1)
578 if(b&1)
579 {
580 assert(i<cba.bits.size());
581 out << ' '
582 << cba.bits[i];
583 }
584
585 out << '\n';
586 }
587
588 for(const auto &bit : must_bits)
589 {
590 out << bit.first << " MUST:";
591 bit_vectort b=bit.second;
592
593 for(unsigned i=0; b!=0; i++, b>>=1)
594 if(b&1)
595 {
596 assert(i<cba.bits.size());
597 out << ' '
598 << cba.bits[i];
599 }
600
601 out << '\n';
602 }
603}
604
609{
610 bool changed=has_values.is_false();
612
613 // first do MAY
614 bitst::iterator it=may_bits.begin();
615 for(const auto &bit : b.may_bits)
616 {
617 while(it!=may_bits.end() && it->first<bit.first)
618 ++it;
619 if(it==may_bits.end() || bit.first<it->first)
620 {
621 may_bits.insert(it, bit);
622 changed=true;
623 }
624 else if(it!=may_bits.end())
625 {
626 bit_vectort &a_bits=it->second;
627 bit_vectort old=a_bits;
628 a_bits|=bit.second;
629 if(old!=a_bits)
630 changed=true;
631
632 ++it;
633 }
634 }
635
636 // now do MUST
637 it=must_bits.begin();
638 for(auto &bit : b.must_bits)
639 {
640 while(it!=must_bits.end() && it->first<bit.first)
641 {
642 it=must_bits.erase(it);
643 changed=true;
644 }
645 if(it==must_bits.end() || bit.first<it->first)
646 {
647 must_bits.insert(it, bit);
648 changed=true;
649 }
650 else if(it!=must_bits.end())
651 {
652 bit_vectort &a_bits=it->second;
653 bit_vectort old=a_bits;
654 a_bits&=bit.second;
655 if(old!=a_bits)
656 changed=true;
657
658 ++it;
659 }
660 }
661
662 // erase blank ones
665
666 return changed;
667}
668
671{
672 for(bitst::iterator a_it=bits.begin();
673 a_it!=bits.end();
674 ) // no a_it++
675 {
676 if(a_it->second==0)
677 a_it=bits.erase(a_it);
678 else
679 a_it++;
680 }
681}
682
684{
685 if(src.id() == ID_get_must || src.id() == ID_get_may)
686 return true;
687
688 forall_operands(it, src)
689 if(has_get_must_or_may(*it))
690 return true;
691
692 return false;
693}
694
696 const exprt &src,
697 custom_bitvector_analysist &custom_bitvector_analysis) const
698{
699 if(src.id() == ID_get_must || src.id() == ID_get_may)
700 {
701 if(src.operands().size()==2)
702 {
703 unsigned bit_nr =
704 custom_bitvector_analysis.get_bit_nr(to_binary_expr(src).op1());
705
706 exprt pointer = to_binary_expr(src).op0();
707
708 if(pointer.type().id()!=ID_pointer)
709 return src;
710
711 if(pointer.is_constant() &&
712 to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all
713 {
714 if(src.id() == ID_get_may)
715 {
716 for(const auto &bit : may_bits)
717 if(get_bit(bit.second, bit_nr))
718 return true_exprt();
719
720 return false_exprt();
721 }
722 else if(src.id() == ID_get_must)
723 {
724 return false_exprt();
725 }
726 else
727 return src;
728 }
729 else
730 {
732 get_rhs(dereference_exprt(pointer));
733
734 bool value=false;
735
736 if(src.id() == ID_get_must)
737 value=get_bit(v.must_bits, bit_nr);
738 else if(src.id() == ID_get_may)
739 value=get_bit(v.may_bits, bit_nr);
740
741 if(value)
742 return true_exprt();
743 else
744 return false_exprt();
745 }
746 }
747 else
748 return src;
749 }
750 else
751 {
752 exprt tmp=src;
753 Forall_operands(it, tmp)
754 *it=eval(*it, custom_bitvector_analysis);
755
756 return tmp;
757 }
758}
759
761{
762}
763
765 const goto_modelt &goto_model,
766 bool use_xml,
767 std::ostream &out)
768{
769 unsigned pass=0, fail=0, unknown=0;
770
771 for(const auto &gf_entry : goto_model.goto_functions.function_map)
772 {
773 if(!gf_entry.second.body.has_assertion())
774 continue;
775
776 // TODO this is a hard-coded hack
777 if(gf_entry.first == "__actual_thread_spawn")
778 continue;
779
780 if(!use_xml)
781 out << "******** Function " << gf_entry.first << '\n';
782
783 forall_goto_program_instructions(i_it, gf_entry.second.body)
784 {
785 exprt result;
786 irep_idt description;
787
788 if(i_it->is_assert())
789 {
791 i_it->get_condition()))
792 {
793 continue;
794 }
795
796 if(operator[](i_it).has_values.is_false())
797 continue;
798
799 exprt tmp = eval(i_it->get_condition(), i_it);
800 const namespacet ns(goto_model.symbol_table);
801 result = simplify_expr(std::move(tmp), ns);
802
803 description = i_it->source_location().get_comment();
804 }
805 else
806 continue;
807
808 if(use_xml)
809 {
810 out << "<result status=\"";
811 if(result.is_true())
812 out << "SUCCESS";
813 else if(result.is_false())
814 out << "FAILURE";
815 else
816 out << "UNKNOWN";
817 out << "\">\n";
818 out << xml(i_it->source_location());
819 out << "<description>"
820 << description
821 << "</description>\n";
822 out << "</result>\n\n";
823 }
824 else
825 {
826 out << i_it->source_location();
827 if(!description.empty())
828 out << ", " << description;
829 out << ": ";
830 const namespacet ns(goto_model.symbol_table);
831 out << from_expr(ns, gf_entry.first, result);
832 out << '\n';
833 }
834
835 if(result.is_true())
836 pass++;
837 else if(result.is_false())
838 fail++;
839 else
840 unknown++;
841 }
842
843 if(!use_xml)
844 out << '\n';
845 }
846
847 if(!use_xml)
848 out << "SUMMARY: " << pass << " pass, " << fail << " fail, "
849 << unknown << " unknown\n";
850}
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
goto_programt::const_targett locationt
Definition: ai.h:126
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
goto_programt::const_targett locationt
Definition: ai_domain.h:73
exprt & op0()
Definition: expr.h:99
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
std::set< exprt > aliases(const exprt &, locationt loc)
local_may_alias_factoryt local_may_alias_factory
exprt eval(const exprt &src, locationt loc)
void check(const goto_modelt &, bool xml, std::ostream &)
void set_bit(const exprt &, unsigned bit_nr, modet)
bool merge(const custom_bitvector_domaint &b, trace_ptrt from, trace_ptrt to)
std::map< irep_idt, bit_vectort > bitst
static irep_idt object2id(const exprt &)
void assign_struct_rec(locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &)
static bool has_get_must_or_may(const exprt &)
vectorst get_rhs(const exprt &) const
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
void assign_lhs(const exprt &, const vectorst &)
void erase_blank_vectors(bitst &)
erase blank bitvectors
static bool get_bit(const bit_vectort src, unsigned bit_nr)
void make_bottom() final override
no states
exprt eval(const exprt &src, custom_bitvector_analysist &) const
Operator to dereference a pointer.
Definition: pointer_expr.h:648
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
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
exprt & op0()
Definition: expr.h:99
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2865
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:243
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:227
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:313
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:367
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:299
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:213
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:271
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:343
const irep_idt & id() const
Definition: irep.h:396
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
Extract member of struct or union.
Definition: std_expr.h:2667
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
number_type number(const key_type &a)
Definition: numbering.h:37
size_type size() const
Definition: numbering.h:66
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The Boolean constant true.
Definition: std_expr.h:2856
bool is_known() const
Definition: threeval.h:28
const char * to_string() const
Definition: threeval.cpp:13
bool is_false() const
Definition: threeval.h:26
static tvt unknown()
Definition: threeval.h:33
#define CPROVER_PREFIX
Field-insensitive, location-sensitive bitvector analysis.
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:126
Deprecated expression utility functions.
#define forall_goto_program_instructions(it, program)
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const string_constantt & to_string_constant(const exprt &expr)