cprover
single_loop_incremental_symex_checker.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Multi-Path Symbolic Execution
4  with Incremental Unwinding of a specified Loop
5 
6 Author: Daniel Kroening, Peter Schrammel
7 
8 \*******************************************************************/
9 
13 
14 #ifndef CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H
15 #define CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H
16 
18 #include "goto_trace_provider.h"
21 #include "witness_provider.h"
22 
28  public goto_trace_providert,
29  public witness_providert
30 {
31 public:
33  const optionst &options,
36 
41  resultt operator()(propertiest &) override;
42 
43  goto_tracet build_full_trace() const override;
44  goto_tracet build_trace(const irep_idt &) const override;
45  goto_tracet build_shortest_trace() const override;
46  const namespacet &get_namespace() const override;
47 
48  void output_error_witness(const goto_tracet &) override;
49  void output_proof() override;
50 
51 protected:
56  path_fifot path_storage; // should go away
63 };
64 
65 #endif // CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
single_loop_incremental_symex_checkert::operator()
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
Definition: single_loop_incremental_symex_checker.cpp:68
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
single_loop_incremental_symex_checkert::symex_symbol_table
symbol_tablet symex_symbol_table
Definition: single_loop_incremental_symex_checker.h:53
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
single_loop_incremental_symex_checkert
Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and...
Definition: single_loop_incremental_symex_checker.h:30
ui_message_handlert
Definition: ui_message.h:20
incremental_goto_checkert::resultt
Definition: incremental_goto_checker.h:41
symex_bmc_incremental_one_loopt
Definition: symex_bmc_incremental_one_loop.h:16
path_fifot
FIFO save queue: paths are resumed in the order that they were saved.
Definition: path_storage.h:184
optionst
Definition: options.h:23
incremental_goto_checkert::options
const optionst & options
Definition: incremental_goto_checker.h:89
symex_bmc_incremental_one_loop.h
single_loop_incremental_symex_checkert::output_error_witness
void output_error_witness(const goto_tracet &) override
Definition: single_loop_incremental_symex_checker.cpp:243
goto_symex_property_decider.h
Property Decider for Goto-Symex.
single_loop_incremental_symex_checkert::path_storage
path_fifot path_storage
Definition: single_loop_incremental_symex_checker.h:56
goto_trace_providert
An implementation of incremental_goto_checkert may implement this interface to provide goto traces.
Definition: goto_trace_provider.h:23
goto_trace_provider.h
Interface for returning Goto Traces from Goto Checkers.
single_loop_incremental_symex_checkert::current_equation_converted
bool current_equation_converted
Definition: single_loop_incremental_symex_checker.h:61
single_loop_incremental_symex_checkert::guard_manager
guard_managert guard_manager
Definition: single_loop_incremental_symex_checker.h:57
incremental_goto_checker.h
Incremental Goto Checker Interface.
single_loop_incremental_symex_checkert::build_full_trace
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
Definition: single_loop_incremental_symex_checker.cpp:189
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
single_loop_incremental_symex_checkert::ns
namespacet ns
Definition: single_loop_incremental_symex_checker.h:54
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
single_loop_incremental_symex_checkert::initial_equation_generated
bool initial_equation_generated
Definition: single_loop_incremental_symex_checker.h:59
single_loop_incremental_symex_checkert::output_proof
void output_proof() override
Definition: single_loop_incremental_symex_checker.cpp:238
single_loop_incremental_symex_checkert::equation
symex_target_equationt equation
Definition: single_loop_incremental_symex_checker.h:55
single_loop_incremental_symex_checkert::build_trace
goto_tracet build_trace(const irep_idt &) const override
Builds and returns the trace for the FAILed property with the given property_id.
Definition: single_loop_incremental_symex_checker.cpp:219
single_loop_incremental_symex_checkert::symex
symex_bmc_incremental_one_loopt symex
Definition: single_loop_incremental_symex_checker.h:58
witness_provider.h
Interface for outputting GraphML Witnesses for Goto Checkers.
single_loop_incremental_symex_checkert::full_equation_generated
bool full_equation_generated
Definition: single_loop_incremental_symex_checker.h:60
single_loop_incremental_symex_checkert::get_namespace
const namespacet & get_namespace() const override
Returns the namespace associated with the traces.
Definition: single_loop_incremental_symex_checker.cpp:233
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
incremental_goto_checkert
An implementation of incremental_goto_checkert provides functionality for checking a set of propertie...
Definition: incremental_goto_checker.h:34
single_loop_incremental_symex_checkert::build_shortest_trace
goto_tracet build_shortest_trace() const override
Builds and returns the trace up to the first failed property.
Definition: single_loop_incremental_symex_checker.cpp:202
single_loop_incremental_symex_checkert::goto_model
abstract_goto_modelt & goto_model
Definition: single_loop_incremental_symex_checker.h:52
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
goto_symex_property_decidert
Provides management of goal variables that encode properties.
Definition: goto_symex_property_decider.h:24
witness_providert
An implementation of incremental_goto_checkert may implement this interface to provide GraphML witnes...
Definition: witness_provider.h:20
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
incremental_goto_checkert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: incremental_goto_checker.h:90
single_loop_incremental_symex_checkert::property_decider
goto_symex_property_decidert property_decider
Definition: single_loop_incremental_symex_checker.h:62
single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert
single_loop_incremental_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Definition: single_loop_incremental_symex_checker.cpp:23