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