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