cprover
goto_check.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: GOTO Programs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_check.h"
13 
14 #include <algorithm>
15 
16 #include <util/arith_tools.h>
17 #include <util/array_name.h>
18 #include <util/c_types.h>
19 #include <util/config.h>
20 #include <util/cprover_prefix.h>
21 #include <util/expr_util.h>
22 #include <util/find_symbols.h>
23 #include <util/ieee_float.h>
24 #include <util/invariant.h>
25 #include <util/make_unique.h>
26 #include <util/options.h>
29 #include <util/prefix.h>
30 #include <util/simplify_expr.h>
31 #include <util/std_expr.h>
32 #include <util/std_types.h>
33 
34 #include <langapi/language.h>
35 #include <langapi/mode.h>
36 
38 
39 #include "guard.h"
41 
43 {
44 public:
46  const namespacet &_ns,
47  const optionst &_options):
48  ns(_ns),
50  {
51  no_enum_check = false;
52  enable_bounds_check=_options.get_bool_option("bounds-check");
53  enable_pointer_check=_options.get_bool_option("pointer-check");
54  enable_memory_leak_check=_options.get_bool_option("memory-leak-check");
55  enable_div_by_zero_check=_options.get_bool_option("div-by-zero-check");
56  enable_enum_range_check = _options.get_bool_option("enum-range-check");
58  _options.get_bool_option("signed-overflow-check");
60  _options.get_bool_option("unsigned-overflow-check");
62  _options.get_bool_option("pointer-overflow-check");
63  enable_conversion_check=_options.get_bool_option("conversion-check");
65  _options.get_bool_option("undefined-shift-check");
67  _options.get_bool_option("float-overflow-check");
68  enable_simplify=_options.get_bool_option("simplify");
69  enable_nan_check=_options.get_bool_option("nan-check");
70  retain_trivial=_options.get_bool_option("retain-trivial");
71  enable_assert_to_assume=_options.get_bool_option("assert-to-assume");
72  enable_assertions=_options.get_bool_option("assertions");
73  enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
74  enable_assumptions=_options.get_bool_option("assumptions");
75  error_labels=_options.get_list_option("error-label");
77  _options.get_bool_option("pointer-primitive-check");
78  }
79 
81 
82  void goto_check(
83  const irep_idt &function_identifier,
84  goto_functiont &goto_function);
85 
91  void collect_allocations(const goto_functionst &goto_functions);
92 
93 protected:
94  const namespacet &ns;
95  std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
99 
105  void check_rec_address(const exprt &expr, guardt &guard);
106 
114  void check_rec_logical_op(const exprt &expr, guardt &guard);
115 
122  void check_rec_if(const if_exprt &if_expr, guardt &guard);
123 
134  bool check_rec_member(const member_exprt &member, guardt &guard);
135 
140  void check_rec_div(const div_exprt &div_expr, guardt &guard);
141 
146  void check_rec_arithmetic_op(const exprt &expr, guardt &guard);
147 
153  void check_rec(const exprt &expr, guardt &guard);
154 
157  void check(const exprt &expr);
158 
159  struct conditiont
160  {
161  conditiont(const exprt &_assertion, const std::string &_description)
162  : assertion(_assertion), description(_description)
163  {
164  }
165 
167  std::string description;
168  };
169 
170  using conditionst = std::list<conditiont>;
171 
172  void bounds_check(const index_exprt &, const guardt &);
173  void div_by_zero_check(const div_exprt &, const guardt &);
174  void mod_by_zero_check(const mod_exprt &, const guardt &);
175  void mod_overflow_check(const mod_exprt &, const guardt &);
176  void enum_range_check(const exprt &, const guardt &);
177  void undefined_shift_check(const shift_exprt &, const guardt &);
178  void pointer_rel_check(const binary_relation_exprt &, const guardt &);
179  void pointer_overflow_check(const exprt &, const guardt &);
180 
187  const dereference_exprt &expr,
188  const exprt &src_expr,
189  const guardt &guard);
190 
196  void pointer_primitive_check(const exprt &expr, const guardt &guard);
197 
203  bool is_pointer_primitive(const exprt &expr);
204 
205  conditionst address_check(const exprt &address, const exprt &size);
206  void integer_overflow_check(const exprt &, const guardt &);
207  void conversion_check(const exprt &, const guardt &);
208  void float_overflow_check(const exprt &, const guardt &);
209  void nan_check(const exprt &, const guardt &);
211 
212  std::string array_name(const exprt &);
213 
223  const exprt &asserted_expr,
224  const std::string &comment,
225  const std::string &property_class,
226  const source_locationt &source_location,
227  const exprt &src_expr,
228  const guardt &guard);
229 
231  typedef std::set<exprt> assertionst;
233 
238  void invalidate(const exprt &lhs);
239 
259 
262 
263  // the first element of the pair is the base address,
264  // and the second is the size of the region
265  typedef std::pair<exprt, exprt> allocationt;
266  typedef std::list<allocationt> allocationst;
268 
270 };
271 
273  const goto_functionst &goto_functions)
274 {
276  return;
277 
278  forall_goto_functions(itf, goto_functions)
279  forall_goto_program_instructions(it, itf->second.body)
280  {
281  const goto_programt::instructiont &instruction=*it;
282  if(!instruction.is_function_call())
283  continue;
284 
285  const code_function_callt &call=
286  to_code_function_call(instruction.code);
287  if(call.function().id()!=ID_symbol ||
289  CPROVER_PREFIX "allocated_memory")
290  continue;
291 
292  const code_function_callt::argumentst &args= call.arguments();
293  if(args.size()!=2 ||
294  args[0].type().id()!=ID_unsignedbv ||
295  args[1].type().id()!=ID_unsignedbv)
296  throw "expected two unsigned arguments to "
297  CPROVER_PREFIX "allocated_memory";
298 
299  assert(args[0].type()==args[1].type());
300  allocations.push_back({args[0], args[1]});
301  }
302 }
303 
305 {
306  if(lhs.id()==ID_index)
307  invalidate(to_index_expr(lhs).array());
308  else if(lhs.id()==ID_member)
309  invalidate(to_member_expr(lhs).struct_op());
310  else if(lhs.id()==ID_symbol)
311  {
312  // clear all assertions about 'symbol'
313  find_symbols_sett find_symbols_set{to_symbol_expr(lhs).get_identifier()};
314 
315  for(auto it = assertions.begin(); it != assertions.end();)
316  {
317  if(has_symbol(*it, find_symbols_set) || has_subexpr(*it, ID_dereference))
318  it = assertions.erase(it);
319  else
320  ++it;
321  }
322  }
323  else
324  {
325  // give up, clear all
326  assertions.clear();
327  }
328 }
329 
331  const div_exprt &expr,
332  const guardt &guard)
333 {
335  return;
336 
337  // add divison by zero subgoal
338 
339  exprt zero=from_integer(0, expr.op1().type());
340  const notequal_exprt inequality(expr.op1(), std::move(zero));
341 
343  inequality,
344  "division by zero",
345  "division-by-zero",
346  expr.find_source_location(),
347  expr,
348  guard);
349 }
350 
351 void goto_checkt::enum_range_check(const exprt &expr, const guardt &guard)
352 {
354  return;
355 
356  const c_enum_tag_typet &c_enum_tag_type = to_c_enum_tag_type(expr.type());
357  symbolt enum_type = ns.lookup(c_enum_tag_type.get_identifier());
358  const c_enum_typet &c_enum_type = to_c_enum_type(enum_type.type);
359 
360  const c_enum_typet::memberst enum_values = c_enum_type.members();
361 
362  std::vector<exprt> disjuncts;
363  for(const auto &enum_value : enum_values)
364  {
365  const constant_exprt val{enum_value.get_value(), c_enum_tag_type};
366  disjuncts.push_back(equal_exprt(expr, val));
367  }
368 
369  const exprt check = disjunction(disjuncts);
370 
372  check,
373  "enum range check",
374  "enum-range-check",
375  expr.find_source_location(),
376  expr,
377  guard);
378 }
379 
381  const shift_exprt &expr,
382  const guardt &guard)
383 {
385  return;
386 
387  // Undefined for all types and shifts if distance exceeds width,
388  // and also undefined for negative distances.
389 
390  const typet &distance_type = expr.distance().type();
391 
392  if(distance_type.id()==ID_signedbv)
393  {
394  binary_relation_exprt inequality(
395  expr.distance(), ID_ge, from_integer(0, distance_type));
396 
398  inequality,
399  "shift distance is negative",
400  "undefined-shift",
401  expr.find_source_location(),
402  expr,
403  guard);
404  }
405 
406  const typet &op_type = expr.op().type();
407 
408  if(op_type.id()==ID_unsignedbv || op_type.id()==ID_signedbv)
409  {
410  exprt width_expr=
411  from_integer(to_bitvector_type(op_type).get_width(), distance_type);
412 
414  binary_relation_exprt(expr.distance(), ID_lt, std::move(width_expr)),
415  "shift distance too large",
416  "undefined-shift",
417  expr.find_source_location(),
418  expr,
419  guard);
420 
421  if(op_type.id()==ID_signedbv && expr.id()==ID_shl)
422  {
423  binary_relation_exprt inequality(
424  expr.op(), ID_ge, from_integer(0, op_type));
425 
427  inequality,
428  "shift operand is negative",
429  "undefined-shift",
430  expr.find_source_location(),
431  expr,
432  guard);
433  }
434  }
435  else
436  {
438  false_exprt(),
439  "shift of non-integer type",
440  "undefined-shift",
441  expr.find_source_location(),
442  expr,
443  guard);
444  }
445 }
446 
448  const mod_exprt &expr,
449  const guardt &guard)
450 {
451  if(!enable_div_by_zero_check || mode == ID_java)
452  return;
453 
454  // add divison by zero subgoal
455 
456  exprt zero=from_integer(0, expr.op1().type());
457  const notequal_exprt inequality(expr.op1(), std::move(zero));
458 
460  inequality,
461  "division by zero",
462  "division-by-zero",
463  expr.find_source_location(),
464  expr,
465  guard);
466 }
467 
469 void goto_checkt::mod_overflow_check(const mod_exprt &expr, const guardt &guard)
470 {
472  return;
473 
474  const auto &type = expr.type();
475 
476  if(type.id() == ID_signedbv)
477  {
478  // INT_MIN % -1 is, in principle, defined to be zero in
479  // ANSI C, C99, C++98, and C++11. Most compilers, however,
480  // fail to produce 0, and in some cases generate an exception.
481  // C11 explicitly makes this case undefined.
482 
483  notequal_exprt int_min_neq(
484  expr.op0(), to_signedbv_type(type).smallest_expr());
485 
486  notequal_exprt minus_one_neq(
487  expr.op1(), from_integer(-1, expr.op1().type()));
488 
490  or_exprt(int_min_neq, minus_one_neq),
491  "result of signed mod is not representable",
492  "overflow",
493  expr.find_source_location(),
494  expr,
495  guard);
496  }
497 }
498 
500  const exprt &expr,
501  const guardt &guard)
502 {
504  return;
505 
506  // First, check type.
507  const typet &type = expr.type();
508 
509  if(type.id()!=ID_signedbv &&
510  type.id()!=ID_unsignedbv)
511  return;
512 
513  if(expr.id()==ID_typecast)
514  {
515  const auto &op = to_typecast_expr(expr).op();
516 
517  // conversion to signed int may overflow
518  const typet &old_type = op.type();
519 
520  if(type.id()==ID_signedbv)
521  {
522  std::size_t new_width=to_signedbv_type(type).get_width();
523 
524  if(old_type.id()==ID_signedbv) // signed -> signed
525  {
526  std::size_t old_width=to_signedbv_type(old_type).get_width();
527  if(new_width>=old_width)
528  return; // always ok
529 
530  const binary_relation_exprt no_overflow_upper(
531  op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
532 
533  const binary_relation_exprt no_overflow_lower(
534  op, ID_ge, from_integer(-power(2, new_width - 1), old_type));
535 
537  and_exprt(no_overflow_lower, no_overflow_upper),
538  "arithmetic overflow on signed type conversion",
539  "overflow",
540  expr.find_source_location(),
541  expr,
542  guard);
543  }
544  else if(old_type.id()==ID_unsignedbv) // unsigned -> signed
545  {
546  std::size_t old_width=to_unsignedbv_type(old_type).get_width();
547  if(new_width>=old_width+1)
548  return; // always ok
549 
550  const binary_relation_exprt no_overflow_upper(
551  op, ID_le, from_integer(power(2, new_width - 1) - 1, old_type));
552 
554  no_overflow_upper,
555  "arithmetic overflow on unsigned to signed type conversion",
556  "overflow",
557  expr.find_source_location(),
558  expr,
559  guard);
560  }
561  else if(old_type.id()==ID_floatbv) // float -> signed
562  {
563  // Note that the fractional part is truncated!
564  ieee_floatt upper(to_floatbv_type(old_type));
565  upper.from_integer(power(2, new_width-1));
566  const binary_relation_exprt no_overflow_upper(
567  op, ID_lt, upper.to_expr());
568 
569  ieee_floatt lower(to_floatbv_type(old_type));
570  lower.from_integer(-power(2, new_width-1)-1);
571  const binary_relation_exprt no_overflow_lower(
572  op, ID_gt, lower.to_expr());
573 
575  and_exprt(no_overflow_lower, no_overflow_upper),
576  "arithmetic overflow on float to signed integer type conversion",
577  "overflow",
578  expr.find_source_location(),
579  expr,
580  guard);
581  }
582  }
583  else if(type.id()==ID_unsignedbv)
584  {
585  std::size_t new_width=to_unsignedbv_type(type).get_width();
586 
587  if(old_type.id()==ID_signedbv) // signed -> unsigned
588  {
589  std::size_t old_width=to_signedbv_type(old_type).get_width();
590 
591  if(new_width>=old_width-1)
592  {
593  // only need lower bound check
594  const binary_relation_exprt no_overflow_lower(
595  op, ID_ge, from_integer(0, old_type));
596 
598  no_overflow_lower,
599  "arithmetic overflow on signed to unsigned type conversion",
600  "overflow",
601  expr.find_source_location(),
602  expr,
603  guard);
604  }
605  else
606  {
607  // need both
608  const binary_relation_exprt no_overflow_upper(
609  op, ID_le, from_integer(power(2, new_width) - 1, old_type));
610 
611  const binary_relation_exprt no_overflow_lower(
612  op, ID_ge, from_integer(0, old_type));
613 
615  and_exprt(no_overflow_lower, no_overflow_upper),
616  "arithmetic overflow on signed to unsigned type conversion",
617  "overflow",
618  expr.find_source_location(),
619  expr,
620  guard);
621  }
622  }
623  else if(old_type.id()==ID_unsignedbv) // unsigned -> unsigned
624  {
625  std::size_t old_width=to_unsignedbv_type(old_type).get_width();
626  if(new_width>=old_width)
627  return; // always ok
628 
629  const binary_relation_exprt no_overflow_upper(
630  op, ID_le, from_integer(power(2, new_width) - 1, old_type));
631 
633  no_overflow_upper,
634  "arithmetic overflow on unsigned to unsigned type conversion",
635  "overflow",
636  expr.find_source_location(),
637  expr,
638  guard);
639  }
640  else if(old_type.id()==ID_floatbv) // float -> unsigned
641  {
642  // Note that the fractional part is truncated!
643  ieee_floatt upper(to_floatbv_type(old_type));
644  upper.from_integer(power(2, new_width)-1);
645  const binary_relation_exprt no_overflow_upper(
646  op, ID_lt, upper.to_expr());
647 
648  ieee_floatt lower(to_floatbv_type(old_type));
649  lower.from_integer(-1);
650  const binary_relation_exprt no_overflow_lower(
651  op, ID_gt, lower.to_expr());
652 
654  and_exprt(no_overflow_lower, no_overflow_upper),
655  "arithmetic overflow on float to unsigned integer type conversion",
656  "overflow",
657  expr.find_source_location(),
658  expr,
659  guard);
660  }
661  }
662  }
663 }
664 
666  const exprt &expr,
667  const guardt &guard)
668 {
671  return;
672 
673  // First, check type.
674  const typet &type = expr.type();
675 
676  if(type.id()==ID_signedbv && !enable_signed_overflow_check)
677  return;
678 
679  if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check)
680  return;
681 
682  // add overflow subgoal
683 
684  if(expr.id()==ID_div)
685  {
686  // undefined for signed division INT_MIN/-1
687  if(type.id()==ID_signedbv)
688  {
689  const auto &div_expr = to_div_expr(expr);
690 
691  equal_exprt int_min_eq(
692  div_expr.dividend(), to_signedbv_type(type).smallest_expr());
693 
694  equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
695 
697  not_exprt(and_exprt(int_min_eq, minus_one_eq)),
698  "arithmetic overflow on signed division",
699  "overflow",
700  expr.find_source_location(),
701  expr,
702  guard);
703  }
704 
705  return;
706  }
707  else if(expr.id()==ID_unary_minus)
708  {
709  if(type.id()==ID_signedbv)
710  {
711  // overflow on unary- can only happen with the smallest
712  // representable number 100....0
713 
714  equal_exprt int_min_eq(
715  to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr());
716 
718  not_exprt(int_min_eq),
719  "arithmetic overflow on signed unary minus",
720  "overflow",
721  expr.find_source_location(),
722  expr,
723  guard);
724  }
725 
726  return;
727  }
728  else if(expr.id() == ID_shl)
729  {
730  if(type.id() == ID_signedbv)
731  {
732  const auto &shl_expr = to_shl_expr(expr);
733  const auto &op = shl_expr.op();
734  const auto &op_type = to_signedbv_type(type);
735  const auto op_width = op_type.get_width();
736  const auto &distance = shl_expr.distance();
737  const auto &distance_type = distance.type();
738 
739  // a left shift of a negative value is undefined;
740  // yet this isn't an overflow
741  exprt neg_value_shift;
742 
743  if(op_type.id() == ID_unsignedbv)
744  neg_value_shift = false_exprt();
745  else
746  neg_value_shift =
747  binary_relation_exprt(op, ID_lt, from_integer(0, op_type));
748 
749  // a shift with negative distance is undefined;
750  // yet this isn't an overflow
751  exprt neg_dist_shift;
752 
753  if(distance_type.id() == ID_unsignedbv)
754  neg_dist_shift = false_exprt();
755  else
756  neg_dist_shift =
757  binary_relation_exprt(op, ID_lt, from_integer(0, distance_type));
758 
759  // shifting a non-zero value by more than its width is undefined;
760  // yet this isn't an overflow
761  const exprt dist_too_large = binary_predicate_exprt(
762  distance, ID_gt, from_integer(op_width, distance_type));
763 
764  const exprt op_zero = equal_exprt(op, from_integer(0, op_type));
765 
766  auto new_type = to_bitvector_type(op_type);
767  new_type.set_width(op_width * 2);
768 
769  const exprt op_ext = typecast_exprt(op, new_type);
770 
771  const exprt op_ext_shifted = shl_exprt(op_ext, distance);
772 
773  // The semantics of signed left shifts are contentious for the case
774  // that a '1' is shifted into the signed bit.
775  // Assuming 32-bit integers, 1<<31 is implementation-defined
776  // in ANSI C and C++98, but is explicitly undefined by C99,
777  // C11 and C++11.
778  bool allow_shift_into_sign_bit = true;
779 
780  if(mode == ID_C)
781  {
782  if(
785  {
786  allow_shift_into_sign_bit = false;
787  }
788  }
789  else if(mode == ID_cpp)
790  {
791  if(
794  {
795  allow_shift_into_sign_bit = false;
796  }
797  }
798 
799  const unsigned number_of_top_bits =
800  allow_shift_into_sign_bit ? op_width : op_width + 1;
801 
802  const exprt top_bits = extractbits_exprt(
803  op_ext_shifted,
804  new_type.get_width() - 1,
805  new_type.get_width() - number_of_top_bits,
806  unsignedbv_typet(number_of_top_bits));
807 
808  const exprt top_bits_zero =
809  equal_exprt(top_bits, from_integer(0, top_bits.type()));
810 
811  // a negative distance shift isn't an overflow;
812  // a negative value shift isn't an overflow;
813  // a shift that's too far isn't an overflow;
814  // a shift of zero isn't overflow;
815  // else check the top bits
817  disjunction({neg_value_shift,
818  neg_dist_shift,
819  dist_too_large,
820  op_zero,
821  top_bits_zero}),
822  "arithmetic overflow on signed shl",
823  "overflow",
824  expr.find_source_location(),
825  expr,
826  guard);
827  }
828 
829  return;
830  }
831 
832  multi_ary_exprt overflow(
833  "overflow-" + expr.id_string(), expr.operands(), bool_typet());
834 
835  if(expr.operands().size()>=3)
836  {
837  // The overflow checks are binary!
838  // We break these up.
839 
840  for(std::size_t i=1; i<expr.operands().size(); i++)
841  {
842  exprt tmp;
843 
844  if(i==1)
845  tmp = to_multi_ary_expr(expr).op0();
846  else
847  {
848  tmp=expr;
849  tmp.operands().resize(i);
850  }
851 
852  overflow.operands().resize(2);
853  overflow.op0()=tmp;
854  overflow.op1()=expr.operands()[i];
855 
856  std::string kind=
857  type.id()==ID_unsignedbv?"unsigned":"signed";
858 
860  not_exprt(overflow),
861  "arithmetic overflow on " + kind + " " + expr.id_string(),
862  "overflow",
863  expr.find_source_location(),
864  expr,
865  guard);
866  }
867  }
868  else
869  {
870  std::string kind=
871  type.id()==ID_unsignedbv?"unsigned":"signed";
872 
874  not_exprt(overflow),
875  "arithmetic overflow on " + kind + " " + expr.id_string(),
876  "overflow",
877  expr.find_source_location(),
878  expr,
879  guard);
880  }
881 }
882 
884  const exprt &expr,
885  const guardt &guard)
886 {
888  return;
889 
890  // First, check type.
891  const typet &type = expr.type();
892 
893  if(type.id()!=ID_floatbv)
894  return;
895 
896  // add overflow subgoal
897 
898  if(expr.id()==ID_typecast)
899  {
900  // Can overflow if casting from larger
901  // to smaller type.
902  const auto &op = to_typecast_expr(expr).op();
903  if(op.type().id() == ID_floatbv)
904  {
905  // float-to-float
906  or_exprt overflow_check{isinf_exprt(op), not_exprt(isinf_exprt(expr))};
907 
909  std::move(overflow_check),
910  "arithmetic overflow on floating-point typecast",
911  "overflow",
912  expr.find_source_location(),
913  expr,
914  guard);
915  }
916  else
917  {
918  // non-float-to-float
920  not_exprt(isinf_exprt(expr)),
921  "arithmetic overflow on floating-point typecast",
922  "overflow",
923  expr.find_source_location(),
924  expr,
925  guard);
926  }
927 
928  return;
929  }
930  else if(expr.id()==ID_div)
931  {
932  // Can overflow if dividing by something small
933  or_exprt overflow_check(
934  isinf_exprt(to_div_expr(expr).dividend()), not_exprt(isinf_exprt(expr)));
935 
937  std::move(overflow_check),
938  "arithmetic overflow on floating-point division",
939  "overflow",
940  expr.find_source_location(),
941  expr,
942  guard);
943 
944  return;
945  }
946  else if(expr.id()==ID_mod)
947  {
948  // Can't overflow
949  return;
950  }
951  else if(expr.id()==ID_unary_minus)
952  {
953  // Can't overflow
954  return;
955  }
956  else if(expr.id()==ID_plus || expr.id()==ID_mult ||
957  expr.id()==ID_minus)
958  {
959  if(expr.operands().size()==2)
960  {
961  // Can overflow
962  or_exprt overflow_check(
963  isinf_exprt(to_binary_expr(expr).op0()),
964  isinf_exprt(to_binary_expr(expr).op1()),
965  not_exprt(isinf_exprt(expr)));
966 
967  std::string kind=
968  expr.id()==ID_plus?"addition":
969  expr.id()==ID_minus?"subtraction":
970  expr.id()==ID_mult?"multiplication":"";
971 
973  std::move(overflow_check),
974  "arithmetic overflow on floating-point " + kind,
975  "overflow",
976  expr.find_source_location(),
977  expr,
978  guard);
979 
980  return;
981  }
982  else if(expr.operands().size()>=3)
983  {
984  assert(expr.id()!=ID_minus);
985 
986  // break up
987  float_overflow_check(make_binary(expr), guard);
988  return;
989  }
990  }
991 }
992 
994  const exprt &expr,
995  const guardt &guard)
996 {
997  if(!enable_nan_check)
998  return;
999 
1000  // first, check type
1001  if(expr.type().id()!=ID_floatbv)
1002  return;
1003 
1004  if(expr.id()!=ID_plus &&
1005  expr.id()!=ID_mult &&
1006  expr.id()!=ID_div &&
1007  expr.id()!=ID_minus)
1008  return;
1009 
1010  // add NaN subgoal
1011 
1012  exprt isnan;
1013 
1014  if(expr.id()==ID_div)
1015  {
1016  const auto &div_expr = to_div_expr(expr);
1017 
1018  // there a two ways to get a new NaN on division:
1019  // 0/0 = NaN and x/inf = NaN
1020  // (note that x/0 = +-inf for x!=0 and x!=inf)
1021  const and_exprt zero_div_zero(
1023  div_expr.op0(), from_integer(0, div_expr.dividend().type())),
1025  div_expr.op1(), from_integer(0, div_expr.divisor().type())));
1026 
1027  const isinf_exprt div_inf(div_expr.op1());
1028 
1029  isnan=or_exprt(zero_div_zero, div_inf);
1030  }
1031  else if(expr.id()==ID_mult)
1032  {
1033  if(expr.operands().size()>=3)
1034  return nan_check(make_binary(expr), guard);
1035 
1036  const auto &mult_expr = to_mult_expr(expr);
1037 
1038  // Inf * 0 is NaN
1039  const and_exprt inf_times_zero(
1040  isinf_exprt(mult_expr.op0()),
1042  mult_expr.op1(), from_integer(0, mult_expr.op1().type())));
1043 
1044  const and_exprt zero_times_inf(
1046  mult_expr.op1(), from_integer(0, mult_expr.op1().type())),
1047  isinf_exprt(mult_expr.op0()));
1048 
1049  isnan=or_exprt(inf_times_zero, zero_times_inf);
1050  }
1051  else if(expr.id()==ID_plus)
1052  {
1053  if(expr.operands().size()>=3)
1054  return nan_check(make_binary(expr), guard);
1055 
1056  const auto &plus_expr = to_plus_expr(expr);
1057 
1058  // -inf + +inf = NaN and +inf + -inf = NaN,
1059  // i.e., signs differ
1060  ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
1061  exprt plus_inf=ieee_floatt::plus_infinity(spec).to_expr();
1062  exprt minus_inf=ieee_floatt::minus_infinity(spec).to_expr();
1063 
1064  isnan = or_exprt(
1065  and_exprt(
1066  equal_exprt(plus_expr.op0(), minus_inf),
1067  equal_exprt(plus_expr.op1(), plus_inf)),
1068  and_exprt(
1069  equal_exprt(plus_expr.op0(), plus_inf),
1070  equal_exprt(plus_expr.op1(), minus_inf)));
1071  }
1072  else if(expr.id()==ID_minus)
1073  {
1074  // +inf - +inf = NaN and -inf - -inf = NaN,
1075  // i.e., signs match
1076 
1077  const auto &minus_expr = to_minus_expr(expr);
1078 
1079  ieee_float_spect spec =
1080  ieee_float_spect(to_floatbv_type(minus_expr.type()));
1081  exprt plus_inf=ieee_floatt::plus_infinity(spec).to_expr();
1082  exprt minus_inf=ieee_floatt::minus_infinity(spec).to_expr();
1083 
1084  isnan = or_exprt(
1085  and_exprt(
1086  equal_exprt(minus_expr.lhs(), plus_inf),
1087  equal_exprt(minus_expr.rhs(), plus_inf)),
1088  and_exprt(
1089  equal_exprt(minus_expr.lhs(), minus_inf),
1090  equal_exprt(minus_expr.rhs(), minus_inf)));
1091  }
1092  else
1093  UNREACHABLE;
1094 
1096  boolean_negate(isnan),
1097  "NaN on " + expr.id_string(),
1098  "NaN",
1099  expr.find_source_location(),
1100  expr,
1101  guard);
1102 }
1103 
1105  const binary_relation_exprt &expr,
1106  const guardt &guard)
1107 {
1109  return;
1110 
1111  if(expr.op0().type().id()==ID_pointer &&
1112  expr.op1().type().id()==ID_pointer)
1113  {
1114  // add same-object subgoal
1115 
1117  {
1118  exprt same_object=::same_object(expr.op0(), expr.op1());
1119 
1121  same_object,
1122  "same object violation",
1123  "pointer",
1124  expr.find_source_location(),
1125  expr,
1126  guard);
1127  }
1128  }
1129 }
1130 
1132  const exprt &expr,
1133  const guardt &guard)
1134 {
1136  return;
1137 
1138  if(expr.id() != ID_plus && expr.id() != ID_minus)
1139  return;
1140 
1142  expr.operands().size() == 2,
1143  "pointer arithmetic expected to have exactly 2 operands");
1144 
1145  exprt overflow("overflow-" + expr.id_string(), bool_typet());
1146  overflow.operands() = expr.operands();
1147 
1149  not_exprt(overflow),
1150  "pointer arithmetic overflow on " + expr.id_string(),
1151  "overflow",
1152  expr.find_source_location(),
1153  expr,
1154  guard);
1155 }
1156 
1158  const dereference_exprt &expr,
1159  const exprt &src_expr,
1160  const guardt &guard)
1161 {
1163  return;
1164 
1165  const exprt &pointer=expr.pointer();
1166 
1167  exprt size;
1168 
1169  if(expr.type().id() == ID_empty)
1170  {
1171  // a dereference *p (with p being a pointer to void) is valid if p points to
1172  // valid memory (of any size). the smallest possible size of the memory
1173  // segment p could be pointing to is 1, hence we use this size for the
1174  // address check
1175  size = from_integer(1, size_type());
1176  }
1177  else
1178  {
1179  auto size_of_expr_opt = size_of_expr(expr.type(), ns);
1180  CHECK_RETURN(size_of_expr_opt.has_value());
1181  size = size_of_expr_opt.value();
1182  }
1183 
1184  auto conditions = address_check(pointer, size);
1185 
1186  for(const auto &c : conditions)
1187  {
1189  c.assertion,
1190  "dereference failure: " + c.description,
1191  "pointer dereference",
1192  src_expr.find_source_location(),
1193  src_expr,
1194  guard);
1195  }
1196 }
1197 
1199  const exprt &expr,
1200  const guardt &guard)
1201 {
1203  return;
1204 
1205  if(expr.source_location().is_built_in())
1206  return;
1207 
1208  const exprt pointer = (expr.id() == ID_r_ok || expr.id() == ID_w_ok)
1209  ? to_binary_expr(expr).lhs()
1210  : to_unary_expr(expr).op();
1211 
1212  CHECK_RETURN(pointer.type().id() == ID_pointer);
1213 
1214  if(pointer.id() == ID_symbol)
1215  {
1216  const auto &symbol_expr = to_symbol_expr(pointer);
1217 
1218  if(has_prefix(id2string(symbol_expr.get_identifier()), CPROVER_PREFIX))
1219  return;
1220  }
1221 
1222  const auto size_of_expr_opt = size_of_expr(pointer.type().subtype(), ns);
1223 
1224  const exprt size = !size_of_expr_opt.has_value()
1225  ? from_integer(1, size_type())
1226  : size_of_expr_opt.value();
1227 
1228  const conditionst &conditions = address_check(pointer, size);
1229 
1230  exprt::operandst conjuncts;
1231 
1232  for(const auto &c : conditions)
1233  conjuncts.push_back(c.assertion);
1234 
1235  const or_exprt or_expr(null_object(pointer), conjunction(conjuncts));
1236 
1238  or_expr,
1239  "pointer in pointer primitive is neither null nor valid",
1240  "pointer primitives",
1241  expr.source_location(),
1242  expr,
1243  guard);
1244 }
1245 
1247 {
1248  // we don't need to include the __CPROVER_same_object primitive here as it
1249  // is replaced by lower level primitives in the special function handling
1250  // during typechecking (see c_typecheck_expr.cpp)
1251  return expr.id() == ID_pointer_object || expr.id() == ID_pointer_offset ||
1252  expr.id() == ID_object_size || expr.id() == ID_r_ok ||
1253  expr.id() == ID_w_ok || expr.id() == ID_is_dynamic_object;
1254 }
1255 
1257 goto_checkt::address_check(const exprt &address, const exprt &size)
1258 {
1260  PRECONDITION(address.type().id() == ID_pointer);
1261  const auto &pointer_type = to_pointer_type(address.type());
1262 
1265 
1266  // For Java, we only need to check for null
1267  if(mode == ID_java)
1268  {
1269  if(flags.is_unknown() || flags.is_null())
1270  {
1271  notequal_exprt not_eq_null(address, null_pointer_exprt(pointer_type));
1272 
1273  return {conditiont(not_eq_null, "reference is null")};
1274  }
1275  else
1276  return {};
1277  }
1278  else
1279  {
1280  conditionst conditions;
1281  exprt::operandst alloc_disjuncts;
1282 
1283  for(const auto &a : allocations)
1284  {
1285  typecast_exprt int_ptr(address, a.first.type());
1286 
1287  binary_relation_exprt lb_check(a.first, ID_le, int_ptr);
1288 
1289  plus_exprt ub{int_ptr, size};
1290 
1291  binary_relation_exprt ub_check(ub, ID_le, plus_exprt(a.first, a.second));
1292 
1293  alloc_disjuncts.push_back(and_exprt(lb_check, ub_check));
1294  }
1295 
1296  const exprt in_bounds_of_some_explicit_allocation =
1297  disjunction(alloc_disjuncts);
1298 
1299  const bool unknown = flags.is_unknown() || flags.is_uninitialized();
1300 
1301  if(unknown)
1302  {
1303  conditions.push_back(conditiont{
1304  not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
1305  }
1306 
1307  if(unknown || flags.is_null())
1308  {
1309  conditions.push_back(conditiont(
1310  or_exprt(
1311  in_bounds_of_some_explicit_allocation,
1312  not_exprt(null_pointer(address))),
1313  "pointer NULL"));
1314  }
1315 
1316  if(unknown || flags.is_dynamic_heap())
1317  {
1318  conditions.push_back(conditiont(
1319  or_exprt(
1320  in_bounds_of_some_explicit_allocation,
1321  not_exprt(deallocated(address, ns))),
1322  "deallocated dynamic object"));
1323  }
1324 
1325  if(unknown || flags.is_dynamic_local())
1326  {
1327  conditions.push_back(conditiont(
1328  or_exprt(
1329  in_bounds_of_some_explicit_allocation,
1330  not_exprt(dead_object(address, ns))),
1331  "dead object"));
1332  }
1333 
1334  if(unknown || flags.is_dynamic_heap())
1335  {
1336  const or_exprt object_bounds_violation(
1337  object_lower_bound(address, nil_exprt()),
1338  object_upper_bound(address, size));
1339 
1340  conditions.push_back(conditiont(
1341  or_exprt(
1342  in_bounds_of_some_explicit_allocation,
1343  implies_exprt(
1344  dynamic_object(address), not_exprt(object_bounds_violation))),
1345  "pointer outside dynamic object bounds"));
1346  }
1347 
1348  if(unknown || flags.is_dynamic_local() || flags.is_static_lifetime())
1349  {
1350  const or_exprt object_bounds_violation(
1351  object_lower_bound(address, nil_exprt()),
1352  object_upper_bound(address, size));
1353 
1354  conditions.push_back(conditiont(
1355  or_exprt(
1356  in_bounds_of_some_explicit_allocation,
1357  implies_exprt(
1358  not_exprt(dynamic_object(address)),
1359  not_exprt(object_bounds_violation))),
1360  "pointer outside object bounds"));
1361  }
1362 
1363  if(unknown || flags.is_integer_address())
1364  {
1365  conditions.push_back(conditiont(
1366  implies_exprt(
1367  integer_address(address), in_bounds_of_some_explicit_allocation),
1368  "invalid integer address"));
1369  }
1370 
1371  return conditions;
1372  }
1373 }
1374 
1375 std::string goto_checkt::array_name(const exprt &expr)
1376 {
1377  return ::array_name(ns, expr);
1378 }
1379 
1381  const index_exprt &expr,
1382  const guardt &guard)
1383 {
1384  if(!enable_bounds_check)
1385  return;
1386 
1387  if(expr.find("bounds_check").is_not_nil() &&
1388  !expr.get_bool("bounds_check"))
1389  return;
1390 
1391  typet array_type = expr.array().type();
1392 
1393  if(array_type.id()==ID_pointer)
1394  throw "index got pointer as array type";
1395  else if(array_type.id()!=ID_array && array_type.id()!=ID_vector)
1396  throw "bounds check expected array or vector type, got "
1397  +array_type.id_string();
1398 
1399  std::string name=array_name(expr.array());
1400 
1401  const exprt &index=expr.index();
1403  ode.build(expr, ns);
1404 
1405  if(index.type().id()!=ID_unsignedbv)
1406  {
1407  // we undo typecasts to signedbv
1408  if(
1409  index.id() == ID_typecast &&
1410  to_typecast_expr(index).op().type().id() == ID_unsignedbv)
1411  {
1412  // ok
1413  }
1414  else
1415  {
1416  const auto i = numeric_cast<mp_integer>(index);
1417 
1418  if(!i.has_value() || *i < 0)
1419  {
1420  exprt effective_offset=ode.offset();
1421 
1422  if(ode.root_object().id()==ID_dereference)
1423  {
1424  exprt p_offset=pointer_offset(
1426  assert(p_offset.type()==effective_offset.type());
1427 
1428  effective_offset=plus_exprt(p_offset, effective_offset);
1429  }
1430 
1431  exprt zero=from_integer(0, ode.offset().type());
1432 
1433  // the final offset must not be negative
1434  binary_relation_exprt inequality(
1435  effective_offset, ID_ge, std::move(zero));
1436 
1438  inequality,
1439  name + " lower bound",
1440  "array bounds",
1441  expr.find_source_location(),
1442  expr,
1443  guard);
1444  }
1445  }
1446  }
1447 
1448  exprt type_matches_size=true_exprt();
1449 
1450  if(ode.root_object().id()==ID_dereference)
1451  {
1452  const exprt &pointer=
1454 
1455  const if_exprt size(
1456  dynamic_object(pointer),
1457  typecast_exprt(dynamic_size(ns), object_size(pointer).type()),
1458  object_size(pointer));
1459 
1460  const plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
1461 
1462  assert(effective_offset.op0().type()==effective_offset.op1().type());
1463 
1464  const auto size_casted =
1465  typecast_exprt::conditional_cast(size, effective_offset.type());
1466 
1467  binary_relation_exprt inequality(effective_offset, ID_lt, size_casted);
1468 
1469  exprt::operandst alloc_disjuncts;
1470  for(const auto &a : allocations)
1471  {
1472  typecast_exprt int_ptr{pointer, a.first.type()};
1473 
1474  binary_relation_exprt lower_bound_check{a.first, ID_le, int_ptr};
1475 
1476  plus_exprt upper_bound{
1477  int_ptr,
1478  typecast_exprt::conditional_cast(ode.offset(), int_ptr.type())};
1479 
1480  binary_relation_exprt upper_bound_check{
1481  std::move(upper_bound), ID_lt, plus_exprt{a.first, a.second}};
1482 
1483  alloc_disjuncts.push_back(
1484  and_exprt{std::move(lower_bound_check), std::move(upper_bound_check)});
1485  }
1486 
1487  exprt in_bounds_of_some_explicit_allocation = disjunction(alloc_disjuncts);
1488 
1489  or_exprt precond(
1490  std::move(in_bounds_of_some_explicit_allocation),
1491  and_exprt(dynamic_object(pointer), not_exprt(malloc_object(pointer, ns))),
1492  inequality);
1493 
1495  precond,
1496  name + " dynamic object upper bound",
1497  "array bounds",
1498  expr.find_source_location(),
1499  expr,
1500  guard);
1501 
1502  auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
1503 
1504  if(type_size_opt.has_value())
1505  {
1506  // Build a predicate that evaluates to true iff the size reported by
1507  // sizeof (i.e., compile-time size) matches the actual run-time size. The
1508  // run-time size for a dynamic (i.e., heap-allocated) object is determined
1509  // by the dynamic_size(ns) expression, which can only be used when
1510  // malloc_object(pointer, ns) evaluates to true for a given pointer.
1511  type_matches_size = if_exprt{
1512  dynamic_object(pointer),
1513  and_exprt{malloc_object(pointer, ns),
1515  dynamic_size(ns), type_size_opt->type()),
1516  *type_size_opt}},
1518  object_size(pointer), type_size_opt->type()),
1519  *type_size_opt}};
1520  }
1521  }
1522 
1523  const exprt &size=array_type.id()==ID_array ?
1524  to_array_type(array_type).size() :
1525  to_vector_type(array_type).size();
1526 
1527  if(size.is_nil())
1528  {
1529  // Linking didn't complete, we don't have a size.
1530  // Not clear what to do.
1531  }
1532  else if(size.id()==ID_infinity)
1533  {
1534  }
1535  else if(size.is_zero() &&
1536  expr.array().id()==ID_member)
1537  {
1538  // a variable sized struct member
1539  //
1540  // Excerpt from the C standard on flexible array members:
1541  // However, when a . (or ->) operator has a left operand that is (a pointer
1542  // to) a structure with a flexible array member and the right operand names
1543  // that member, it behaves as if that member were replaced with the longest
1544  // array (with the same element type) that would not make the structure
1545  // larger than the object being accessed; [...]
1546  const auto type_size_opt = size_of_expr(ode.root_object().type(), ns);
1547  CHECK_RETURN(type_size_opt.has_value());
1548 
1549  binary_relation_exprt inequality(
1551  ode.offset(), type_size_opt.value().type()),
1552  ID_lt,
1553  type_size_opt.value());
1554 
1556  implies_exprt(type_matches_size, inequality),
1557  name + " upper bound",
1558  "array bounds",
1559  expr.find_source_location(),
1560  expr,
1561  guard);
1562  }
1563  else
1564  {
1565  binary_relation_exprt inequality(index, ID_lt, size);
1566 
1567  // typecast size
1568  inequality.op1() = typecast_exprt::conditional_cast(
1569  inequality.op1(), inequality.op0().type());
1570 
1572  implies_exprt(type_matches_size, inequality),
1573  name + " upper bound",
1574  "array bounds",
1575  expr.find_source_location(),
1576  expr,
1577  guard);
1578  }
1579 }
1580 
1582  const exprt &asserted_expr,
1583  const std::string &comment,
1584  const std::string &property_class,
1585  const source_locationt &source_location,
1586  const exprt &src_expr,
1587  const guardt &guard)
1588 {
1589  // first try simplifier on it
1590  exprt simplified_expr =
1591  enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr;
1592 
1593  // throw away trivial properties?
1594  if(!retain_trivial && simplified_expr.is_true())
1595  return;
1596 
1597  // add the guard
1598  exprt guarded_expr =
1599  guard.is_true()
1600  ? std::move(simplified_expr)
1601  : implies_exprt{guard.as_expr(), std::move(simplified_expr)};
1602 
1603  if(assertions.insert(guarded_expr).second)
1604  {
1605  auto t = new_code.add(
1607  std::move(guarded_expr), source_location)
1609  std::move(guarded_expr), source_location));
1610 
1611  std::string source_expr_string;
1612  get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
1613 
1614  t->source_location.set_comment(comment + " in " + source_expr_string);
1615  t->source_location.set_property_class(property_class);
1616  }
1617 }
1618 
1620 {
1621  // we don't look into quantifiers
1622  if(expr.id() == ID_exists || expr.id() == ID_forall)
1623  return;
1624 
1625  if(expr.id() == ID_dereference)
1626  {
1627  check_rec(to_dereference_expr(expr).pointer(), guard);
1628  }
1629  else if(expr.id() == ID_index)
1630  {
1631  const index_exprt &index_expr = to_index_expr(expr);
1632  check_rec_address(index_expr.array(), guard);
1633  check_rec(index_expr.index(), guard);
1634  }
1635  else
1636  {
1637  for(const auto &operand : expr.operands())
1638  check_rec_address(operand, guard);
1639  }
1640 }
1641 
1643 {
1644  INVARIANT(
1645  expr.is_boolean(),
1646  "'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
1647 
1648  guardt old_guard = guard;
1649 
1650  for(const auto &op : expr.operands())
1651  {
1652  INVARIANT(
1653  op.is_boolean(),
1654  "'" + expr.id_string() + "' takes Boolean operands only, but got " +
1655  op.pretty());
1656 
1657  check_rec(op, guard);
1658  guard.add(expr.id() == ID_or ? boolean_negate(op) : op);
1659  }
1660 
1661  guard = std::move(old_guard);
1662 }
1663 
1664 void goto_checkt::check_rec_if(const if_exprt &if_expr, guardt &guard)
1665 {
1666  INVARIANT(
1667  if_expr.cond().is_boolean(),
1668  "first argument of if must be boolean, but got " + if_expr.cond().pretty());
1669 
1670  check_rec(if_expr.cond(), guard);
1671 
1672  {
1673  guardt old_guard = guard;
1674  guard.add(if_expr.cond());
1675  check_rec(if_expr.true_case(), guard);
1676  guard = std::move(old_guard);
1677  }
1678 
1679  {
1680  guardt old_guard = guard;
1681  guard.add(not_exprt{if_expr.cond()});
1682  check_rec(if_expr.false_case(), guard);
1683  guard = std::move(old_guard);
1684  }
1685 }
1686 
1688 {
1689  const dereference_exprt &deref = to_dereference_expr(member.struct_op());
1690 
1691  check_rec(deref.pointer(), guard);
1692 
1693  // avoid building the following expressions when pointer_validity_check
1694  // would return immediately anyway
1696  return true;
1697 
1698  // we rewrite s->member into *(s+member_offset)
1699  // to avoid requiring memory safety of the entire struct
1700  auto member_offset_opt = member_offset_expr(member, ns);
1701 
1702  if(member_offset_opt.has_value())
1703  {
1704  pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
1705  new_pointer_type.subtype() = member.type();
1706 
1707  const exprt char_pointer = typecast_exprt::conditional_cast(
1708  deref.pointer(), pointer_type(char_type()));
1709 
1710  const exprt new_address_casted = typecast_exprt::conditional_cast(
1711  plus_exprt{char_pointer,
1713  member_offset_opt.value(), pointer_diff_type())},
1714  new_pointer_type);
1715 
1716  dereference_exprt new_deref{new_address_casted};
1717  new_deref.add_source_location() = deref.source_location();
1718  pointer_validity_check(new_deref, member, guard);
1719 
1720  return true;
1721  }
1722  return false;
1723 }
1724 
1725 void goto_checkt::check_rec_div(const div_exprt &div_expr, guardt &guard)
1726 {
1727  div_by_zero_check(to_div_expr(div_expr), guard);
1728 
1729  if(div_expr.type().id() == ID_signedbv)
1730  integer_overflow_check(div_expr, guard);
1731  else if(div_expr.type().id() == ID_floatbv)
1732  {
1733  nan_check(div_expr, guard);
1734  float_overflow_check(div_expr, guard);
1735  }
1736 }
1737 
1739 {
1740  if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
1741  {
1742  integer_overflow_check(expr, guard);
1743  }
1744  else if(expr.type().id() == ID_floatbv)
1745  {
1746  nan_check(expr, guard);
1747  float_overflow_check(expr, guard);
1748  }
1749  else if(expr.type().id() == ID_pointer)
1750  {
1751  pointer_overflow_check(expr, guard);
1752  }
1753 }
1754 
1755 void goto_checkt::check_rec(const exprt &expr, guardt &guard)
1756 {
1757  // we don't look into quantifiers
1758  if(expr.id() == ID_exists || expr.id() == ID_forall)
1759  return;
1760 
1761  if(expr.id() == ID_address_of)
1762  {
1763  check_rec_address(to_address_of_expr(expr).object(), guard);
1764  return;
1765  }
1766  else if(expr.id() == ID_and || expr.id() == ID_or)
1767  {
1768  check_rec_logical_op(expr, guard);
1769  return;
1770  }
1771  else if(expr.id() == ID_if)
1772  {
1773  check_rec_if(to_if_expr(expr), guard);
1774  return;
1775  }
1776  else if(
1777  expr.id() == ID_member &&
1778  to_member_expr(expr).struct_op().id() == ID_dereference)
1779  {
1780  if(check_rec_member(to_member_expr(expr), guard))
1781  return;
1782  }
1783 
1784  forall_operands(it, expr)
1785  check_rec(*it, guard);
1786 
1787  if(expr.type().id() == ID_c_enum_tag)
1788  enum_range_check(expr, guard);
1789 
1790  if(expr.id()==ID_index)
1791  {
1792  bounds_check(to_index_expr(expr), guard);
1793  }
1794  else if(expr.id()==ID_div)
1795  {
1796  check_rec_div(to_div_expr(expr), guard);
1797  }
1798  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr)
1799  {
1800  undefined_shift_check(to_shift_expr(expr), guard);
1801 
1802  if(expr.id()==ID_shl && expr.type().id()==ID_signedbv)
1803  integer_overflow_check(expr, guard);
1804  }
1805  else if(expr.id()==ID_mod)
1806  {
1807  mod_by_zero_check(to_mod_expr(expr), guard);
1808  mod_overflow_check(to_mod_expr(expr), guard);
1809  }
1810  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
1811  expr.id()==ID_mult ||
1812  expr.id()==ID_unary_minus)
1813  {
1814  check_rec_arithmetic_op(expr, guard);
1815  }
1816  else if(expr.id()==ID_typecast)
1817  conversion_check(expr, guard);
1818  else if(expr.id()==ID_le || expr.id()==ID_lt ||
1819  expr.id()==ID_ge || expr.id()==ID_gt)
1821  else if(expr.id()==ID_dereference)
1822  {
1823  pointer_validity_check(to_dereference_expr(expr), expr, guard);
1824  }
1825  else if(is_pointer_primitive(expr))
1826  {
1827  pointer_primitive_check(expr, guard);
1828  }
1829 }
1830 
1831 void goto_checkt::check(const exprt &expr)
1832 {
1833  guardt guard{true_exprt{}, guard_manager};
1834  check_rec(expr, guard);
1835 }
1836 
1839 {
1840  bool modified = false;
1841 
1842  for(auto &op : expr.operands())
1843  {
1844  auto op_result = rw_ok_check(op);
1845  if(op_result.has_value())
1846  {
1847  op = *op_result;
1848  modified = true;
1849  }
1850  }
1851 
1852  if(expr.id() == ID_r_ok || expr.id() == ID_w_ok)
1853  {
1854  // these get an address as first argument and a size as second
1856  expr.operands().size() == 2, "r/w_ok must have two operands");
1857 
1858  const auto conditions =
1859  address_check(to_binary_expr(expr).op0(), to_binary_expr(expr).op1());
1860 
1861  exprt::operandst conjuncts;
1862 
1863  for(const auto &c : conditions)
1864  conjuncts.push_back(c.assertion);
1865 
1866  return conjunction(conjuncts);
1867  }
1868  else if(modified)
1869  return std::move(expr);
1870  else
1871  return {};
1872 }
1873 
1877 {
1878 public:
1880  void set_flag(bool &flag, bool new_value)
1881  {
1882  if(flag != new_value)
1883  {
1884  flags_to_reset.emplace_back(&flag, flag);
1885  flag = new_value;
1886  }
1887  }
1888 
1891  {
1892  for(const auto &flag_pair : flags_to_reset)
1893  *flag_pair.first = flag_pair.second;
1894  }
1895 
1896 private:
1897  std::list<std::pair<bool *, bool>> flags_to_reset;
1898 };
1899 
1901  const irep_idt &function_identifier,
1902  goto_functiont &goto_function)
1903 {
1904  assertions.clear();
1905 
1906  const auto &function_symbol = ns.lookup(function_identifier);
1907  mode = function_symbol.mode;
1908 
1909  bool did_something = false;
1910 
1912  util_make_unique<local_bitvector_analysist>(goto_function, ns);
1913 
1914  goto_programt &goto_program=goto_function.body;
1915 
1916  Forall_goto_program_instructions(it, goto_program)
1917  {
1918  current_target = it;
1920 
1921  flag_resett flag_resetter;
1922  const auto &pragmas = i.source_location.get_pragmas();
1923  for(const auto &d : pragmas)
1924  {
1925  if(d.first == "disable:bounds-check")
1926  flag_resetter.set_flag(enable_bounds_check, false);
1927  else if(d.first == "disable:pointer-check")
1928  flag_resetter.set_flag(enable_pointer_check, false);
1929  else if(d.first == "disable:memory-leak-check")
1930  flag_resetter.set_flag(enable_memory_leak_check, false);
1931  else if(d.first == "disable:div-by-zero-check")
1932  flag_resetter.set_flag(enable_div_by_zero_check, false);
1933  else if(d.first == "disable:enum-range-check")
1934  flag_resetter.set_flag(enable_enum_range_check, false);
1935  else if(d.first == "disable:signed-overflow-check")
1936  flag_resetter.set_flag(enable_signed_overflow_check, false);
1937  else if(d.first == "disable:unsigned-overflow-check")
1938  flag_resetter.set_flag(enable_unsigned_overflow_check, false);
1939  else if(d.first == "disable:pointer-overflow-check")
1940  flag_resetter.set_flag(enable_pointer_overflow_check, false);
1941  else if(d.first == "disable:float-overflow-check")
1942  flag_resetter.set_flag(enable_float_overflow_check, false);
1943  else if(d.first == "disable:conversion-check")
1944  flag_resetter.set_flag(enable_conversion_check, false);
1945  else if(d.first == "disable:undefined-shift-check")
1946  flag_resetter.set_flag(enable_undefined_shift_check, false);
1947  else if(d.first == "disable:nan-check")
1948  flag_resetter.set_flag(enable_nan_check, false);
1949  else if(d.first == "disable:pointer-primitive-check")
1950  flag_resetter.set_flag(enable_pointer_primitive_check, false);
1951  }
1952 
1953  new_code.clear();
1954 
1955  // we clear all recorded assertions if
1956  // 1) we want to generate all assertions or
1957  // 2) the instruction is a branch target
1958  if(retain_trivial ||
1959  i.is_target())
1960  assertions.clear();
1961 
1962  if(i.has_condition())
1963  {
1964  check(i.get_condition());
1965 
1966  if(has_subexpr(i.get_condition(), [](const exprt &expr) {
1967  return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1968  }))
1969  {
1970  auto rw_ok_cond = rw_ok_check(i.get_condition());
1971  if(rw_ok_cond.has_value())
1972  i.set_condition(*rw_ok_cond);
1973  }
1974  }
1975 
1976  // magic ERROR label?
1977  for(const auto &label : error_labels)
1978  {
1979  if(std::find(i.labels.begin(), i.labels.end(), label)!=i.labels.end())
1980  {
1981  auto t = new_code.add(
1985 
1986  t->source_location.set_property_class("error label");
1987  t->source_location.set_comment("error label "+label);
1988  t->source_location.set("user-provided", true);
1989  }
1990  }
1991 
1992  if(i.is_other())
1993  {
1994  const auto &code = i.get_other();
1995  const irep_idt &statement = code.get_statement();
1996 
1997  if(statement==ID_expression)
1998  {
1999  check(code);
2000  }
2001  else if(statement==ID_printf)
2002  {
2003  for(const auto &op : code.operands())
2004  check(op);
2005  }
2006  }
2007  else if(i.is_assign())
2008  {
2009  const code_assignt &code_assign=to_code_assign(i.code);
2010 
2011  // Reset the no_enum_check with the flag reset for exception
2012  // safety
2013  {
2014  flag_resett no_enum_check_flag_resetter;
2015  no_enum_check_flag_resetter.set_flag(no_enum_check, true);
2016  check(code_assign.lhs());
2017  }
2018  check(code_assign.rhs());
2019 
2020  // the LHS might invalidate any assertion
2021  invalidate(code_assign.lhs());
2022 
2023  if(has_subexpr(code_assign.rhs(), [](const exprt &expr) {
2024  return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
2025  }))
2026  {
2027  exprt &rhs = to_code_assign(i.code).rhs();
2028  auto rw_ok_cond = rw_ok_check(rhs);
2029  if(rw_ok_cond.has_value())
2030  rhs = *rw_ok_cond;
2031  }
2032  }
2033  else if(i.is_function_call())
2034  {
2035  const code_function_callt &code_function_call=
2037 
2038  // for Java, need to check whether 'this' is null
2039  // on non-static method invocations
2040  if(mode==ID_java &&
2042  !code_function_call.arguments().empty() &&
2043  code_function_call.function().type().id()==ID_code &&
2044  to_code_type(code_function_call.function().type()).has_this())
2045  {
2046  exprt pointer=code_function_call.arguments()[0];
2047 
2050 
2051  if(flags.is_unknown() || flags.is_null())
2052  {
2053  notequal_exprt not_eq_null(
2054  pointer,
2056 
2058  not_eq_null,
2059  "this is null on method invocation",
2060  "pointer dereference",
2061  i.source_location,
2062  pointer,
2064  }
2065  }
2066 
2067  for(const auto &op : code_function_call.operands())
2068  check(op);
2069 
2070  // the call might invalidate any assertion
2071  assertions.clear();
2072  }
2073  else if(i.is_return())
2074  {
2075  if(i.code.operands().size()==1)
2076  {
2077  const code_returnt &code_return = to_code_return(i.code);
2078  check(code_return.return_value());
2079  // the return value invalidate any assertion
2080  invalidate(code_return.return_value());
2081 
2082  if(has_subexpr(code_return.return_value(), [](const exprt &expr) {
2083  return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
2084  }))
2085  {
2086  exprt &return_value = to_code_return(i.code).return_value();
2087  auto rw_ok_cond = rw_ok_check(return_value);
2088  if(rw_ok_cond.has_value())
2089  return_value = *rw_ok_cond;
2090  }
2091  }
2092  }
2093  else if(i.is_throw())
2094  {
2095  if(i.code.get_statement()==ID_expression &&
2096  i.code.operands().size()==1 &&
2097  i.code.op0().operands().size()==1)
2098  {
2099  // must not throw NULL
2100 
2101  exprt pointer = to_unary_expr(i.code.op0()).op();
2102 
2103  const notequal_exprt not_eq_null(
2104  pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
2105 
2107  not_eq_null,
2108  "throwing null",
2109  "pointer dereference",
2110  i.source_location,
2111  pointer,
2113  }
2114 
2115  // this has no successor
2116  assertions.clear();
2117  }
2118  else if(i.is_assert())
2119  {
2120  bool is_user_provided=i.source_location.get_bool("user-provided");
2121 
2122  if((is_user_provided && !enable_assertions &&
2123  i.source_location.get_property_class()!="error label") ||
2124  (!is_user_provided && !enable_built_in_assertions))
2125  {
2126  i.turn_into_skip();
2127  did_something = true;
2128  }
2129  }
2130  else if(i.is_assume())
2131  {
2132  if(!enable_assumptions)
2133  {
2134  i.turn_into_skip();
2135  did_something = true;
2136  }
2137  }
2138  else if(i.is_dead())
2139  {
2141  {
2142  assert(i.code.operands().size()==1);
2143  const symbol_exprt &variable=to_symbol_expr(i.code.op0());
2144 
2145  // is it dirty?
2146  if(local_bitvector_analysis->dirty(variable))
2147  {
2148  // need to mark the dead variable as dead
2149  exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2150  exprt address_of_expr = typecast_exprt::conditional_cast(
2151  address_of_exprt(variable), lhs.type());
2152  if_exprt rhs(
2154  std::move(address_of_expr),
2155  lhs);
2158  std::move(lhs), std::move(rhs), i.source_location));
2159  t->code.add_source_location()=i.source_location;
2160  }
2161  }
2162  }
2163  else if(i.is_end_function())
2164  {
2165  if(
2166  function_identifier == goto_functionst::entry_point() &&
2168  {
2169  const symbolt &leak=ns.lookup(CPROVER_PREFIX "memory_leak");
2170  const symbol_exprt leak_expr=leak.symbol_expr();
2171 
2172  // add self-assignment to get helpful counterexample output
2173  new_code.add(goto_programt::make_assignment(leak_expr, leak_expr));
2174 
2175  source_locationt source_location;
2176  source_location.set_function(function_identifier);
2177 
2178  equal_exprt eq(
2179  leak_expr,
2182  eq,
2183  "dynamically allocated memory never freed",
2184  "memory-leak",
2185  source_location,
2186  eq,
2188  }
2189  }
2190 
2192  {
2193  if(i_it->source_location.is_nil())
2194  {
2195  i_it->source_location.id(irep_idt());
2196 
2197  if(!it->source_location.get_file().empty())
2198  i_it->source_location.set_file(it->source_location.get_file());
2199 
2200  if(!it->source_location.get_line().empty())
2201  i_it->source_location.set_line(it->source_location.get_line());
2202 
2203  if(!it->source_location.get_function().empty())
2204  i_it->source_location.set_function(
2205  it->source_location.get_function());
2206 
2207  if(!it->source_location.get_column().empty())
2208  i_it->source_location.set_column(it->source_location.get_column());
2209 
2210  if(!it->source_location.get_java_bytecode_index().empty())
2211  i_it->source_location.set_java_bytecode_index(
2212  it->source_location.get_java_bytecode_index());
2213  }
2214  }
2215 
2216  // insert new instructions -- make sure targets are not moved
2217  did_something |= !new_code.instructions.empty();
2218 
2219  while(!new_code.instructions.empty())
2220  {
2221  goto_program.insert_before_swap(it, new_code.instructions.front());
2222  new_code.instructions.pop_front();
2223  it++;
2224  }
2225  }
2226 
2227  if(did_something)
2228  remove_skip(goto_program);
2229 }
2230 
2232  const irep_idt &function_identifier,
2233  goto_functionst::goto_functiont &goto_function,
2234  const namespacet &ns,
2235  const optionst &options)
2236 {
2237  goto_checkt goto_check(ns, options);
2238  goto_check.goto_check(function_identifier, goto_function);
2239 }
2240 
2242  const namespacet &ns,
2243  const optionst &options,
2244  goto_functionst &goto_functions)
2245 {
2246  goto_checkt goto_check(ns, options);
2247 
2248  goto_check.collect_allocations(goto_functions);
2249 
2250  Forall_goto_functions(it, goto_functions)
2251  {
2252  goto_check.goto_check(it->first, it->second);
2253  }
2254 }
2255 
2257  const optionst &options,
2258  goto_modelt &goto_model)
2259 {
2260  const namespacet ns(goto_model.symbol_table);
2261  goto_check(ns, options, goto_model.goto_functions);
2262 }
goto_checkt::allocationt
std::pair< exprt, exprt > allocationt
Definition: goto_check.cpp:265
goto_checkt::allocationst
std::list< allocationt > allocationst
Definition: goto_check.cpp:266
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
guard_exprt
Definition: guard_expr.h:27
goto_checkt::array_name
std::string array_name(const exprt &)
Definition: goto_check.cpp:1375
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:721
goto_functiont::body
goto_programt body
Definition: goto_function.h:30
array_name
std::string array_name(const namespacet &ns, const exprt &expr)
Definition: array_name.cpp:20
ieee_floatt
Definition: ieee_float.h:120
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
goto_programt::instructiont::is_throw
bool is_throw() const
Definition: goto_program.h:462
goto_checkt::current_target
goto_programt::const_targett current_target
Definition: goto_check.cpp:96
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:791
source_locationt::get_property_class
const irep_idt & get_property_class() const
Definition: source_location.h:66
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:269
typet::subtype
const typet & subtype() const
Definition: type.h:47
c_enum_typet
The type of C enums.
Definition: std_types.h:620
has_subexpr
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:139
conjunction
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:51
goto_checkt::bounds_check
void bounds_check(const index_exprt &, const guardt &)
Definition: goto_check.cpp:1380
goto_checkt::conditiont::assertion
exprt assertion
Definition: goto_check.cpp:166
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1080
goto_checkt::enable_div_by_zero_check
bool enable_div_by_zero_check
Definition: goto_check.cpp:243
local_bitvector_analysis.h
Field-insensitive, location-sensitive bitvector analysis.
arith_tools.h
codet::op0
exprt & op0()
Definition: expr.h:102
goto_checkt::enable_undefined_shift_check
bool enable_undefined_shift_check
Definition: goto_check.cpp:249
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
Definition: std_expr.cpp:141
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:126
goto_checkt::guard_manager
guard_managert guard_manager
Definition: goto_check.cpp:97
null_pointer
exprt null_pointer(const exprt &pointer)
Definition: pointer_predicates.cpp:136
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:466
goto_checkt::enable_assumptions
bool enable_assumptions
Definition: goto_check.cpp:257
optionst
Definition: options.h:23
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
goto_checkt::enable_simplify
bool enable_simplify
Definition: goto_check.cpp:251
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:681
typet
The type of an expression, extends irept.
Definition: type.h:29
source_locationt::get_pragmas
const irept::named_subt & get_pragmas() const
Definition: source_location.h:200
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
goto_checkt::enable_nan_check
bool enable_nan_check
Definition: goto_check.cpp:252
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
local_bitvector_analysist::flagst::is_dynamic_heap
bool is_dynamic_heap() const
Definition: local_bitvector_analysis.h:131
goto_checkt::new_code
goto_programt new_code
Definition: goto_check.cpp:230
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
goto_checkt::enable_built_in_assertions
bool enable_built_in_assertions
Definition: goto_check.cpp:256
c_enum_typet::memberst
std::vector< c_enum_membert > memberst
Definition: std_types.h:644
goto_checkt::check_rec_address
void check_rec_address(const exprt &expr, guardt &guard)
Check an address-of expression: if it is a dereference then check the pointer if it is an index then ...
Definition: goto_check.cpp:1619
pointer_predicates.h
Various predicates over pointers in programs.
goto_programt::instructiont::is_dead
bool is_dead() const
Definition: goto_program.h:468
goto_checkt::enable_assert_to_assume
bool enable_assert_to_assume
Definition: goto_check.cpp:254
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1832
goto_checkt::retain_trivial
bool retain_trivial
Definition: goto_check.cpp:253
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
invariant.h
and_exprt
Boolean AND.
Definition: std_expr.h:2137
goto_checkt::enable_pointer_primitive_check
bool enable_pointer_primitive_check
Definition: goto_check.cpp:258
goto_checkt::allocations
allocationst allocations
Definition: goto_check.cpp:267
flag_resett::~flag_resett
~flag_resett()
Restore the values of all flags that have been modified via set_flag.
Definition: goto_check.cpp:1890
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
flag_resett
Set a Boolean flag to a new value (via set_flag) and restore the previous value when the entire objec...
Definition: goto_check.cpp:1877
goto_checkt::pointer_validity_check
void pointer_validity_check(const dereference_exprt &expr, const exprt &src_expr, const guardt &guard)
Generates VCCs for the validity of the given dereferencing operation.
Definition: goto_check.cpp:1157
exprt
Base class for all expressions.
Definition: expr.h:53
goto_checkt::enable_conversion_check
bool enable_conversion_check
Definition: goto_check.cpp:248
goto_checkt::check_rec_div
void check_rec_div(const div_exprt &div_expr, guardt &guard)
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numb...
Definition: goto_check.cpp:1725
goto_modelt
Definition: goto_model.h:26
guard_exprt::is_true
bool is_true() const
Definition: guard_expr.h:63
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:631
mode.h
options.h
Options.
goto_check
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
Definition: goto_check.cpp:2231
irep_idt
dstringt irep_idt
Definition: irep.h:32
goto_checkt::no_enum_check
bool no_enum_check
Definition: goto_check.cpp:98
bool_typet
The Boolean type.
Definition: std_types.h:37
goto_checkt::conditionst
std::list< conditiont > conditionst
Definition: goto_check.cpp:170
optionst::value_listt
std::list< std::string > value_listt
Definition: options.h:25
dynamic_object
exprt dynamic_object(const exprt &pointer)
Definition: pointer_predicates.cpp:71
guardt
guard_exprt guardt
Definition: guard.h:27
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
configt::ansi_c
struct configt::ansi_ct ansi_c
make_binary
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:36
goto_checkt::pointer_rel_check
void pointer_rel_check(const binary_relation_exprt &, const guardt &)
Definition: goto_check.cpp:1104
div_exprt
Division.
Definition: std_expr.h:1031
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
shift_exprt::op
exprt & op()
Definition: std_expr.h:2505
equal_exprt
Equality.
Definition: std_expr.h:1190
goto_checkt::nan_check
void nan_check(const exprt &, const guardt &)
Definition: goto_check.cpp:993
goto_checkt::enable_memory_leak_check
bool enable_memory_leak_check
Definition: goto_check.cpp:242
goto_checkt::enum_range_check
void enum_range_check(const exprt &, const guardt &)
Definition: goto_check.cpp:351
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:965
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
goto_checkt::pointer_primitive_check
void pointer_primitive_check(const exprt &expr, const guardt &guard)
Generates VCCs to check that pointers passed to pointer primitives are either null or valid.
Definition: goto_check.cpp:1198
notequal_exprt
Disequality.
Definition: std_expr.h:1248
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:255
ieee_float_spect
Definition: ieee_float.h:26
goto_checkt::enable_unsigned_overflow_check
bool enable_unsigned_overflow_check
Definition: goto_check.cpp:246
goto_checkt::enable_float_overflow_check
bool enable_float_overflow_check
Definition: goto_check.cpp:250
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
goto_checkt::mod_by_zero_check
void mod_by_zero_check(const mod_exprt &, const guardt &)
Definition: goto_check.cpp:447
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2543
array_typet::size
const exprt & size() const
Definition: std_types.h:973
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
guard.h
Guard Data Structure.
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
goto_checkt::pointer_overflow_check
void pointer_overflow_check(const exprt &, const guardt &)
Definition: goto_check.cpp:1131
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
goto_checkt::check_rec_logical_op
void check_rec_logical_op(const exprt &expr, guardt &guard)
Check a logical operation: check each operand in separation while extending the guarding condition as...
Definition: goto_check.cpp:1642
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:29
goto_programt::instructiont::turn_into_skip
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:351
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
make_unique.h
find_symbols.h
goto_checkt::check
void check(const exprt &expr)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
Definition: goto_check.cpp:1831
or_exprt
Boolean OR.
Definition: std_expr.h:2245
goto_checkt::check_rec
void check_rec(const exprt &expr, guardt &guard)
Recursively descend into expr and run the appropriate check for each sub-expression,...
Definition: goto_check.cpp:1755
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1125
goto_checkt::address_check
conditionst address_check(const exprt &address, const exprt &size)
Definition: goto_check.cpp:1257
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1248
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1011
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_checkt::float_overflow_check
void float_overflow_check(const exprt &, const guardt &)
Definition: goto_check.cpp:883
goto_checkt::conditiont
Definition: goto_check.cpp:160
goto_checkt::enable_pointer_check
bool enable_pointer_check
Definition: goto_check.cpp:241
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
guard_exprt::add
void add(const exprt &expr)
Definition: guard_expr.cpp:40
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:817
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:231
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
goto_checkt::ns
const namespacet & ns
Definition: goto_check.cpp:94
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:2901
boolean_negate
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
object_upper_bound
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
Definition: pointer_predicates.cpp:178
std_types.h
Pre-defined types.
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
local_bitvector_analysist::flagst::is_integer_address
bool is_integer_address() const
Definition: local_bitvector_analysis.h:161
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:920
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
goto_programt::instructiont::labels
labelst labels
Definition: goto_program.h:331
deallocated
exprt deallocated(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:50
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
dead_object
exprt dead_object(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:58
goto_checkt::enable_enum_range_check
bool enable_enum_range_check
Definition: goto_check.cpp:244
goto_checkt::assertionst
std::set< exprt > assertionst
Definition: goto_check.cpp:231
language.h
Abstract interface to support a programming language.
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
integer_address
exprt integer_address(const exprt &pointer)
Definition: pointer_predicates.cpp:129
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
goto_programt::instructiont::has_condition
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:279
goto_checkt::local_bitvector_analysis
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
Definition: goto_check.cpp:95
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:408
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
local_bitvector_analysist::flagst::is_null
bool is_null() const
Definition: local_bitvector_analysis.h:141
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
goto_checkt::enable_assertions
bool enable_assertions
Definition: goto_check.cpp:255
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:32
local_bitvector_analysist::flagst::is_static_lifetime
bool is_static_lifetime() const
Definition: local_bitvector_analysis.h:151
irept::is_nil
bool is_nil() const
Definition: irep.h:398
goto_checkt::check_rec_member
bool check_rec_member(const member_exprt &member, guardt &guard)
Check that a member expression is valid:
Definition: goto_check.cpp:1687
irept::id
const irep_idt & id() const
Definition: irep.h:418
goto_programt::instructiont::is_end_function
bool is_end_function() const
Definition: goto_program.h:475
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1192
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1359
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
goto_check.h
Program Transformation.
goto_checkt::rw_ok_check
optionalt< exprt > rw_ok_check(exprt)
expand the r_ok and w_ok predicates
Definition: goto_check.cpp:1838
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
goto_checkt::collect_allocations
void collect_allocations(const goto_functionst &goto_functions)
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
Definition: goto_check.cpp:272
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
cprover_prefix.h
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:218
local_bitvector_analysist::flagst::is_dynamic_local
bool is_dynamic_local() const
Definition: local_bitvector_analysis.h:121
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:511
goto_checkt::undefined_shift_check
void undefined_shift_check(const shift_exprt &, const guardt &)
Definition: goto_check.cpp:380
object_lower_bound
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Definition: pointer_predicates.cpp:208
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:268
goto_checkt::div_by_zero_check
void div_by_zero_check(const div_exprt &, const guardt &)
Definition: goto_check.cpp:330
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:37
goto_checkt::goto_functiont
goto_functionst::goto_functiont goto_functiont
Definition: goto_check.cpp:80
null_object
exprt null_object(const exprt &pointer)
Definition: pointer_predicates.cpp:123
goto_checkt::error_labels
error_labelst error_labels
Definition: goto_check.cpp:261
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
code_typet::has_this
bool has_this() const
Definition: std_types.h:818
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:783
ieee_floatt::plus_infinity
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:200
flag_resett::set_flag
void set_flag(bool &flag, bool new_value)
Store the current value of flag and then set its value to new_value.
Definition: goto_check.cpp:1880
config
configt config
Definition: config.cpp:24
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
source_locationt
Definition: source_location.h:20
configt::ansi_ct::c_standardt::C99
@ C99
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_checkt
Definition: goto_check.cpp:43
malloc_object
exprt malloc_object(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:42
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
has_symbol
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
Definition: find_symbols.cpp:37
goto_checkt::enable_bounds_check
bool enable_bounds_check
Definition: goto_check.cpp:240
local_bitvector_analysist::flagst::is_unknown
bool is_unknown() const
Definition: local_bitvector_analysis.h:91
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
expr_util.h
Deprecated expression utility functions.
configt::ansi_ct::c_standardt::C11
@ C11
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
shift_exprt
A base class for shift operators.
Definition: std_expr.h:2496
goto_programt::instructiont::is_assert
bool is_assert() const
Definition: goto_program.h:470
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:696
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:22
goto_checkt::goto_check
void goto_check(const irep_idt &function_identifier, goto_functiont &goto_function)
Definition: goto_check.cpp:1900
goto_checkt::mod_overflow_check
void mod_overflow_check(const mod_exprt &, const guardt &)
check a mod expression for the case INT_MIN % -1
Definition: goto_check.cpp:469
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
shift_exprt::distance
exprt & distance()
Definition: std_expr.h:2515
local_bitvector_analysist::flagst
Definition: local_bitvector_analysis.h:50
isinf_exprt
Evaluates to true if the operand is infinite.
Definition: std_expr.h:3554
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
goto_checkt::invalidate
void invalidate(const exprt &lhs)
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.
Definition: goto_check.cpp:304
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
configt::ansi_ct::c_standard
enum configt::ansi_ct::c_standardt c_standard
ieee_float.h
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
goto_checkt::enable_signed_overflow_check
bool enable_signed_overflow_check
Definition: goto_check.cpp:245
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1298
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
goto_checkt::add_guarded_property
void add_guarded_property(const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr, const guardt &guard)
Include the asserted_expr in the code conditioned by the guard.
Definition: goto_check.cpp:1581
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:460
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_checkt::integer_overflow_check
void integer_overflow_check(const exprt &, const guardt &)
Definition: goto_check.cpp:665
local_bitvector_analysist::flagst::is_uninitialized
bool is_uninitialized() const
Definition: local_bitvector_analysis.h:101
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
same_object
exprt same_object(const exprt &p1, const exprt &p2)
Definition: pointer_predicates.cpp:27
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
goto_checkt::conditiont::description
std::string description
Definition: goto_check.cpp:167
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
configt::cppt::cpp_standardt::CPP14
@ CPP14
config.h
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1775
goto_programt::instructiont::set_condition
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:292
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
goto_checkt::error_labelst
optionst::value_listt error_labelst
Definition: goto_check.cpp:260
configt::cppt::cpp_standardt::CPP11
@ CPP11
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2697
exprt::operands
operandst & operands()
Definition: expr.h:95
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
index_exprt
Array index operator.
Definition: std_expr.h:1293
is_invalid_pointer_exprt
Definition: pointer_predicates.h:48
goto_programt::instructiont::is_assume
bool is_assume() const
Definition: goto_program.h:469
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
goto_checkt::mode
irep_idt mode
Definition: goto_check.cpp:269
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
configt::cpp
struct configt::cppt cpp
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
pointer_diff_type
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:228
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
remove_skip.h
Program Transformation.
goto_checkt::enable_pointer_overflow_check
bool enable_pointer_overflow_check
Definition: goto_check.cpp:247
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1320
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
goto_checkt::check_rec_if
void check_rec_if(const if_exprt &if_expr, guardt &guard)
Check an if expression: check the if-condition alone, and then check the true/false-cases with the gu...
Definition: goto_check.cpp:1664
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:285
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
ieee_float_equal_exprt
IEEE-floating-point equality.
Definition: std_expr.h:3689
goto_checkt::assertions
assertionst assertions
Definition: goto_check.cpp:232
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:461
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:119
source_locationt::is_built_in
static bool is_built_in(const std::string &s)
Definition: source_location.cpp:16
goto_checkt::is_pointer_primitive
bool is_pointer_primitive(const exprt &expr)
Returns true if the given expression is a pointer primitive such as __CPROVER_r_ok()
Definition: goto_check.cpp:1246
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:226
array_name.h
Misc Utilities.
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:866
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
std_expr.h
API to expression classes.
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:774
goto_programt::instructiont::is_target
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:337
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_checkt::conditiont::conditiont
conditiont(const exprt &_assertion, const std::string &_description)
Definition: goto_check.cpp:161
dynamic_size
exprt dynamic_size(const namespacet &ns)
Definition: pointer_predicates.cpp:66
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
c_types.h
goto_checkt::check_rec_arithmetic_op
void check_rec_arithmetic_op(const exprt &expr, guardt &guard)
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers),...
Definition: goto_check.cpp:1738
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
to_shl_expr
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: std_expr.h:2580
ieee_floatt::minus_infinity
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:203
goto_checkt::goto_checkt
goto_checkt(const namespacet &_ns, const optionst &_options)
Definition: goto_check.cpp:45
goto_checkt::conversion_check
void conversion_check(const exprt &, const guardt &)
Definition: goto_check.cpp:499
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
validation_modet::INVARIANT
@ INVARIANT
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
mod_exprt
Modulo.
Definition: std_expr.h:1100
c_enum_typet::members
const memberst & members() const
Definition: std_types.h:646
flag_resett::flags_to_reset
std::list< std::pair< bool *, bool > > flags_to_reset
Definition: goto_check.cpp:1897
goto_programt::instructiont::is_return
bool is_return() const
Definition: goto_program.h:459
shl_exprt
Left shift.
Definition: std_expr.h:2561
configt::cppt::cpp_standard
enum configt::cppt::cpp_standardt cpp_standard
not_exprt
Boolean negation.
Definition: std_expr.h:2843
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:1870