cprover
Loading...
Searching...
No Matches
multi_path_symex_only_checker.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Checker using Multi-Path Symbolic Execution only
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H
13#define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H
14
16
18
20
21#include "symex_bmc.h"
22
52
53#endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H
Abstract interface to eager or lazy GOTO models.
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...
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...
Definition namespace.h:94
FIFO save queue: paths are resumed in the order that they were saved.
The symbol table.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
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
Bounded Model Checking for ANSI-C.
Loop unwinding.