CBMC
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 
17 class symbol_table_baset;
18 class goto_programt;
19 class goto_functionst;
20 class message_handlert;
21 
43 {
44 public:
55  const irep_idt &_function_id,
56  const std::vector<exprt> &_targets,
57  const goto_functionst &_functions,
58  cfg_infot &_cfg_info,
59  const source_locationt &_source_location,
60  symbol_table_baset &_st,
61  message_handlert &_message_handler)
63  _function_id,
64  _functions,
65  _cfg_info,
66  _st,
67  _message_handler),
68  targets(_targets),
69  source_location(_source_location)
70  {
71  }
72 
74  void get_instructions(goto_programt &dest);
75 
76 private:
115  void havoc_if_valid(car_exprt car, goto_programt &dest);
116 
118  void havoc_static_local(car_exprt car, goto_programt &dest);
119 
120  const std::vector<exprt> &targets;
122 };
123 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
Class that represents a normalized conditional address range, with:
Stores information about a goto function computed from its CFG.
Definition: cfg_info.h:40
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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,...
havoc_assigns_clause_targetst(const irep_idt &_function_id, const std::vector< exprt > &_targets, const goto_functionst &_functions, cfg_infot &_cfg_info, const source_locationt &_source_location, symbol_table_baset &_st, message_handlert &_message_handler)
void get_instructions(goto_programt &dest)
Generates the assigns clause replacement instructions in dest.
void havoc_static_local(car_exprt car, goto_programt &dest)
Havoc a static local expression.
A class that generates instrumentation for assigns clause checking.
The symbol table base class interface.
Specify write set in function contracts.