cprover
havoc_assigns_clause_targets.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Havoc multiple and possibly dependent targets simultaneously
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
13 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
14 
16 #include <util/expr.h>
17 
18 class namespacet;
19 class symbol_tablet;
20 class goto_programt;
21 class goto_functionst;
22 class message_handlert;
23 
55 {
56 public:
58  const irep_idt &_function_id,
59  const std::vector<exprt> &_targets,
60  const goto_functionst &_functions,
61  const source_locationt &_source_location,
62  symbol_tablet &_st,
63  message_handlert &_message_handler)
64  : instrument_spec_assignst(_function_id, _functions, _st, _message_handler),
65  targets(_targets),
66  source_location(_source_location)
67  {
68  }
69 
71  void get_instructions(goto_programt &dest);
72 
73 private:
102  void havoc_if_valid(car_exprt car, goto_programt &dest);
103 
104  const std::vector<exprt> &targets;
106 };
107 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
Class that represents a normalized conditional address range, with:
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
Class to generate havocking instructions for target expressions of a function contract's assign claus...
const std::vector< exprt > & targets
void havoc_if_valid(car_exprt car, goto_programt &dest)
Generates instructions to conditionally havoc the given conditional address range expression car,...
void get_instructions(goto_programt &dest)
Generates the assigns clause replacement instructions in dest.
havoc_assigns_clause_targetst(const irep_idt &_function_id, const std::vector< exprt > &_targets, const goto_functionst &_functions, const source_locationt &_source_location, symbol_tablet &_st, message_handlert &_message_handler)
A class that generates instrumentation for assigns clause checking.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The symbol table.
Definition: symbol_table.h:14
Specify write set in function contracts.