cprover
code_contracts.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Verify and use annotated invariants and pre/post-conditions
4 
5 Author: Michael Tautschnig
6 
7 Date: February 2016
8 
9 \*******************************************************************/
10 
13 
14 #include "code_contracts.h"
15 
16 #include <algorithm>
17 
19 
22 
24 
25 #include <util/arith_tools.h>
26 #include <util/c_types.h>
27 #include <util/expr_util.h>
28 #include <util/format_type.h>
29 #include <util/fresh_symbol.h>
30 #include <util/mathematical_expr.h>
32 #include <util/message.h>
35 #include <util/replace_symbol.h>
36 
37 #include "loop_utils.h"
38 
43 {
44 public:
46  {
47  }
48 
49  // \brief Has this object been passed to exprt::visit() on an exprt whose
50  // descendants contain __CPROVER_return_value?
52  {
53  return found;
54  }
55 
56  void operator()(const exprt &exp) override
57  {
58  if(exp.id() != ID_symbol)
59  return;
60  const symbol_exprt &sym = to_symbol_expr(exp);
61  found |= sym.get_identifier() == CPROVER_PREFIX "return_value";
62  }
63 
64 protected:
65  bool found;
66 };
67 
68 exprt get_size(const typet &type, const namespacet &ns, messaget &log)
69 {
70  auto size_of_opt = size_of_expr(type, ns);
71  CHECK_RETURN(size_of_opt.has_value());
72  exprt result = size_of_opt.value();
73  result.add(ID_C_c_sizeof_type) = type;
74  return result;
75 }
76 
78  goto_functionst::goto_functiont &goto_function,
79  const local_may_aliast &local_may_alias,
80  const goto_programt::targett loop_head,
81  const loopt &loop)
82 {
83  PRECONDITION(!loop.empty());
84 
85  // find the last back edge
86  goto_programt::targett loop_end = loop_head;
87  for(const auto &t : loop)
88  if(
89  t->is_goto() && t->get_target() == loop_head &&
90  t->location_number > loop_end->location_number)
91  loop_end = t;
92 
93  // see whether we have an invariant
94  exprt invariant = static_cast<const exprt &>(
95  loop_end->get_condition().find(ID_C_spec_loop_invariant));
96  if(invariant.is_nil())
97  return;
98 
99  // change H: loop; E: ...
100  // to
101  // H: assert(invariant);
102  // havoc;
103  // assume(invariant);
104  // if(guard) goto E:
105  // loop;
106  // assert(invariant);
107  // assume(false);
108  // E: ...
109 
110  // find out what can get changed in the loop
111  modifiest modifies;
112  get_modifies(local_may_alias, loop, modifies);
113 
114  // build the havocking code
115  goto_programt havoc_code;
116 
117  // assert the invariant
118  {
119  goto_programt::targett a = havoc_code.add(
120  goto_programt::make_assertion(invariant, loop_head->source_location));
121  a->source_location.set_comment("Check loop invariant before entry");
122  }
123 
124  // havoc variables being written to
125  build_havoc_code(loop_head, modifies, havoc_code);
126 
127  // assume the invariant
128  havoc_code.add(
129  goto_programt::make_assumption(invariant, loop_head->source_location));
130 
131  // non-deterministically skip the loop if it is a do-while loop
132  if(!loop_head->is_goto())
133  {
134  havoc_code.add(goto_programt::make_goto(
135  loop_end,
137  }
138 
139  // Now havoc at the loop head.
140  // Use insert_before_swap to preserve jumps to loop head.
141  goto_function.body.insert_before_swap(loop_head, havoc_code);
142 
143  // assert the invariant at the end of the loop body
144  {
146  goto_programt::make_assertion(invariant, loop_end->source_location);
147  a.source_location.set_comment("Check that loop invariant is preserved");
148  goto_function.body.insert_before_swap(loop_end, a);
149  ++loop_end;
150  }
151 
152  // change the back edge into assume(false) or assume(guard)
153  loop_end->targets.clear();
154  loop_end->type=ASSUME;
155  if(loop_head->is_goto())
156  loop_end->set_condition(false_exprt());
157  else
158  loop_end->set_condition(boolean_negate(loop_end->get_condition()));
159 }
160 
162  const codet &code,
163  const irep_idt &mode,
164  goto_programt &program)
165 {
167  converter.goto_convert(code, program, mode);
168 }
169 
171 {
172  const symbolt &function_symbol = ns.lookup(fun_name);
173  const auto &type = to_code_with_contract_type(function_symbol.type);
174  return type.has_contract();
175 }
176 
178  exprt expression,
180  irep_idt mode)
181 {
182  if(expression.id() == ID_not || expression.id() == ID_typecast)
183  {
184  // For unary connectives, recursively check for
185  // nested quantified formulae in the term
186  const auto &unary_expression = to_unary_expr(expression);
187  add_quantified_variable(unary_expression.op(), replace, mode);
188  }
189  if(expression.id() == ID_notequal || expression.id() == ID_implies)
190  {
191  // For binary connectives, recursively check for
192  // nested quantified formulae in the left and right terms
193  const auto &binary_expression = to_binary_expr(expression);
194  add_quantified_variable(binary_expression.lhs(), replace, mode);
195  add_quantified_variable(binary_expression.rhs(), replace, mode);
196  }
197  if(expression.id() == ID_if)
198  {
199  // For ternary connectives, recursively check for
200  // nested quantified formulae in all three terms
201  const auto &if_expression = to_if_expr(expression);
202  add_quantified_variable(if_expression.cond(), replace, mode);
203  add_quantified_variable(if_expression.true_case(), replace, mode);
204  add_quantified_variable(if_expression.false_case(), replace, mode);
205  }
206  if(expression.id() == ID_and || expression.id() == ID_or)
207  {
208  // For multi-ary connectives, recursively check for
209  // nested quantified formulae in all terms
210  const auto &multi_ary_expression = to_multi_ary_expr(expression);
211  for(const auto &operand : multi_ary_expression.operands())
212  {
213  add_quantified_variable(operand, replace, mode);
214  }
215  }
216  else if(expression.id() == ID_exists || expression.id() == ID_forall)
217  {
218  // When a quantifier expression is found,
219  // 1. get quantified variables
220  const auto &quantifier_expression = to_quantifier_expr(expression);
221  const auto &quantified_variables = quantifier_expression.variables();
222  for(const auto &quantified_variable : quantified_variables)
223  {
224  // for each quantified variable...
225  const auto &quantified_symbol = to_symbol_expr(quantified_variable);
226 
227  // 1.1 create fresh symbol
228  symbolt new_symbol = get_fresh_aux_symbol(
229  quantified_symbol.type(),
230  id2string(quantified_symbol.get_identifier()),
231  "tmp",
232  quantified_symbol.source_location(),
233  mode,
234  symbol_table);
235 
236  // 1.2 add created fresh symbol to expression map
237  symbol_exprt q(
238  quantified_symbol.get_identifier(), quantified_symbol.type());
239  replace.insert(q, new_symbol.symbol_expr());
240 
241  // 1.3 recursively check for nested quantified formulae
242  add_quantified_variable(quantifier_expression.where(), replace, mode);
243  }
244  }
245 }
246 
248  const irep_idt &function_id,
249  goto_programt &goto_program,
250  goto_programt::targett target)
251 {
252  const code_function_callt &call = target->get_function_call();
253 
254  // Return if the function is not named in the call; currently we don't handle
255  // function pointers.
256  PRECONDITION(call.function().id() == ID_symbol);
257 
258  // Retrieve the function type, which is needed to extract the contract
259  // components.
260  const irep_idt &function = to_symbol_expr(call.function()).get_identifier();
261  const symbolt &function_symbol = ns.lookup(function);
262  const auto &type = to_code_with_contract_type(function_symbol.type);
263 
264  // Isolate each component of the contract.
265  exprt assigns = type.assigns();
266  exprt requires = type.requires();
267  exprt ensures = type.ensures();
268 
269  // Check to see if the function contract actually constrains its effect on
270  // the program state; if not, return.
271  if(ensures.is_nil() && assigns.is_nil())
272  return false;
273 
274  // Create a replace_symbolt object, for replacing expressions in the callee
275  // with expressions from the call site (e.g. the return value).
277  if(type.return_type() != empty_typet())
278  {
279  // Check whether the function's return value is not disregarded.
280  if(call.lhs().is_not_nil())
281  {
282  // If so, have it replaced appropriately.
283  // For example, if foo() ensures that its return value is > 5, then
284  // rewrite calls to foo as follows:
285  // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
286  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
287  replace.insert(ret_val, call.lhs());
288  }
289  else
290  {
291  // If the function does return a value, but the return value is
292  // disregarded, check if the postcondition includes the return value.
294  ensures.visit(v);
295  if(v.found_return_value())
296  {
297  // The postcondition does mention __CPROVER_return_value, so mint a
298  // fresh variable to replace __CPROVER_return_value with.
299  const symbolt &fresh = get_fresh_aux_symbol(
300  type.return_type(),
301  id2string(function),
302  "ignored_return_value",
303  call.source_location(),
304  symbol_table.lookup_ref(function).mode,
305  ns,
306  symbol_table);
307  symbol_exprt ret_val(CPROVER_PREFIX "return_value", type.return_type());
308  replace.insert(ret_val, fresh.symbol_expr());
309  }
310  }
311  }
312 
313  // Replace formal parameters
314  code_function_callt::argumentst::const_iterator a_it=
315  call.arguments().begin();
316  for(code_typet::parameterst::const_iterator p_it = type.parameters().begin();
317  p_it != type.parameters().end() && a_it != call.arguments().end();
318  ++p_it, ++a_it)
319  {
320  if(!p_it->get_identifier().empty())
321  {
322  symbol_exprt p(p_it->get_identifier(), p_it->type());
323  replace.insert(p, *a_it);
324  }
325  }
326 
327  // Add quantified variables in contracts to the symbol map
328  irep_idt mode = symbol_table.lookup_ref(function).mode;
331 
332  // Replace expressions in the contract components.
333  replace(assigns);
334  replace(requires);
335  replace(ensures);
336 
337  // Insert assertion of the precondition immediately before the call site.
338  if(requires.is_not_nil())
339  {
340  goto_programt assertion;
342  code_assertt(requires),
343  symbol_table.lookup_ref(function).mode,
344  assertion);
345  auto lines_to_iterate = assertion.instructions.size();
346  goto_program.insert_before_swap(target, assertion);
347  std::advance(target, lines_to_iterate);
348  }
349 
350  // Create a series of non-deterministic assignments to havoc the variables
351  // in the assigns clause.
352  if(assigns.is_not_nil())
353  {
354  assigns_clauset assigns_cause(assigns, *this, function_id, log);
355  goto_programt assigns_havoc = assigns_cause.havoc_code(
356  function_symbol.location, function_id, function_symbol.mode);
357 
358  // Insert the non-deterministic assignment immediately before the call site.
359  std::size_t lines_to_iterate = assigns_havoc.instructions.size();
360  goto_program.insert_before_swap(target, assigns_havoc);
361  std::advance(target, lines_to_iterate);
362  }
363 
364  // To remove the function call, replace it with an assumption statement
365  // assuming the postcondition, if there is one. Otherwise, replace the
366  // function call with a SKIP statement.
367  if(ensures.is_not_nil())
368  {
369  goto_programt assumption;
371  code_assumet(ensures),
372  symbol_table.lookup_ref(function).mode,
373  assumption);
374  auto lines_to_iterate = assumption.instructions.size();
375  goto_program.insert_before_swap(target, assumption);
376  std::advance(target, lines_to_iterate);
377  }
378  *target = goto_programt::make_skip();
379 
380  // Add this function to the set of replaced functions.
381  summarized.insert(function);
382  return false;
383 }
384 
386  goto_functionst::goto_functiont &goto_function)
387 {
388  local_may_aliast local_may_alias(goto_function);
389  natural_loops_mutablet natural_loops(goto_function.body);
390 
391  // iterate over the (natural) loops in the function
392  for(const auto &loop : natural_loops.loop_map)
394  goto_function, local_may_alias, loop.first, loop.second);
395 }
396 
398  const typet &type,
399  const source_locationt &source_location,
400  const irep_idt &function_id,
401  const irep_idt &mode)
402 {
403  return get_fresh_aux_symbol(
404  type,
405  id2string(function_id) + "::tmp_cc",
406  "tmp_cc",
407  source_location,
408  mode,
409  symbol_table);
410 }
411 
413  const exprt &lhs,
414  std::vector<exprt> &aliasable_references)
415 {
416  exprt::operandst operands;
417  operands.reserve(aliasable_references.size());
418  for(auto aliasable : aliasable_references)
419  {
420  operands.push_back(equal_exprt(lhs, typecast_exprt(aliasable, lhs.type())));
421  }
422  return disjunction(operands);
423 }
424 
426  goto_programt::instructionst::iterator &instruction_iterator,
427  goto_programt &program,
428  exprt &assigns,
429  std::set<irep_idt> &freely_assignable_symbols,
430  assigns_clauset &assigns_clause)
431 {
432  INVARIANT(
433  instruction_iterator->is_assign(),
434  "The first instruction of instrument_assign_statement should always be"
435  " an assignment");
436 
437  const exprt &lhs = instruction_iterator->get_assign().lhs();
438 
439  goto_programt alias_assertion;
440  alias_assertion.add(goto_programt::make_assertion(
441  assigns_clause.alias_expression(lhs),
442  instruction_iterator->source_location));
443 
444  int lines_to_iterate = alias_assertion.instructions.size();
445  program.insert_before_swap(instruction_iterator, alias_assertion);
446  std::advance(instruction_iterator, lines_to_iterate);
447 }
448 
450  goto_programt::instructionst::iterator &instruction_iterator,
451  goto_programt &program,
452  exprt &assigns,
453  const irep_idt &function_id,
454  std::set<irep_idt> &freely_assignable_symbols,
455  assigns_clauset &assigns_clause)
456 {
457  INVARIANT(
458  instruction_iterator->is_function_call(),
459  "The first argument of instrument_call_statement should always be "
460  "a function call");
461 
462  code_function_callt call = instruction_iterator->get_function_call();
463  const irep_idt &called_name =
465 
466  if(called_name == "malloc")
467  {
468  goto_programt::instructionst::iterator local_instruction_iterator =
469  instruction_iterator;
470  // malloc statments return a void pointer, which is then cast and assigned
471  // to a result variable. We iterate one line forward to grab the result of
472  // the malloc once it is cast.
473  local_instruction_iterator++;
474  if(local_instruction_iterator->is_assign())
475  {
476  const exprt &rhs = local_instruction_iterator->get_assign().rhs();
477  INVARIANT(
478  rhs.id() == ID_typecast,
479  "malloc is called but the result is not cast. Excluding result from "
480  "the assignable memory frame.");
481  typet cast_type = rhs.type();
482 
483  // Make freshly allocated memory assignable, if we can determine its type.
484  assigns_clause_targett *new_target =
485  assigns_clause.add_pointer_target(rhs);
486  goto_programt &pointer_capture = new_target->get_init_block();
487 
488  int lines_to_iterate = pointer_capture.instructions.size();
489  program.insert_before_swap(local_instruction_iterator, pointer_capture);
490  std::advance(instruction_iterator, lines_to_iterate + 1);
491  }
492  return; // assume malloc edits no pre-existing memory objects.
493  }
494 
495  if(
496  call.lhs().is_not_nil() && call.lhs().id() == ID_symbol &&
497  freely_assignable_symbols.find(
498  to_symbol_expr(call.lhs()).get_identifier()) ==
499  freely_assignable_symbols.end())
500  {
501  exprt alias_expr = assigns_clause.alias_expression(call.lhs());
502 
503  goto_programt alias_assertion;
504  alias_assertion.add(goto_programt::make_assertion(
505  alias_expr, instruction_iterator->source_location));
506  program.insert_before_swap(instruction_iterator, alias_assertion);
507  ++instruction_iterator;
508  }
509 
510  PRECONDITION(call.function().id() == ID_symbol);
511  const symbolt &called_symbol = ns.lookup(called_name);
512  const code_typet &called_type = to_code_type(called_symbol.type);
513 
514  exprt called_assigns =
515  to_code_with_contract_type(called_symbol.type).assigns();
516  if(called_assigns.is_nil()) // Called function has no assigns clause
517  {
518  // Create a false assertion, so the analysis
519  // will fail if this function is called.
520  goto_programt failing_assertion;
521  failing_assertion.add(goto_programt::make_assertion(
522  false_exprt(), instruction_iterator->source_location));
523  program.insert_before_swap(instruction_iterator, failing_assertion);
524  ++instruction_iterator;
525 
526  return;
527  }
528  else // Called function has assigns clause
529  {
531  // Replace formal parameters
532  code_function_callt::argumentst::const_iterator a_it =
533  call.arguments().begin();
534  for(code_typet::parameterst::const_iterator p_it =
535  called_type.parameters().begin();
536  p_it != called_type.parameters().end() &&
537  a_it != call.arguments().end();
538  ++p_it, ++a_it)
539  {
540  if(!p_it->get_identifier().empty())
541  {
542  symbol_exprt p(p_it->get_identifier(), p_it->type());
543  replace.insert(p, *a_it);
544  }
545  }
546 
547  replace(called_assigns);
548 
549  // check compatibility of assigns clause with the called function
550  assigns_clauset called_assigns_clause(
551  called_assigns, *this, function_id, log);
552  exprt compatible =
553  assigns_clause.compatible_expression(called_assigns_clause);
554  goto_programt alias_assertion;
555  alias_assertion.add(goto_programt::make_assertion(
556  compatible, instruction_iterator->source_location));
557  program.insert_before_swap(instruction_iterator, alias_assertion);
558  ++instruction_iterator;
559  }
560 }
561 
563 {
564  // Collect all GOTOs and mallocs
565  std::vector<goto_programt::instructiont> back_gotos;
566  std::vector<goto_programt::instructiont> malloc_calls;
567 
568  int index = 0;
569  for(goto_programt::instructiont instruction : program.instructions)
570  {
571  if(instruction.is_backwards_goto())
572  {
573  back_gotos.push_back(instruction);
574  }
575  if(instruction.is_function_call())
576  {
577  code_function_callt call = instruction.get_function_call();
578  const irep_idt &called_name =
580 
581  if(called_name == "malloc")
582  {
583  malloc_calls.push_back(instruction);
584  }
585  }
586  index++;
587  }
588  // Make sure there are no gotos that go back such that a malloc
589  // is between the goto and its destination (possible loop).
590  for(auto goto_entry : back_gotos)
591  {
592  for(const auto &target : goto_entry.targets)
593  {
594  for(auto malloc_entry : malloc_calls)
595  {
596  if(
597  malloc_entry.location_number >= target->location_number &&
598  malloc_entry.location_number < goto_entry.location_number)
599  {
600  log.error() << "Call to malloc at location "
601  << malloc_entry.location_number << " falls between goto "
602  << "source location " << goto_entry.location_number
603  << " and it's destination at location "
604  << target->location_number << ". "
605  << "Unable to complete instrumentation, as this malloc "
606  << "may be in a loop." << messaget::eom;
607  throw 0;
608  }
609  }
610  }
611  }
612  return false;
613 }
614 
615 bool code_contractst::add_pointer_checks(const std::string &function_name)
616 {
617  // Get the function object before instrumentation.
618  auto old_function = goto_functions.function_map.find(function_name);
619  if(old_function == goto_functions.function_map.end())
620  {
621  log.error() << "Could not find function '" << function_name
622  << "' in goto-program; not enforcing contracts."
623  << messaget::eom;
624  return true;
625  }
626  goto_programt &program = old_function->second.body;
627  if(program.instructions.empty()) // empty function body
628  {
629  return false;
630  }
631 
632  const irep_idt function_id(function_name);
633  const symbolt &function_symbol = ns.lookup(function_id);
634  const auto &type = to_code_with_contract_type(function_symbol.type);
635 
636  exprt assigns_expr = type.assigns();
637  // Return if there are no reference checks to perform.
638  if(assigns_expr.is_nil())
639  return false;
640 
641  assigns_clauset assigns(assigns_expr, *this, function_id, log);
642 
643  goto_programt::instructionst::iterator instruction_it =
644  program.instructions.begin();
645 
646  // Create temporary variables to hold the assigns
647  // clause targets before they can be modified.
648  goto_programt standin_decls = assigns.init_block(function_symbol.location);
649  goto_programt mark_dead = assigns.dead_stmts(
650  function_symbol.location, function_name, function_symbol.mode);
651 
652  // Create a list of variables that are okay to assign.
653  std::set<irep_idt> freely_assignable_symbols;
654  for(code_typet::parametert param : type.parameters())
655  {
656  freely_assignable_symbols.insert(param.get_identifier());
657  }
658 
659  int lines_to_iterate = standin_decls.instructions.size();
660  program.insert_before_swap(instruction_it, standin_decls);
661  std::advance(instruction_it, lines_to_iterate);
662 
663  if(check_for_looped_mallocs(program))
664  {
665  return true;
666  }
667 
668  // Insert aliasing assertions
669  for(; instruction_it != program.instructions.end(); ++instruction_it)
670  {
671  if(instruction_it->is_decl())
672  {
673  freely_assignable_symbols.insert(
674  instruction_it->get_decl().symbol().get_identifier());
675 
676  assigns_clause_targett *new_target =
677  assigns.add_target(instruction_it->get_decl().symbol());
678  goto_programt &pointer_capture = new_target->get_init_block();
679 
680  lines_to_iterate = pointer_capture.instructions.size();
681  for(auto in : pointer_capture.instructions)
682  {
683  program.insert_after(instruction_it, in);
684  ++instruction_it;
685  }
686  }
687  else if(instruction_it->is_assign())
688  {
690  instruction_it,
691  program,
692  assigns_expr,
693  freely_assignable_symbols,
694  assigns);
695  }
696  else if(instruction_it->is_function_call())
697  {
699  instruction_it,
700  program,
701  assigns_expr,
702  function_id,
703  freely_assignable_symbols,
704  assigns);
705  }
706  }
707 
708  // Walk the iterator back to the last statement
709  while(!instruction_it->is_end_function())
710  {
711  --instruction_it;
712  }
713 
714  // Make sure the temporary symbols are marked dead
715  lines_to_iterate = mark_dead.instructions.size();
716  program.insert_before_swap(instruction_it, mark_dead);
717 
718  return false;
719 }
720 
721 bool code_contractst::enforce_contract(const std::string &fun_to_enforce)
722 {
723  // Add statements to the source function
724  // to ensure assigns clause is respected.
725  add_pointer_checks(fun_to_enforce);
726 
727  // Rename source function
728  std::stringstream ss;
729  ss << CPROVER_PREFIX << "contracts_original_" << fun_to_enforce;
730  const irep_idt mangled(ss.str());
731  const irep_idt original(fun_to_enforce);
732 
733  auto old_function = goto_functions.function_map.find(original);
734  if(old_function == goto_functions.function_map.end())
735  {
736  log.error() << "Could not find function '" << fun_to_enforce
737  << "' in goto-program; not enforcing contracts."
738  << messaget::eom;
739  return true;
740  }
741 
742  std::swap(goto_functions.function_map[mangled], old_function->second);
743  goto_functions.function_map.erase(old_function);
744 
745  // Place a new symbol with the mangled name into the symbol table
746  source_locationt sl;
747  sl.set_file("instrumented for code contracts");
748  sl.set_line("0");
749  symbolt mangled_sym;
750  const symbolt *original_sym = symbol_table.lookup(original);
751  mangled_sym = *original_sym;
752  mangled_sym.name = mangled;
753  mangled_sym.base_name = mangled;
754  mangled_sym.location = sl;
755  const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
756  INVARIANT(
757  mangled_found.second,
758  "There should be no existing function called " + ss.str() +
759  " in the symbol table because that name is a mangled name");
760 
761  // Insert wrapper function into goto_functions
762  auto nexist_old_function = goto_functions.function_map.find(original);
763  INVARIANT(
764  nexist_old_function == goto_functions.function_map.end(),
765  "There should be no function called " + fun_to_enforce +
766  " in the function map because that function should have had its"
767  " name mangled");
768 
769  auto mangled_fun = goto_functions.function_map.find(mangled);
770  INVARIANT(
771  mangled_fun != goto_functions.function_map.end(),
772  "There should be a function called " + ss.str() +
773  " in the function map because we inserted a fresh goto-program"
774  " with that mangled name");
775 
776  goto_functiont &wrapper = goto_functions.function_map[original];
777  wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
779  add_contract_check(original, mangled, wrapper.body);
780  return false;
781 }
782 
784  const irep_idt &wrapper_fun,
785  const irep_idt &mangled_fun,
786  goto_programt &dest)
787 {
788  PRECONDITION(!dest.instructions.empty());
789 
790  const symbolt &function_symbol = ns.lookup(mangled_fun);
791  const auto &code_type = to_code_with_contract_type(function_symbol.type);
792 
793  const exprt &assigns = code_type.assigns();
794  const exprt &requires = code_type.requires();
795  const exprt &ensures = code_type.ensures();
796  INVARIANT(
797  ensures.is_not_nil() || assigns.is_not_nil(),
798  "Code contract enforcement is trivial without an ensures or assigns "
799  "clause.");
800 
801  // build:
802  // if(nondet)
803  // decl ret
804  // decl parameter1 ...
805  // assume(requires) [optional]
806  // ret=function(parameter1, ...)
807  // assert(ensures)
808  // skip: ...
809 
810  // build skip so that if(nondet) can refer to it
811  goto_programt tmp_skip;
813  tmp_skip.add(goto_programt::make_skip(ensures.source_location()));
814 
815  goto_programt check;
816 
817  // prepare function call including all declarations
818  code_function_callt call(function_symbol.symbol_expr());
820 
821  // decl ret
822  code_returnt return_stmt;
823  if(code_type.return_type() != empty_typet())
824  {
826  code_type.return_type(),
827  skip->source_location,
828  wrapper_fun,
829  function_symbol.mode)
830  .symbol_expr();
831  check.add(goto_programt::make_decl(r, skip->source_location));
832 
833  call.lhs()=r;
834  return_stmt = code_returnt(r);
835 
836  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
837  replace.insert(ret_val, r);
838  }
839 
840  // decl parameter1 ...
841  goto_functionst::function_mapt::iterator f_it =
842  goto_functions.function_map.find(mangled_fun);
844 
845  const goto_functionst::goto_functiont &gf = f_it->second;
846  for(const auto &parameter : gf.parameter_identifiers)
847  {
848  PRECONDITION(!parameter.empty());
849  const symbolt &parameter_symbol = ns.lookup(parameter);
851  parameter_symbol.type,
852  skip->source_location,
853  wrapper_fun,
854  parameter_symbol.mode)
855  .symbol_expr();
858  p, parameter_symbol.symbol_expr(), skip->source_location));
859 
860  call.arguments().push_back(p);
861 
862  replace.insert(parameter_symbol.symbol_expr(), p);
863  }
864 
865  // Add quantified variables in contracts to the symbol map
867  ensures, replace, function_symbol.mode);
869  requires, replace, function_symbol.mode);
870 
871  // assume(requires)
872  if(requires.is_not_nil())
873  {
874  // rewrite any use of parameters
875  exprt requires_cond = requires;
876  replace(requires_cond);
877 
878  goto_programt assumption;
880  code_assumet(requires_cond), function_symbol.mode, assumption);
881  check.destructive_append(assumption);
882  }
883 
884  // ret=mangled_fun(parameter1, ...)
886 
887  // rewrite any use of __CPROVER_return_value
888  exprt ensures_cond = ensures;
889  replace(ensures_cond);
890 
891  // assert(ensures)
892  if(ensures.is_not_nil())
893  {
894  goto_programt assertion;
896  code_assertt(ensures_cond), function_symbol.mode, assertion);
897  check.destructive_append(assertion);
898  }
899 
900  if(code_type.return_type() != empty_typet())
901  {
902  check.add(goto_programt::make_return(return_stmt, skip->source_location));
903  }
904 
905  // prepend the new code to dest
906  check.destructive_append(tmp_skip);
907  dest.destructive_insert(dest.instructions.begin(), check);
908 }
909 
911  const std::set<std::string> &funs_to_replace)
912 {
913  bool fail = false;
914  for(const auto &fun : funs_to_replace)
915  {
916  if(!has_contract(fun))
917  {
918  log.error() << "Function '" << fun
919  << "' does not have a contract; "
920  "not replacing calls with contract."
921  << messaget::eom;
922  fail = true;
923  }
924  }
925  if(fail)
926  return true;
927 
928  for(auto &goto_function : goto_functions.function_map)
929  {
930  Forall_goto_program_instructions(ins, goto_function.second.body)
931  {
932  if(ins->is_function_call())
933  {
934  const code_function_callt &call = ins->get_function_call();
935 
936  if(call.function().id() != ID_symbol)
937  continue;
938 
939  const irep_idt &function_name =
941  auto found = std::find(
942  funs_to_replace.begin(),
943  funs_to_replace.end(),
944  id2string(function_name));
945  if(found == funs_to_replace.end())
946  continue;
947 
948  fail |= apply_function_contract(
949  function_name, goto_function.second.body, ins);
950  }
951  }
952  }
953 
954  if(fail)
955  return true;
956 
957  for(auto &goto_function : goto_functions.function_map)
958  remove_skip(goto_function.second.body);
959 
961 
962  return false;
963 }
964 
966 {
967  std::set<std::string> funs_to_replace;
968  for(auto &goto_function : goto_functions.function_map)
969  {
970  if(has_contract(goto_function.first))
971  funs_to_replace.insert(id2string(goto_function.first));
972  }
973  return replace_calls(funs_to_replace);
974 }
975 
977 {
978  std::set<std::string> funs_to_enforce;
979  for(auto &goto_function : goto_functions.function_map)
980  {
981  if(has_contract(goto_function.first))
982  funs_to_enforce.insert(id2string(goto_function.first));
983  else
984  apply_loop_contract(goto_function.second);
985  }
986  return enforce_contracts(funs_to_enforce);
987 }
988 
990  const std::set<std::string> &funs_to_enforce)
991 {
992  bool fail = false;
993  for(const auto &fun : funs_to_enforce)
994  {
995  auto goto_function = goto_functions.function_map.find(fun);
996  if(goto_function == goto_functions.function_map.end())
997  {
998  fail = true;
999  log.error() << "Could not find function '" << fun
1000  << "' in goto-program; not enforcing contracts."
1001  << messaget::eom;
1002  continue;
1003  }
1004  apply_loop_contract(goto_function->second);
1005 
1006  if(!has_contract(fun))
1007  {
1008  fail = true;
1009  log.error() << "Could not find any contracts within function '" << fun
1010  << "'; nothing to enforce." << messaget::eom;
1011  continue;
1012  }
1013 
1014  if(!fail)
1015  fail = enforce_contract(fun);
1016  }
1017  return fail;
1018 }
1019 
1021  const exprt &object_ptr,
1022  code_contractst &contract,
1023  messaget &log_parameter,
1024  const irep_idt &function_id)
1026  Scalar,
1027  pointer_for(object_ptr),
1028  contract,
1029  log_parameter),
1030  local_standin_variable(typet())
1031 {
1032  const symbolt &function_symbol = contract.ns.lookup(function_id);
1033 
1034  // Declare a new symbol to stand in for the reference
1035  symbolt standin_symbol = contract.new_tmp_symbol(
1036  pointer_object.type(),
1037  function_symbol.location,
1038  function_id,
1039  function_symbol.mode);
1040 
1041  local_standin_variable = standin_symbol.symbol_expr();
1042 
1043  // Build standin variable initialization block
1044  init_block.add(
1048  function_symbol.location));
1049 }
1050 
1051 std::vector<symbol_exprt>
1053 {
1054  std::vector<symbol_exprt> result;
1055  result.push_back(local_standin_variable);
1056  return result;
1057 }
1058 
1060 {
1061  return same_object(ptr, local_standin_variable);
1062 }
1063 
1065  const assigns_clause_targett &called_target)
1066 {
1067  if(called_target.target_type == Scalar)
1068  {
1069  return alias_expression(called_target.get_direct_pointer());
1070  }
1071  else // Struct or Array
1072  {
1073  return false_exprt();
1074  }
1075 }
1076 
1079 {
1080  goto_programt assigns_havoc;
1081 
1083  side_effect_expr_nondett rhs(lhs.type(), location);
1084 
1085  goto_programt::targett target =
1086  assigns_havoc.add(goto_programt::make_assignment(
1087  code_assignt(std::move(lhs), std::move(rhs)), location));
1088  target->code_nonconst().add_source_location() = location;
1089 
1090  return assigns_havoc;
1091 }
1092 
1094  const exprt &object_ptr,
1095  code_contractst &contract,
1096  messaget &log_parameter,
1097  const irep_idt &function_id)
1099  Struct,
1100  pointer_for(object_ptr),
1101  contract,
1102  log_parameter),
1103  main_struct_standin(typet())
1104 {
1105  const symbolt &struct_symbol =
1106  contract.ns.lookup(to_tag_type(object_ptr.type()));
1107  const symbolt &function_symbol = contract.ns.lookup(function_id);
1108 
1109  // Declare a new symbol to stand in for the reference
1110  symbolt struct_temp_symbol = contract.new_tmp_symbol(
1111  pointer_object.type(),
1112  function_symbol.location,
1113  function_id,
1114  function_symbol.mode);
1115  main_struct_standin = struct_temp_symbol.symbol_expr();
1117 
1118  // Build standin variable initialization block
1119  init_block.add(
1123  function_symbol.location));
1124 
1125  // Handle component members
1126  std::vector<exprt> component_members;
1127  const struct_typet &struct_type = to_struct_type(struct_symbol.type);
1129  {
1130  exprt current_member = member_exprt(object_ptr, component);
1131  component_members.push_back(current_member);
1132  }
1133 
1134  while(!component_members.empty())
1135  {
1136  exprt current_operation = component_members.front();
1137  exprt operation_address = pointer_for(current_operation);
1138 
1139  // Declare a new symbol to stand in for the reference
1140  symbolt standin_symbol = contract.new_tmp_symbol(
1141  operation_address.type(),
1142  function_symbol.location,
1143  function_id,
1144  function_symbol.mode);
1145 
1146  symbol_exprt current_standin = standin_symbol.symbol_expr();
1147  local_standin_variables.push_back(current_standin);
1148 
1149  // Add to standin variable initialization block
1150  init_block.add(
1151  goto_programt::make_decl(current_standin, function_symbol.location));
1153  code_assignt(current_standin, operation_address),
1154  function_symbol.location));
1155 
1156  if(current_operation.type().id() == ID_struct_tag)
1157  {
1158  const symbolt &current_struct_symbol =
1159  contract.ns.lookup(to_tag_type(current_operation.type()));
1160 
1161  const struct_typet &curr_struct_t =
1162  to_struct_type(current_struct_symbol.type);
1163  for(struct_union_typet::componentt component : curr_struct_t.components())
1164  {
1165  exprt current_member = member_exprt(current_operation, component);
1166  component_members.push_back(current_member);
1167  }
1168  }
1169  component_members.erase(component_members.begin());
1170  }
1171 }
1172 
1173 std::vector<symbol_exprt>
1175 {
1176  return local_standin_variables;
1177 }
1178 
1180 {
1181  exprt::operandst disjuncts;
1182  disjuncts.reserve(local_standin_variables.size());
1184  {
1185  const typet &ptr_concrete_type = to_pointer_type(ptr.type()).subtype();
1186  auto left_size = size_of_expr(ptr_concrete_type, contract.ns);
1187  const typet &standin_concrete_type =
1188  to_pointer_type(symbol.type()).subtype();
1189  auto right_size = size_of_expr(standin_concrete_type, contract.ns);
1190  INVARIANT(left_size.has_value(), "Unable to determine size of type (lhs).");
1191  INVARIANT(
1192  right_size.has_value(), "Unable to determine size of type (rhs).");
1193  if(*left_size == *right_size)
1194  {
1195  exprt same_obj = same_object(ptr, symbol);
1196  exprt same_offset =
1197  equal_exprt(pointer_offset(ptr), pointer_offset(symbol));
1198 
1199  disjuncts.push_back(and_exprt{same_obj, same_offset});
1200  }
1201  }
1202 
1203  return disjunction(disjuncts);
1204 }
1205 
1207  const assigns_clause_targett &called_target)
1208 {
1209  if(called_target.target_type == Scalar)
1210  {
1211  return alias_expression(called_target.get_direct_pointer());
1212  }
1213  else if(called_target.target_type == Struct)
1214  {
1215  const assigns_clause_struct_targett &struct_target =
1216  static_cast<const assigns_clause_struct_targett &>(called_target);
1217 
1218  exprt same_obj =
1219  same_object(this->main_struct_standin, struct_target.pointer_object);
1220  // the size of the called struct should be less than or
1221  // equal to that of the assignable target struct.
1222  exprt current_size =
1224  exprt curr_upper_offset =
1225  pointer_offset(plus_exprt(this->main_struct_standin, current_size));
1226  exprt called_size =
1227  get_size(struct_target.pointer_object.type(), contract.ns, log);
1228  exprt called_upper_offset =
1229  pointer_offset(plus_exprt(struct_target.pointer_object, called_size));
1230 
1231  exprt in_range_lower = binary_predicate_exprt(
1232  pointer_offset(struct_target.pointer_object),
1233  ID_ge,
1235  exprt in_range_upper =
1236  binary_predicate_exprt(curr_upper_offset, ID_ge, called_upper_offset);
1237 
1238  exprt in_range = and_exprt(in_range_lower, in_range_upper);
1239  return and_exprt(same_obj, in_range);
1240  }
1241  else // Array
1242  {
1243  return false_exprt();
1244  }
1245 }
1246 
1249 {
1250  goto_programt assigns_havoc;
1251 
1253  side_effect_expr_nondett rhs(lhs.type(), location);
1254 
1255  goto_programt::targett target =
1256  assigns_havoc.add(goto_programt::make_assignment(
1257  code_assignt(std::move(lhs), std::move(rhs)), location));
1258  target->code_nonconst().add_source_location() = location;
1259 
1260  return assigns_havoc;
1261 }
1262 
1264  const exprt &object_ptr,
1265  code_contractst &contract,
1266  messaget &log_parameter,
1267  const irep_idt &function_id)
1268  : assigns_clause_targett(Array, object_ptr, contract, log_parameter),
1269  lower_offset_object(),
1270  upper_offset_object(),
1271  array_standin_variable(typet()),
1272  lower_offset_variable(typet()),
1273  upper_offset_variable(typet())
1274 {
1275  const symbolt &function_symbol = contract.ns.lookup(function_id);
1276 
1277  // Declare a new symbol to stand in for the reference
1278  symbolt standin_symbol = contract.new_tmp_symbol(
1279  pointer_object.type(),
1280  function_symbol.location,
1281  function_id,
1282  function_symbol.mode);
1283 
1284  array_standin_variable = standin_symbol.symbol_expr();
1285 
1286  // Add array temp to variable initialization block
1287  init_block.add(
1291  function_symbol.location));
1292 
1293  if(object_ptr.id() == ID_address_of)
1294  {
1295  exprt constant_size =
1296  get_size(object_ptr.type().subtype(), contract.ns, log);
1298  mult_exprt(
1299  typecast_exprt(object_ptr, unsigned_long_int_type()), constant_size),
1300  signed_int_type());
1301 
1302  // Declare a new symbol to stand in for the reference
1303  symbolt lower_standin_symbol = contract.new_tmp_symbol(
1305  function_symbol.location,
1306  function_id,
1307  function_symbol.mode);
1308 
1309  lower_offset_variable = lower_standin_symbol.symbol_expr();
1310 
1311  // Add array temp to variable initialization block
1313  lower_offset_variable, function_symbol.location));
1316  function_symbol.location));
1317 
1319  mult_exprt(
1320  typecast_exprt(object_ptr, unsigned_long_int_type()), constant_size),
1321  signed_int_type());
1322 
1323  // Declare a new symbol to stand in for the reference
1324  symbolt upper_standin_symbol = contract.new_tmp_symbol(
1326  function_symbol.location,
1327  function_id,
1328  function_symbol.mode);
1329 
1330  upper_offset_variable = upper_standin_symbol.symbol_expr();
1331 
1332  // Add array temp to variable initialization block
1334  upper_offset_variable, function_symbol.location));
1337  function_symbol.location));
1338  }
1339 }
1340 
1341 std::vector<symbol_exprt>
1343 {
1344  std::vector<symbol_exprt> result;
1345  result.push_back(array_standin_variable);
1346  result.push_back(lower_offset_variable);
1347  result.push_back(upper_offset_variable);
1348 
1349  return result;
1350 }
1351 
1354 {
1355  goto_programt assigns_havoc;
1356 
1357  modifiest assigns_tgts;
1358  typet lower_type = lower_offset_variable.type();
1359  exprt array_type_size =
1361 
1362  for(mp_integer i = lower_bound; i < upper_bound; ++i)
1363  {
1364  irep_idt offset_string(from_integer(i, integer_typet()).get_value());
1365  irep_idt offset_irep(offset_string);
1366  constant_exprt val_const(offset_irep, lower_type);
1367  dereference_exprt array_deref(plus_exprt(
1369 
1370  assigns_tgts.insert(array_deref);
1371  }
1372 
1373  for(auto lhs : assigns_tgts)
1374  {
1375  side_effect_expr_nondett rhs(lhs.type(), location);
1376 
1377  goto_programt::targett target =
1378  assigns_havoc.add(goto_programt::make_assignment(
1379  code_assignt(std::move(lhs), std::move(rhs)), location));
1380  target->code_nonconst().add_source_location() = location;
1381  }
1382 
1383  return assigns_havoc;
1384 }
1385 
1387 {
1388  exprt ptr_offset = pointer_offset(ptr);
1389  exprt::operandst conjuncts;
1390 
1391  conjuncts.push_back(same_object(ptr, array_standin_variable));
1392  conjuncts.push_back(binary_predicate_exprt(
1393  ptr_offset,
1394  ID_ge,
1395  typecast_exprt(lower_offset_variable, ptr_offset.type())));
1396  conjuncts.push_back(binary_predicate_exprt(
1397  typecast_exprt(upper_offset_variable, ptr_offset.type()),
1398  ID_ge,
1399  ptr_offset));
1400 
1401  return conjunction(conjuncts);
1402 }
1403 
1405  const assigns_clause_targett &called_target)
1406 {
1407  if(called_target.target_type == Scalar)
1408  {
1409  return alias_expression(called_target.get_direct_pointer());
1410  }
1411  else if(called_target.target_type == Array)
1412  {
1413  const assigns_clause_array_targett &array_target =
1414  static_cast<const assigns_clause_array_targett &>(called_target);
1415  exprt same_obj =
1416  same_object(this->array_standin_variable, array_target.pointer_object);
1417  exprt in_range_lower = binary_predicate_exprt(
1418  array_target.lower_offset_object, ID_ge, this->lower_offset_variable);
1419  exprt in_range_upper = binary_predicate_exprt(
1420  this->upper_offset_variable, ID_ge, array_target.upper_offset_object);
1421  exprt in_range = and_exprt(in_range_lower, in_range_upper);
1422  return and_exprt(same_obj, in_range);
1423  }
1424  else // Struct
1425  {
1426  return false_exprt();
1427  }
1428 }
1429 
1431  const exprt &assigns,
1432  code_contractst &contract,
1433  const irep_idt function_id,
1434  messaget log_parameter)
1435  : assigns_expr(assigns),
1436  parent(contract),
1437  function_id(function_id),
1438  log(log_parameter)
1439 {
1440  for(exprt current_operation : assigns_expr.operands())
1441  {
1442  add_target(current_operation);
1443  }
1444 }
1446 {
1447  for(assigns_clause_targett *target : targets)
1448  {
1449  delete target;
1450  }
1451 }
1452 
1454 {
1455  if(current_operation.id() == ID_address_of)
1456  {
1457  assigns_clause_array_targett *array_target =
1459  current_operation, parent, log, function_id);
1460  targets.push_back(array_target);
1461  return array_target;
1462  }
1463  else if(current_operation.type().id() == ID_struct_tag)
1464  {
1465  assigns_clause_struct_targett *struct_target =
1467  current_operation, parent, log, function_id);
1468  targets.push_back(struct_target);
1469  return struct_target;
1470  }
1471  else
1472  {
1473  assigns_clause_scalar_targett *scalar_target =
1475  current_operation, parent, log, function_id);
1476  targets.push_back(scalar_target);
1477  return scalar_target;
1478  }
1479 }
1480 
1483 {
1484  return add_target(dereference_exprt(current_operation));
1485 }
1486 
1488 {
1489  goto_programt result;
1490  for(assigns_clause_targett *target : targets)
1491  {
1492  for(goto_programt::instructiont inst :
1493  target->get_init_block().instructions)
1494  {
1495  result.add(goto_programt::instructiont(inst));
1496  }
1497  }
1498  return result;
1499 }
1500 
1502  source_locationt location,
1503  irep_idt function_name,
1504  irep_idt language_mode)
1505 {
1507  {
1508  for(assigns_clause_targett *target : targets)
1509  {
1510  for(symbol_exprt symbol : target->temporary_declarations())
1511  {
1513  goto_programt::make_decl(symbol, symbol.source_location()));
1514  }
1515  }
1516  }
1517  return standin_declarations;
1518 }
1519 
1521  source_locationt location,
1522  irep_idt function_name,
1523  irep_idt language_mode)
1524 {
1525  goto_programt dead_statements;
1526  for(assigns_clause_targett *target : targets)
1527  {
1528  for(symbol_exprt symbol : target->temporary_declarations())
1529  {
1530  dead_statements.add(
1531  goto_programt::make_dead(symbol, symbol.source_location()));
1532  }
1533  }
1534  return dead_statements;
1535 }
1536 
1538  source_locationt location,
1539  irep_idt function_name,
1540  irep_idt language_mode)
1541 {
1542  goto_programt havoc_statements;
1543  for(assigns_clause_targett *target : targets)
1544  {
1545  for(goto_programt::instructiont instruction :
1546  target->havoc_code(location).instructions)
1547  {
1548  havoc_statements.add(std::move(instruction));
1549  }
1550  }
1551  return havoc_statements;
1552 }
1553 
1555 {
1556  if(targets.empty())
1557  {
1558  return false_exprt();
1559  }
1560 
1562 
1563  bool first_iter = true;
1564  exprt result = false_exprt();
1565  for(assigns_clause_targett *target : targets)
1566  {
1567  if(first_iter)
1568  {
1569  result = target->alias_expression(left_ptr);
1570  first_iter = false;
1571  }
1572  else
1573  {
1574  result = or_exprt(result, target->alias_expression(left_ptr));
1575  }
1576  }
1577  return result;
1578 }
1579 
1581  const assigns_clauset &called_assigns)
1582 {
1583  if(called_assigns.targets.empty())
1584  {
1585  return true_exprt();
1586  }
1587 
1588  bool first_clause = true;
1589  exprt result = true_exprt();
1590  for(assigns_clause_targett *called_target : called_assigns.targets)
1591  {
1592  bool first_iter = true;
1593  exprt current_target_compatible = false_exprt();
1594  for(assigns_clause_targett *target : targets)
1595  {
1596  if(first_iter)
1597  {
1598  current_target_compatible =
1599  target->compatible_expression(*called_target);
1600  first_iter = false;
1601  }
1602  else
1603  {
1604  current_target_compatible = or_exprt(
1605  current_target_compatible,
1606  target->compatible_expression(*called_target));
1607  }
1608  }
1609  if(first_clause)
1610  {
1611  result = current_target_compatible;
1612  first_clause = false;
1613  }
1614  else
1615  {
1616  exprt::operandst conjuncts;
1617  conjuncts.push_back(result);
1618  conjuncts.push_back(current_target_compatible);
1619  result = conjunction(conjuncts);
1620  }
1621  }
1622 
1623  return result;
1624 }
assigns_clause_array_targett::temporary_declarations
std::vector< symbol_exprt > temporary_declarations() const
Definition: code_contracts.cpp:1342
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1185
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
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
assigns_clause_array_targett::compatible_expression
exprt compatible_expression(const assigns_clause_targett &called_target)
Definition: code_contracts.cpp:1404
to_code_with_contract_type
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition: c_types.h:397
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
assigns_clauset::function_id
const irep_idt function_id
Definition: code_contracts.h:364
assigns_clause_scalar_targett::havoc_code
goto_programt havoc_code(source_locationt location) const
Definition: code_contracts.cpp:1078
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
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
assigns_clause_struct_targett::compatible_expression
exprt compatible_expression(const assigns_clause_targett &called_target)
Definition: code_contracts.cpp:1206
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
assigns_clause_targett::target_type
target_type
Definition: code_contracts.h:209
code_contractst::add_contract_check
void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest)
Definition: code_contracts.cpp:783
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:141
arith_tools.h
assigns_clause_array_targett::upper_offset_object
exprt upper_offset_object
Definition: code_contracts.h:321
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:911
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
assigns_clauset::dead_stmts
goto_programt dead_stmts(source_locationt location, irep_idt function_name, irep_idt language_mode)
Definition: code_contracts.cpp:1520
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
assigns_clauset::targets
std::vector< assigns_clause_targett * > targets
Definition: code_contracts.h:360
fresh_symbol.h
Fresh auxiliary symbol creation.
assigns_clause_targett::log
messaget & log
Definition: code_contracts.h:262
assigns_clauset::assigns_expr
const exprt & assigns_expr
Definition: code_contracts.h:358
code_contractst::add_quantified_variable
void add_quantified_variable(exprt expression, replace_symbolt &replace, irep_idt mode)
This function recursively searches the expression to find nested or non-nested quantified expressions...
Definition: code_contracts.cpp:177
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
assigns_clause_struct_targett::temporary_declarations
std::vector< symbol_exprt > temporary_declarations() const
Definition: code_contracts.cpp:1174
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
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
assigns_clause_targett::pointer_for
static exprt pointer_for(const exprt &exp)
Definition: code_contracts.h:251
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:122
replace_symbol.h
pointer_predicates.h
Various predicates over pointers in programs.
assigns_clause_array_targett::assigns_clause_array_targett
assigns_clause_array_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
Definition: code_contracts.cpp:1263
assigns_clause_array_targett::lower_offset_variable
symbol_exprt lower_offset_variable
Definition: code_contracts.h:324
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
assigns_clause_scalar_targett::compatible_expression
exprt compatible_expression(const assigns_clause_targett &called_target)
Definition: code_contracts.cpp:1064
code_contractst::apply_function_contract
bool apply_function_contract(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target)
Definition: code_contracts.cpp:247
code_assertt
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:619
goto_convert_class.h
Program Transformation.
and_exprt
Boolean AND.
Definition: std_expr.h:1834
assigns_clause_array_targett::upper_bound
mp_integer upper_bound
Definition: code_contracts.h:318
integer_typet
Unbounded, signed integers (mathematical integers, not bitvectors)
Definition: mathematical_types.h:22
return_value_visitort
Predicate to be used with the exprt::visit() function.
Definition: code_contracts.cpp:43
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:941
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
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:746
assigns_clauset::alias_expression
exprt alias_expression(const exprt &lhs)
Definition: code_contracts.cpp:1554
exprt
Base class for all expressions.
Definition: expr.h:54
code_contractst::log
messaget & log
Definition: code_contracts.h:100
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
code_with_contract_typet::assigns
const exprt & assigns() const
Definition: c_types.h:348
bool_typet
The Boolean type.
Definition: std_types.h:36
assigns_clause_targett::contract
const code_contractst & contract
Definition: code_contracts.h:260
messaget::eom
static eomt eom
Definition: message.h:297
assigns_clauset::add_pointer_target
assigns_clause_targett * add_pointer_target(exprt current_operation)
Definition: code_contracts.cpp:1482
assigns_clauset::add_target
assigns_clause_targett * add_target(exprt current_operation)
Definition: code_contracts.cpp:1453
assigns_clauset::assigns_clauset
assigns_clauset(const exprt &assigns, code_contractst &contract, const irep_idt function_id, messaget log_parameter)
Definition: code_contracts.cpp:1430
assigns_clause_targett::pointer_object
const exprt pointer_object
Definition: code_contracts.h:259
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
assigns_clauset::log
messaget log
Definition: code_contracts.h:365
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:904
equal_exprt
Equality.
Definition: std_expr.h:1139
return_value_visitort::return_value_visitort
return_value_visitort()
Definition: code_contracts.cpp:45
exprt::visit
void visit(class expr_visitort &visitor)
These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children h...
Definition: expr.cpp:282
check_apply_invariants
static void check_apply_invariants(goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop)
Definition: code_contracts.cpp:77
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
local_may_aliast
Definition: local_may_alias.h:26
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_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:982
goto_convertt::goto_convert
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:278
assigns_clause_targett::Array
@ Array
Definition: code_contracts.h:212
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
code_contractst::instrument_call_statement
void instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, const irep_idt &function_id, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
Inserts an assertion statement into program before the function call at ins_it, to ensure that any me...
Definition: code_contracts.cpp:449
code_contractst::instrument_assign_statement
void instrument_assign_statement(goto_programt::instructionst::iterator &instruction_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
Inserts an assertion statement into program before the assignment instruction_it, to ensure that the ...
Definition: code_contracts.cpp:425
mathematical_types.h
Mathematical types.
unsigned_long_int_type
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
source_locationt::set_line
void set_line(const irep_idt &line)
Definition: source_location.h:106
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1033
assigns_clause_struct_targett::local_standin_variables
std::vector< symbol_exprt > local_standin_variables
Definition: code_contracts.h:299
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
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::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
assigns_clause_scalar_targett::temporary_declarations
std::vector< symbol_exprt > temporary_declarations() const
Definition: code_contracts.cpp:1052
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
assigns_clauset::parent
code_contractst & parent
Definition: code_contracts.h:363
modifiest
std::set< exprt > modifiest
Definition: loop_utils.h:17
assigns_clause_array_targett::lower_bound
mp_integer lower_bound
Definition: code_contracts.h:317
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:877
assigns_clauset::init_block
goto_programt init_block(source_locationt location)
Definition: code_contracts.cpp:1487
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:399
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:428
empty_typet
The empty type.
Definition: std_types.h:45
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
or_exprt
Boolean OR.
Definition: std_expr.h:1942
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:661
assigns_clause_targett::get_init_block
goto_programt & get_init_block()
Definition: code_contracts.h:246
assigns_clause_targett::Scalar
@ Scalar
Definition: code_contracts.h:210
goto_convertt
Definition: goto_convert_class.h:31
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:835
code_contractst::has_contract
bool has_contract(const irep_idt)
Does the named function have a contract?
Definition: code_contracts.cpp:170
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:567
assigns_clause_scalar_targett::alias_expression
exprt alias_expression(const exprt &lhs)
Definition: code_contracts.cpp:1059
goto_programt::instructiont::is_backwards_goto
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:521
source_locationt::set_file
void set_file(const irep_idt &file)
Definition: source_location.h:96
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
code_contractst::create_alias_expression
exprt create_alias_expression(const exprt &lhs, std::vector< exprt > &aliasable_references)
Creates a boolean expression which is true when there exists an expression in aliasable_references wi...
Definition: code_contracts.cpp:412
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
assigns_clause_struct_targett::main_struct_standin
symbol_exprt main_struct_standin
Definition: code_contracts.h:298
code_contractst::check_for_looped_mallocs
bool check_for_looped_mallocs(const goto_programt &)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
Definition: code_contracts.cpp:562
code_contractst
Definition: code_contracts.h:34
code_contractst::add_pointer_checks
bool add_pointer_checks(const std::string &)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
Definition: code_contracts.cpp:615
loop_templatet
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:935
assigns_clause_array_targett::alias_expression
exprt alias_expression(const exprt &lhs)
Definition: code_contracts.cpp:1386
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
assigns_clauset
Definition: code_contracts.h:329
const_expr_visitort
Definition: expr.h:381
assigns_clauset::temporary_declarations
goto_programt & temporary_declarations(source_locationt location, irep_idt function_name, irep_idt language_mode)
Definition: code_contracts.cpp:1501
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
code_typet
Base type of functions.
Definition: std_types.h:533
assigns_clause_scalar_targett
Definition: code_contracts.h:266
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
assigns_clauset::compatible_expression
exprt compatible_expression(const assigns_clauset &called_assigns)
Definition: code_contracts.cpp:1580
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_contractst::ns
namespacet ns
Definition: code_contracts.h:93
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
code_contractst::convert_to_goto
void convert_to_goto(const codet &code, const irep_idt &mode, goto_programt &program)
Create goto instructions based on code and add them to program.
Definition: code_contracts.cpp:161
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
assigns_clause_array_targett::array_standin_variable
symbol_exprt array_standin_variable
Definition: code_contracts.h:323
natural_loops_templatet< goto_programt, goto_programt::targett >
assigns_clause_struct_targett::alias_expression
exprt alias_expression(const exprt &lhs)
Definition: code_contracts.cpp:1179
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:38
loop_utils.h
Helper functions for k-induction and loop invariants.
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:653
code_contractst::apply_loop_contract
void apply_loop_contract(goto_functionst::goto_functiont &goto_function)
Definition: code_contracts.cpp:385
assigns_clauset::havoc_code
goto_programt havoc_code(source_locationt location, irep_idt function_name, irep_idt language_mode)
Definition: code_contracts.cpp:1537
goto_programt::make_return
static instructiont make_return(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:822
source_locationt
Definition: source_location.h:20
return_value_visitort::operator()
void operator()(const exprt &exp) override
Definition: code_contracts.cpp:56
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
code_contractst::new_tmp_symbol
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
Definition: code_contracts.cpp:397
assigns_clause_targett::Struct
@ Struct
Definition: code_contracts.h:211
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
struct_union_typet::componentt
Definition: std_types.h:63
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
assigns_clause_array_targett::havoc_code
goto_programt havoc_code(source_locationt location) const
Definition: code_contracts.cpp:1353
expr_util.h
Deprecated expression utility functions.
assigns_clause_scalar_targett::local_standin_variable
symbol_exprt local_standin_variable
Definition: code_contracts.h:280
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
assigns_clause_struct_targett
Definition: code_contracts.h:284
code_contractst::enforce_contracts
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
Definition: code_contracts.cpp:976
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
assigns_clause_array_targett::upper_offset_variable
symbol_exprt upper_offset_variable
Definition: code_contracts.h:325
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1342
code_contractst::goto_functions
goto_functionst & goto_functions
Definition: code_contracts.h:97
to_quantifier_expr
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: mathematical_expr.h:316
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
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
ASSUME
@ ASSUME
Definition: goto_program.h:36
assigns_clause_array_targett
Definition: code_contracts.h:303
get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:135
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functionst::update
void update()
Definition: goto_functions.h:81
same_object
exprt same_object(const exprt &p1, const exprt &p2)
Definition: pointer_predicates.cpp:28
assigns_clause_array_targett::lower_offset_object
exprt lower_offset_object
Definition: code_contracts.h:320
code_typet::parametert
Definition: std_types.h:550
assigns_clause_struct_targett::havoc_code
goto_programt havoc_code(source_locationt location) const
Definition: code_contracts.cpp:1248
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
signed_long_int_type
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
code_contractst::replace_calls
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
Definition: code_contracts.cpp:965
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:639
code_contractst::summarized
std::unordered_set< irep_idt > summarized
Definition: code_contracts.h:102
loop_templatet::empty
bool empty() const
Returns true if this loop contains no instructions.
Definition: loop_analysis.h:67
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
assigns_clauset::standin_declarations
goto_programt standin_declarations
Definition: code_contracts.h:361
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:278
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:36
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:889
exprt::operands
operandst & operands()
Definition: expr.h:96
r
static int8_t r
Definition: irep_hash.h:59
code_contractst::enforce_contract
bool enforce_contract(const std::string &)
Enforce contract of a single function.
Definition: code_contracts.cpp:721
static_lifetime_init.h
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:590
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
return_value_visitort::found_return_value
bool found_return_value()
Definition: code_contracts.cpp:51
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
get_size
exprt get_size(const typet &type, const namespacet &ns, messaget &log)
Definition: code_contracts.cpp:68
build_havoc_code
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:85
message.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
assigns_clause_scalar_targett::assigns_clause_scalar_targett
assigns_clause_scalar_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
Definition: code_contracts.cpp:1020
assigns_clause_targett::init_block
goto_programt init_block
Definition: code_contracts.h:261
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:445
return_value_visitort::found
bool found
Definition: code_contracts.cpp:65
assigns_clauset::~assigns_clauset
~assigns_clauset()
Definition: code_contracts.cpp:1445
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
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
assigns_clause_targett
A base class for assigns clause targets.
Definition: code_contracts.h:206
assigns_clause_targett::get_direct_pointer
const exprt & get_direct_pointer() const
Definition: code_contracts.h:241
c_types.h
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
assigns_clause_struct_targett::assigns_clause_struct_targett
assigns_clause_struct_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
Definition: code_contracts.cpp:1093
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
format_type.h
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
code_contractst::symbol_table
symbol_tablet & symbol_table
Definition: code_contracts.h:96
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
code_contracts.h
Verify and use annotated invariants and pre/post-conditions.
loop_analysist::loop_map
loop_mapt loop_map
Definition: loop_analysis.h:88
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35