14#ifndef CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H
15#define CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H
Abstract interface to eager or lazy GOTO models.
Provides management of goal variables that encode properties.
An implementation of incremental_goto_checkert may implement this interface to provide goto traces.
incremental_goto_checkert()=delete
ui_message_handlert & ui_message_handler
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.
goto_tracet build_trace(const irep_idt &) const override
Builds and returns the trace for the FAILed property with the given property_id.
bool current_equation_converted
guard_managert guard_manager
void output_proof() override
goto_tracet build_shortest_trace() const override
Builds and returns the trace up to the first failed property.
symex_bmc_incremental_one_loopt symex
bool initial_equation_generated
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
void output_error_witness(const goto_tracet &) override
single_loop_incremental_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
goto_symex_property_decidert property_decider
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
symex_target_equationt equation
bool full_equation_generated
const namespacet & get_namespace() const override
Returns the namespace associated with the traces.
abstract_goto_modelt & goto_model
symbol_tablet symex_symbol_table
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
An implementation of incremental_goto_checkert may implement this interface to provide GraphML witnes...
Property Decider for Goto-Symex.
Interface for returning Goto Traces from Goto Checkers.
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.
Interface for outputting GraphML Witnesses for Goto Checkers.