12#ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H
13#define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H
49 std::unordered_set<irep_idt> &updated_properties);
Abstract interface to eager or lazy GOTO models.
incremental_goto_checkert()=delete
ui_message_handlert & ui_message_handler
multi_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
symbol_tablet symex_symbol_table
symex_target_equationt equation
guard_managert guard_manager
abstract_goto_modelt & goto_model
virtual void update_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Updates the properties from the equation and adds their property IDs to updated_properties.
virtual void generate_equation()
Generates the equation by running goto-symex.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
FIFO save queue: paths are resumed in the order that they were saved.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
guard_expr_managert guard_managert
Incremental Goto Checker Interface.
Storage of symbolic execution paths to resume.
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Bounded Model Checking for ANSI-C.