cprover
Loading...
Searching...
No Matches
single_loop_incremental_symex_checker.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Checker using Multi-Path Symbolic Execution
4 with Incremental Unwinding of a specified Loop
5
6Author: 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
20
22#include "goto_trace_provider.h"
25#include "witness_provider.h"
26
69
70#endif // 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.
Trace of a GOTO program.
Definition goto_trace.h:177
ui_message_handlert & ui_message_handler
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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.
goto_tracet build_shortest_trace() const override
Builds and returns the trace up to the first failed property.
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
single_loop_incremental_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
const namespacet & get_namespace() const override
Returns the namespace associated with the traces.
The 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
Definition guard.h:28
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.
Definition properties.h:76
Loop unwinding.
dstringt irep_idt
Interface for outputting GraphML Witnesses for Goto Checkers.