12#ifndef CPROVER_GOTO_SYNTHESIZER_CEGIS_VERIFIER_H
13#define CPROVER_GOTO_SYNTHESIZER_CEGIS_VERIFIER_H
46 const std::unordered_map<exprt, mp_integer, irep_hash> &
object_sizes,
47 const std::unordered_map<exprt, mp_integer, irep_hash> &
havoced_values,
48 const std::unordered_map<exprt, mp_integer, irep_hash>
104 const std::map<
loop_idt, std::set<exprt>> &assigns_map,
108 : invariant_candidates(invariant_candidates),
109 assigns_map(assigns_map),
110 goto_model(goto_model),
113 ns(goto_model.symbol_table)
129 std::list<loop_idt> get_cause_loop_id(
136 get_cause_loop_id_for_assigns(
const goto_tracet &goto_trace);
145 unsigned location_number_of_target);
148 void restore_functions();
157 bool is_instruction_in_transformed_loop(
160 unsigned location_number_of_target);
164 bool is_instruction_in_transformed_loop_condition(
167 unsigned location_number_of_target);
170 void preprocess_goto_model();
173 const std::map<loop_idt, std::set<exprt>> &assigns_map;
181 std::unordered_map<irep_idt, goto_programt> original_functions;
185 std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
189 std::unordered_set<goto_programt::const_targett, const_target_hash>
Goto Verifier for Verifying all Properties.
Verifier that take a goto program as input, and output formatted counterexamples for counterexample-g...
std::unordered_set< goto_programt::const_targett, const_target_hash > loop_havoc_set
Loop havoc instructions instrumented during applying loop contracts.
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > original_loop_number_map
Verify goto_model.
cegis_verifiert(const invariant_mapt &invariant_candidates, const std::map< loop_idt, std::set< exprt > > &assigns_map, goto_modelt &goto_model, const optionst &options, messaget &log)
Formatted counterexample.
cext(const std::unordered_map< exprt, mp_integer, irep_hash > &object_sizes, const std::unordered_map< exprt, mp_integer, irep_hash > &havoced_values, const std::unordered_map< exprt, mp_integer, irep_hash > &havoced_pointer_offsets, const std::unordered_map< exprt, mp_integer, irep_hash > &loop_entry_values, const std::unordered_map< exprt, mp_integer, irep_hash > &loop_entry_offsets, const std::set< exprt > &live_variables)
std::unordered_map< exprt, mp_integer, irep_hash > loop_entry_values
std::list< loop_idt > cause_loop_ids
violation_locationt violation_location
@ cex_not_hold_upon_entry
cext(const violation_typet &violation_type)
std::unordered_map< exprt, mp_integer, irep_hash > loop_entry_offsets
std::unordered_map< exprt, mp_integer, irep_hash > havoced_values
std::set< exprt > live_variables
std::unordered_map< exprt, mp_integer, irep_hash > havoced_pointer_offsets
std::unordered_map< exprt, mp_integer, irep_hash > object_sizes
violation_typet violation_type
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
instructionst::const_iterator const_targett
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
nonstd::optional< T > optionalt
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Loop id used to identify loops.
std::map< loop_idt, exprt > invariant_mapt