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  // initialize to make Visual Studio happy
334  modet mode = modet::SET_MUST;
335 
336  if(identifier=="__CPROVER_set_must")
337  mode=modet::SET_MUST;
338  else if(identifier=="__CPROVER_clear_must")
339  mode=modet::CLEAR_MUST;
340  else if(identifier=="__CPROVER_set_may")
341  mode=modet::SET_MAY;
342  else if(identifier=="__CPROVER_clear_may")
343  mode=modet::CLEAR_MAY;
344  else
345  UNREACHABLE;
346 
347  exprt lhs=code_function_call.arguments()[0];
348 
349  if(lhs.type().id()==ID_pointer)
350  {
351  if(lhs.is_constant() &&
352  to_constant_expr(lhs).get_value()==ID_NULL) // 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 &lhs : lhs_set)
379  {
380  set_bit(lhs, bit_nr, mode);
381  }
382  }
383  }
384  }
385  }
386  else if(identifier=="memcpy" ||
387  identifier=="memmove")
388  {
389  if(code_function_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(code_function_call.arguments()[0]);
394  dereference_exprt rhs_deref(code_function_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(from->function != to->function)
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  code_function_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==code_function_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  vectorst rhs_vectors=get_rhs(rhs_deref);
437  assign_lhs(lhs_deref, rhs_vectors);
438  }
439 
440  ++arg_it;
441  }
442  }
443  }
444  }
445  }
446  break;
447 
448  case OTHER:
449  {
450  const irep_idt &statement=instruction.code.get_statement();
451 
452  if(statement=="set_may" ||
453  statement=="set_must" ||
454  statement=="clear_may" ||
455  statement=="clear_must")
456  {
457  assert(instruction.code.operands().size()==2);
458 
459  unsigned bit_nr=
460  cba.get_bit_nr(instruction.code.op1());
461 
462  // initialize to make Visual Studio happy
463  modet mode = modet::SET_MUST;
464 
465  if(statement=="set_must")
466  mode=modet::SET_MUST;
467  else if(statement=="clear_must")
468  mode=modet::CLEAR_MUST;
469  else if(statement=="set_may")
470  mode=modet::SET_MAY;
471  else if(statement=="clear_may")
472  mode=modet::CLEAR_MAY;
473  else
474  UNREACHABLE;
475 
476  exprt lhs=instruction.code.op0();
477 
478  if(lhs.type().id()==ID_pointer)
479  {
480  if(lhs.is_constant() &&
481  to_constant_expr(lhs).get_value()==ID_NULL) // 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 &lhs : lhs_set)
512  {
513  set_bit(lhs, bit_nr, mode);
514  }
515  }
516  }
517  }
518  }
519  break;
520 
521  case GOTO:
522  if(has_get_must_or_may(instruction.guard))
523  {
524  exprt guard=instruction.guard;
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())
529  guard.make_not();
530 
531  exprt result=eval(guard, cba);
532  exprt result2=simplify_expr(result, ns);
533 
534  if(result2.is_false())
535  make_bottom();
536  }
537  break;
538 
539  default:
540  {
541  }
542  }
543 }
544 
546  std::ostream &out,
547  const ai_baset &ai,
548  const namespacet &) const
549 {
550  if(has_values.is_known())
551  {
552  out << has_values.to_string() << '\n';
553  return;
554  }
555 
556  const custom_bitvector_analysist &cba=
557  static_cast<const custom_bitvector_analysist &>(ai);
558 
559  for(const auto &bit : may_bits)
560  {
561  out << bit.first << " MAY:";
562  bit_vectort b=bit.second;
563 
564  for(unsigned i=0; b!=0; i++, b>>=1)
565  if(b&1)
566  {
567  assert(i<cba.bits.size());
568  out << ' '
569  << cba.bits[i];
570  }
571 
572  out << '\n';
573  }
574 
575  for(const auto &bit : must_bits)
576  {
577  out << bit.first << " MUST:";
578  bit_vectort b=bit.second;
579 
580  for(unsigned i=0; b!=0; i++, b>>=1)
581  if(b&1)
582  {
583  assert(i<cba.bits.size());
584  out << ' '
585  << cba.bits[i];
586  }
587 
588  out << '\n';
589  }
590 }
591 
593  const custom_bitvector_domaint &b,
594  locationt,
595  locationt)
596 {
597  bool changed=has_values.is_false();
599 
600  // first do MAY
601  bitst::iterator it=may_bits.begin();
602  for(const auto &bit : b.may_bits)
603  {
604  while(it!=may_bits.end() && it->first<bit.first)
605  ++it;
606  if(it==may_bits.end() || bit.first<it->first)
607  {
608  may_bits.insert(it, bit);
609  changed=true;
610  }
611  else if(it!=may_bits.end())
612  {
613  bit_vectort &a_bits=it->second;
614  bit_vectort old=a_bits;
615  a_bits|=bit.second;
616  if(old!=a_bits)
617  changed=true;
618 
619  ++it;
620  }
621  }
622 
623  // now do MUST
624  it=must_bits.begin();
625  for(auto &bit : b.must_bits)
626  {
627  while(it!=must_bits.end() && it->first<bit.first)
628  {
629  it=must_bits.erase(it);
630  changed=true;
631  }
632  if(it==must_bits.end() || bit.first<it->first)
633  {
634  must_bits.insert(it, bit);
635  changed=true;
636  }
637  else if(it!=must_bits.end())
638  {
639  bit_vectort &a_bits=it->second;
640  bit_vectort old=a_bits;
641  a_bits&=bit.second;
642  if(old!=a_bits)
643  changed=true;
644 
645  ++it;
646  }
647  }
648 
649  // erase blank ones
652 
653  return changed;
654 }
655 
658 {
659  for(bitst::iterator a_it=bits.begin();
660  a_it!=bits.end();
661  ) // no a_it++
662  {
663  if(a_it->second==0)
664  a_it=bits.erase(a_it);
665  else
666  a_it++;
667  }
668 }
669 
671 {
672  if(src.id()=="get_must" ||
673  src.id()=="get_may")
674  return true;
675 
676  forall_operands(it, src)
677  if(has_get_must_or_may(*it))
678  return true;
679 
680  return false;
681 }
682 
684  const exprt &src,
685  custom_bitvector_analysist &custom_bitvector_analysis) const
686 {
687  if(src.id()=="get_must" || src.id()=="get_may")
688  {
689  if(src.operands().size()==2)
690  {
691  unsigned bit_nr=
692  custom_bitvector_analysis.get_bit_nr(src.op1());
693 
694  exprt pointer=src.op0();
695 
696  if(pointer.type().id()!=ID_pointer)
697  return src;
698 
699  if(pointer.is_constant() &&
700  to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all
701  {
702  if(src.id()=="get_may")
703  {
704  for(const auto &bit : may_bits)
705  if(get_bit(bit.second, bit_nr))
706  return true_exprt();
707 
708  return false_exprt();
709  }
710  else if(src.id()=="get_must")
711  {
712  return false_exprt();
713  }
714  else
715  return src;
716  }
717  else
718  {
720  get_rhs(dereference_exprt(pointer));
721 
722  bool value=false;
723 
724  if(src.id()=="get_must")
725  value=get_bit(v.must_bits, bit_nr);
726  else if(src.id()=="get_may")
727  value=get_bit(v.may_bits, bit_nr);
728 
729  if(value)
730  return true_exprt();
731  else
732  return false_exprt();
733  }
734  }
735  else
736  return src;
737  }
738  else
739  {
740  exprt tmp=src;
741  Forall_operands(it, tmp)
742  *it=eval(*it, custom_bitvector_analysis);
743 
744  return tmp;
745  }
746 }
747 
749 {
750 }
751 
753  const goto_modelt &goto_model,
754  bool use_xml,
755  std::ostream &out)
756 {
757  unsigned pass=0, fail=0, unknown=0;
758 
759  forall_goto_functions(f_it, goto_model.goto_functions)
760  {
761  if(!f_it->second.body.has_assertion())
762  continue;
763 
764  // TODO this is a hard-coded hack
765  if(f_it->first=="__actual_thread_spawn")
766  continue;
767 
768  if(!use_xml)
769  out << "******** Function " << f_it->first << '\n';
770 
771  forall_goto_program_instructions(i_it, f_it->second.body)
772  {
773  exprt result;
774  irep_idt description;
775 
776  if(i_it->is_assert())
777  {
779  continue;
780 
781  if(operator[](i_it).has_values.is_false())
782  continue;
783 
784  exprt tmp=eval(i_it->guard, i_it);
785  const namespacet ns(goto_model.symbol_table);
786  result=simplify_expr(tmp, ns);
787 
788  description=i_it->source_location.get_comment();
789  }
790  else
791  continue;
792 
793  if(use_xml)
794  {
795  out << "<result status=\"";
796  if(result.is_true())
797  out << "SUCCESS";
798  else if(result.is_false())
799  out << "FAILURE";
800  else
801  out << "UNKNOWN";
802  out << "\">\n";
803  out << xml(i_it->source_location);
804  out << "<description>"
805  << description
806  << "</description>\n";
807  out << "</result>\n\n";
808  }
809  else
810  {
811  out << i_it->source_location;
812  if(!description.empty())
813  out << ", " << description;
814  out << ": ";
815  const namespacet ns(goto_model.symbol_table);
816  out << from_expr(ns, f_it->first, result);
817  out << '\n';
818  }
819 
820  if(result.is_true())
821  pass++;
822  else if(result.is_false())
823  fail++;
824  else
825  unknown++;
826  }
827 
828  if(!use_xml)
829  out << '\n';
830  }
831 
832  if(!use_xml)
833  out << "SUMMARY: " << pass << " pass, " << fail << " fail, "
834  << unknown << " unknown\n";
835 }
#define loc()
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
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
how function calls are treated: a) there is an edge from each call site to the function head b) there...
const irep_idt & get_statement() const
Definition: std_code.h:40
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:291
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:44
exprt & object()
Definition: std_expr.h:3178
goto_programt::const_targett locationt
Definition: ai.h:36
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:344
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:268
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
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:4439
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:3199
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:3326
void make_bottom() final override
no states
Extract member of struct or union.
Definition: std_expr.h:3869
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:240
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:209
The boolean constant true.
Definition: std_expr.h:4486
argumentst & arguments()
Definition: std_code.h:890
A declaration of a local variable.
Definition: std_code.h:254
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
bool is_known() const
Definition: threeval.h:28
exprt & rhs()
Definition: std_code.h:214
void set_bit(const exprt &, unsigned bit_nr, modet)
Operator to dereference a pointer.
Definition: std_expr.h:3282
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:3953
A function call.
Definition: std_code.h:858
#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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
exprt & symbol()
Definition: std_code.h:321
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
The boolean constant false.
Definition: std_expr.h:4497
bool is_constant() const
Definition: expr.cpp:119
void make_not()
Definition: expr.cpp:91
exprt & function()
Definition: std_code.h:878
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3305
const parameterst & parameters() const
Definition: std_types.h:905
#define UNREACHABLE
Definition: invariant.h:271
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:307
#define Forall_operands(it, expr)
Definition: expr.h:23
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:90
dstringt irep_idt
Definition: irep.h:32
#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:73
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:136
Assignment.
Definition: std_code.h:196
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909