CBMC
custom_bitvector_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive bitvector analysis
4 
5 Author: 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>
17 #include <util/string_constant.h>
18 #include <util/xml_irep.h>
19 
20 #include <langapi/language_util.h>
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 
35  case modet::CLEAR_MUST:
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 
43  case modet::CLEAR_MAY:
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).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  lhs.type().id() == ID_struct
238  ? to_struct_type(lhs.type())
239  : ns.follow_tag(to_struct_tag_type(lhs.type()));
240 
241  // assign member-by-member
242  for(const auto &c : struct_type.components())
243  {
244  member_exprt lhs_member(lhs, c),
245  rhs_member(rhs, c);
246  assign_struct_rec(from, lhs_member, rhs_member, cba, ns);
247  }
248  }
249  else
250  {
251  // may alias other stuff
252  std::set<exprt> lhs_set=cba.aliases(lhs, from);
253 
254  vectorst rhs_vectors=get_rhs(rhs);
255 
256  for(const auto &lhs_alias : lhs_set)
257  {
258  assign_lhs(lhs_alias, rhs_vectors);
259  }
260 
261  // is it a pointer?
262  if(lhs.type().id()==ID_pointer)
263  {
264  dereference_exprt lhs_deref(lhs);
265  dereference_exprt rhs_deref(rhs);
266  assign_lhs(lhs_deref, get_rhs(rhs_deref));
267  }
268  }
269 }
270 
272  const irep_idt &function_from,
273  trace_ptrt trace_from,
274  const irep_idt &function_to,
275  trace_ptrt trace_to,
276  ai_baset &ai,
277  const namespacet &ns)
278 {
279  locationt from{trace_from->current_location()};
280  locationt to{trace_to->current_location()};
281 
282  // upcast of ai
284  static_cast<custom_bitvector_analysist &>(ai);
285 
286  const goto_programt::instructiont &instruction=*from;
287 
288  switch(instruction.type())
289  {
290  case ASSIGN:
292  from, instruction.assign_lhs(), instruction.assign_rhs(), cba, ns);
293  break;
294 
295  case DECL:
296  {
297  const auto &decl_symbol = instruction.decl_symbol();
298  assign_lhs(decl_symbol, vectorst());
299 
300  // is it a pointer?
301  if(decl_symbol.type().id() == ID_pointer)
302  assign_lhs(dereference_exprt(decl_symbol), vectorst());
303  }
304  break;
305 
306  case DEAD:
307  assign_lhs(instruction.dead_symbol(), vectorst());
308 
309  // is it a pointer?
310  if(instruction.dead_symbol().type().id() == ID_pointer)
312  break;
313 
314  case FUNCTION_CALL:
315  {
316  const exprt &function = instruction.call_function();
317 
318  if(function.id()==ID_symbol)
319  {
320  const irep_idt &identifier=to_symbol_expr(function).get_identifier();
321 
322  if(
323  identifier == CPROVER_PREFIX "set_must" ||
324  identifier == CPROVER_PREFIX "clear_must" ||
325  identifier == CPROVER_PREFIX "set_may" ||
326  identifier == CPROVER_PREFIX "clear_may")
327  {
328  if(instruction.call_arguments().size() == 2)
329  {
330  unsigned bit_nr = cba.get_bit_nr(instruction.call_arguments()[1]);
331 
332  // initialize to make Visual Studio happy
333  modet mode = modet::SET_MUST;
334 
335  if(identifier == CPROVER_PREFIX "set_must")
336  mode=modet::SET_MUST;
337  else if(identifier == CPROVER_PREFIX "clear_must")
338  mode=modet::CLEAR_MUST;
339  else if(identifier == CPROVER_PREFIX "set_may")
340  mode=modet::SET_MAY;
341  else if(identifier == CPROVER_PREFIX "clear_may")
342  mode=modet::CLEAR_MAY;
343  else
344  UNREACHABLE;
345 
346  exprt lhs = instruction.call_arguments()[0];
347 
348  if(lhs.type().id()==ID_pointer)
349  {
350  if(
351  lhs.is_constant() &&
352  to_constant_expr(lhs).is_null_pointer()) // NULL means all
353  {
354  if(mode==modet::CLEAR_MAY)
355  {
356  for(auto &bit : may_bits)
357  clear_bit(bit.second, bit_nr);
358 
359  // erase blank ones
361  }
362  else if(mode==modet::CLEAR_MUST)
363  {
364  for(auto &bit : must_bits)
365  clear_bit(bit.second, bit_nr);
366 
367  // erase blank ones
369  }
370  }
371  else
372  {
373  dereference_exprt deref(lhs);
374 
375  // may alias other stuff
376  std::set<exprt> lhs_set=cba.aliases(deref, from);
377 
378  for(const auto &l : lhs_set)
379  {
380  set_bit(l, bit_nr, mode);
381  }
382  }
383  }
384  }
385  }
386  else if(identifier=="memcpy" ||
387  identifier=="memmove")
388  {
389  if(instruction.call_arguments().size() == 3)
390  {
391  // we copy all tracked bits from op1 to op0
392  // we do not consider any bits attached to the size op2
393  dereference_exprt lhs_deref(instruction.call_arguments()[0]);
394  dereference_exprt rhs_deref(instruction.call_arguments()[1]);
395 
396  assign_struct_rec(from, lhs_deref, rhs_deref, cba, ns);
397  }
398  }
399  else
400  {
401  // only if there is an actual call, i.e., we have a body
402  if(function_from != function_to)
403  {
404  const code_typet &code_type=
405  to_code_type(ns.lookup(identifier).type);
406 
407  code_function_callt::argumentst::const_iterator arg_it =
408  instruction.call_arguments().begin();
409  for(const auto &param : code_type.parameters())
410  {
411  const irep_idt &p_identifier=param.get_identifier();
412  if(p_identifier.empty())
413  continue;
414 
415  // there may be a mismatch in the number of arguments
416  if(arg_it == instruction.call_arguments().end())
417  break;
418 
419  // assignments arguments -> parameters
420  symbol_exprt p=ns.lookup(p_identifier).symbol_expr();
421  // may alias other stuff
422  std::set<exprt> lhs_set=cba.aliases(p, from);
423 
424  vectorst rhs_vectors=get_rhs(*arg_it);
425 
426  for(const auto &lhs : lhs_set)
427  {
428  assign_lhs(lhs, rhs_vectors);
429  }
430 
431  // is it a pointer?
432  if(p.type().id()==ID_pointer)
433  {
434  dereference_exprt lhs_deref(p);
435  dereference_exprt rhs_deref(*arg_it);
436  assign_lhs(lhs_deref, get_rhs(rhs_deref));
437  }
438 
439  ++arg_it;
440  }
441  }
442  }
443  }
444  }
445  break;
446 
447  case OTHER:
448  {
449  const auto &code = instruction.get_other();
450  const irep_idt &statement = code.get_statement();
451 
452  if(
453  statement == ID_set_may || statement == ID_set_must ||
454  statement == ID_clear_may || statement == ID_clear_must)
455  {
457  code.operands().size() == 2, "set/clear_may/must has two operands");
458 
459  unsigned bit_nr = cba.get_bit_nr(code.op1());
460 
461  // initialize to make Visual Studio happy
462  modet mode = modet::SET_MUST;
463 
464  if(statement == ID_set_must)
465  mode=modet::SET_MUST;
466  else if(statement == ID_clear_must)
467  mode=modet::CLEAR_MUST;
468  else if(statement == ID_set_may)
469  mode=modet::SET_MAY;
470  else if(statement == ID_clear_may)
471  mode=modet::CLEAR_MAY;
472  else
473  UNREACHABLE;
474 
475  exprt lhs = code.op0();
476 
477  if(lhs.type().id()==ID_pointer)
478  {
479  if(
480  lhs.is_constant() &&
481  to_constant_expr(lhs).is_null_pointer()) // NULL means all
482  {
483  if(mode==modet::CLEAR_MAY)
484  {
485  for(bitst::iterator b_it=may_bits.begin();
486  b_it!=may_bits.end();
487  b_it++)
488  clear_bit(b_it->second, bit_nr);
489 
490  // erase blank ones
492  }
493  else if(mode==modet::CLEAR_MUST)
494  {
495  for(bitst::iterator b_it=must_bits.begin();
496  b_it!=must_bits.end();
497  b_it++)
498  clear_bit(b_it->second, bit_nr);
499 
500  // erase blank ones
502  }
503  }
504  else
505  {
506  dereference_exprt deref(lhs);
507 
508  // may alias other stuff
509  std::set<exprt> lhs_set=cba.aliases(deref, from);
510 
511  for(const auto &l : lhs_set)
512  {
513  set_bit(l, bit_nr, mode);
514  }
515  }
516  }
517  }
518  }
519  break;
520 
521  case GOTO:
522  if(has_get_must_or_may(instruction.condition()))
523  {
524  exprt guard = instruction.condition();
525 
526  // Comparing iterators is safe as the target must be within the same list
527  // of instructions because this is a GOTO.
528  if(to!=from->get_target())
530 
531  const exprt result2 = simplify_expr(eval(guard, cba), ns);
532 
533  if(result2.is_false())
534  make_bottom();
535  }
536  break;
537 
538  case CATCH:
539  case THROW:
540  DATA_INVARIANT(false, "Exceptions must be removed before analysis");
541  break;
542  case SET_RETURN_VALUE:
543  DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
544  break;
545  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
546  case ATOMIC_END: // Ignoring is a valid over-approximation
547  case END_FUNCTION: // No action required
548  case LOCATION: // No action required
549  case START_THREAD: // Require a concurrent analysis at higher level
550  case END_THREAD: // Require a concurrent analysis at higher level
551  case SKIP: // No action required
552  case ASSERT: // No action required
553  case ASSUME: // Ignoring is a valid over-approximation
554  break;
555  case INCOMPLETE_GOTO:
556  case NO_INSTRUCTION_TYPE:
557  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
558  break;
559  }
560 }
561 
563  std::ostream &out,
564  const ai_baset &ai,
565  const namespacet &) const
566 {
567  if(has_values.is_known())
568  {
569  out << has_values.to_string() << '\n';
570  return;
571  }
572 
573  const custom_bitvector_analysist &cba=
574  static_cast<const custom_bitvector_analysist &>(ai);
575 
576  for(const auto &bit : may_bits)
577  {
578  out << bit.first << " MAY:";
579  bit_vectort b=bit.second;
580 
581  for(unsigned i=0; b!=0; i++, b>>=1)
582  if(b&1)
583  {
584  INVARIANT(i < cba.bits.size(), "inconsistent bit widths");
585  out << ' '
586  << cba.bits[i];
587  }
588 
589  out << '\n';
590  }
591 
592  for(const auto &bit : must_bits)
593  {
594  out << bit.first << " MUST:";
595  bit_vectort b=bit.second;
596 
597  for(unsigned i=0; b!=0; i++, b>>=1)
598  if(b&1)
599  {
600  INVARIANT(i < cba.bits.size(), "inconsistent bit widths");
601  out << ' '
602  << cba.bits[i];
603  }
604 
605  out << '\n';
606  }
607 }
608 
610  const custom_bitvector_domaint &b,
611  trace_ptrt,
612  trace_ptrt)
613 {
614  bool changed=has_values.is_false();
616 
617  // first do MAY
618  bitst::iterator it=may_bits.begin();
619  for(const auto &bit : b.may_bits)
620  {
621  while(it!=may_bits.end() && it->first<bit.first)
622  ++it;
623  if(it==may_bits.end() || bit.first<it->first)
624  {
625  may_bits.insert(it, bit);
626  changed=true;
627  }
628  else if(it!=may_bits.end())
629  {
630  bit_vectort &a_bits=it->second;
631  bit_vectort old=a_bits;
632  a_bits|=bit.second;
633  if(old!=a_bits)
634  changed=true;
635 
636  ++it;
637  }
638  }
639 
640  // now do MUST
641  it=must_bits.begin();
642  for(auto &bit : b.must_bits)
643  {
644  while(it!=must_bits.end() && it->first<bit.first)
645  {
646  it=must_bits.erase(it);
647  changed=true;
648  }
649  if(it==must_bits.end() || bit.first<it->first)
650  {
651  must_bits.insert(it, bit);
652  changed=true;
653  }
654  else if(it!=must_bits.end())
655  {
656  bit_vectort &a_bits=it->second;
657  bit_vectort old=a_bits;
658  a_bits&=bit.second;
659  if(old!=a_bits)
660  changed=true;
661 
662  ++it;
663  }
664  }
665 
666  // erase blank ones
669 
670  return changed;
671 }
672 
675 {
676  for(bitst::iterator a_it=bits.begin();
677  a_it!=bits.end();
678  ) // no a_it++
679  {
680  if(a_it->second==0)
681  a_it=bits.erase(a_it);
682  else
683  a_it++;
684  }
685 }
686 
688 {
689  if(src.id() == ID_get_must || src.id() == ID_get_may)
690  return true;
691 
692  for(const auto &op : src.operands())
693  {
694  if(has_get_must_or_may(op))
695  return true;
696  }
697 
698  return false;
699 }
700 
702  const exprt &src,
703  custom_bitvector_analysist &custom_bitvector_analysis) const
704 {
705  if(src.id() == ID_get_must || src.id() == ID_get_may)
706  {
707  if(src.operands().size()==2)
708  {
709  unsigned bit_nr =
710  custom_bitvector_analysis.get_bit_nr(to_binary_expr(src).op1());
711 
712  exprt pointer = to_binary_expr(src).op0();
713 
714  if(pointer.type().id()!=ID_pointer)
715  return src;
716 
717  if(
718  pointer.is_constant() &&
719  to_constant_expr(pointer).is_null_pointer()) // NULL means all
720  {
721  if(src.id() == ID_get_may)
722  {
723  for(const auto &bit : may_bits)
724  if(get_bit(bit.second, bit_nr))
725  return true_exprt();
726 
727  return false_exprt();
728  }
729  else if(src.id() == ID_get_must)
730  {
731  return false_exprt();
732  }
733  else
734  return src;
735  }
736  else
737  {
739  get_rhs(dereference_exprt(pointer));
740 
741  bool value=false;
742 
743  if(src.id() == ID_get_must)
744  value=get_bit(v.must_bits, bit_nr);
745  else if(src.id() == ID_get_may)
746  value=get_bit(v.may_bits, bit_nr);
747 
748  if(value)
749  return true_exprt();
750  else
751  return false_exprt();
752  }
753  }
754  else
755  return src;
756  }
757  else
758  {
759  exprt tmp=src;
760  Forall_operands(it, tmp)
761  *it=eval(*it, custom_bitvector_analysis);
762 
763  return tmp;
764  }
765 }
766 
768 {
769 }
770 
772  const goto_modelt &goto_model,
773  bool use_xml,
774  std::ostream &out)
775 {
776  unsigned pass=0, fail=0, unknown=0;
777 
778  for(const auto &gf_entry : goto_model.goto_functions.function_map)
779  {
780  if(!gf_entry.second.body.has_assertion())
781  continue;
782 
783  // TODO this is a hard-coded hack
784  if(gf_entry.first == "__actual_thread_spawn")
785  continue;
786 
787  if(!use_xml)
788  out << "******** Function " << gf_entry.first << '\n';
789 
790  forall_goto_program_instructions(i_it, gf_entry.second.body)
791  {
792  exprt result;
793  irep_idt description;
794 
795  if(i_it->is_assert())
796  {
797  if(!custom_bitvector_domaint::has_get_must_or_may(i_it->condition()))
798  {
799  continue;
800  }
801 
802  if(operator[](i_it).has_values.is_false())
803  continue;
804 
805  exprt tmp = eval(i_it->condition(), i_it);
806  const namespacet ns(goto_model.symbol_table);
807  result = simplify_expr(std::move(tmp), ns);
808 
809  description = i_it->source_location().get_comment();
810  }
811  else
812  continue;
813 
814  if(use_xml)
815  {
816  out << "<result status=\"";
817  if(result.is_true())
818  out << "SUCCESS";
819  else if(result.is_false())
820  out << "FAILURE";
821  else
822  out << "UNKNOWN";
823  out << "\">\n";
824  out << xml(i_it->source_location());
825  out << "<description>"
826  << description
827  << "</description>\n";
828  out << "</result>\n\n";
829  }
830  else
831  {
832  out << i_it->source_location();
833  if(!description.empty())
834  out << ", " << description;
835  out << ": ";
836  const namespacet ns(goto_model.symbol_table);
837  out << from_expr(ns, gf_entry.first, result);
838  out << '\n';
839  }
840 
841  if(result.is_true())
842  pass++;
843  else if(result.is_false())
844  fail++;
845  else
846  unknown++;
847  }
848 
849  if(!use_xml)
850  out << '\n';
851  }
852 
853  if(!use_xml)
854  out << "SUMMARY: " << pass << " pass, " << fail << " fail, "
855  << unknown << " unknown\n";
856 }
static exprt guard(const exprt::operandst &guards, exprt cond)
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:117
goto_programt::const_targett locationt
Definition: ai.h:124
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:73
goto_programt::const_targett locationt
Definition: ai_domain.h:72
exprt & op0()
Definition: expr.h:133
Base type of functions.
Definition: std_types.h:583
const parameterst & parameters() const
Definition: std_types.h:699
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:834
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Base class for all expressions.
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
exprt & op0()
Definition: expr.h:133
operandst & operands()
Definition: expr.h:94
The Boolean constant false.
Definition: std_expr.h:3072
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
const exprt & condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:366
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:272
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:314
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:214
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:244
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:228
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:200
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:344
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:300
const irep_idt & id() const
Definition: irep.h:388
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
Extract member of struct or union.
Definition: std_expr.h:2844
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
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:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
The Boolean constant true.
Definition: std_expr.h:3063
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:27
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:103
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition: expr_util.cpp:344
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
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:110
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3045
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2102
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:715
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2936
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
const string_constantt & to_string_constant(const exprt &expr)
dstringt irep_idt