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