cprover
multi_path_symex_only_checker.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Multi-Path Symbolic Execution only
4 
5 Author: 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 
17 #include "symex_bmc.h"
18 
20 {
21 public:
23  const optionst &options,
26 
27  resultt operator()(propertiest &) override;
28 
29 protected:
35  path_fifot path_storage; // should go away
37 
39  virtual void generate_equation();
40 
43  virtual void update_properties(
44  propertiest &properties,
45  std::unordered_set<irep_idt> &updated_properties);
46 };
47 
48 #endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
multi_path_symex_only_checkert::symex_symbol_table
symbol_tablet symex_symbol_table
Definition: multi_path_symex_only_checker.h:31
ui_message_handlert
Definition: ui_message.h:20
incremental_goto_checkert::resultt
Definition: incremental_goto_checker.h:41
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
multi_path_symex_only_checkert::multi_path_symex_only_checkert
multi_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Definition: multi_path_symex_only_checker.cpp:22
multi_path_symex_only_checkert::equation
symex_target_equationt equation
Definition: multi_path_symex_only_checker.h:33
incremental_goto_checker.h
Incremental Goto Checker Interface.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
multi_path_symex_only_checkert::symex
symex_bmct symex
Definition: multi_path_symex_only_checker.h:36
multi_path_symex_only_checkert::ns
namespacet ns
Definition: multi_path_symex_only_checker.h:32
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
multi_path_symex_only_checkert::guard_manager
guard_managert guard_manager
Definition: multi_path_symex_only_checker.h:34
multi_path_symex_only_checkert
Definition: multi_path_symex_only_checker.h:20
multi_path_symex_only_checkert::path_storage
path_fifot path_storage
Definition: multi_path_symex_only_checker.h:35
multi_path_symex_only_checkert::goto_model
abstract_goto_modelt & goto_model
Definition: multi_path_symex_only_checker.h:30
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
multi_path_symex_only_checkert::update_properties
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.
Definition: multi_path_symex_only_checker.cpp:79
incremental_goto_checkert
An implementation of incremental_goto_checkert provides functionality for checking a set of propertie...
Definition: incremental_goto_checker.h:34
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
symex_bmct
Definition: symex_bmc.h:26
incremental_goto_checkert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: incremental_goto_checker.h:90
symex_bmc.h
Bounded Model Checking for ANSI-C.
multi_path_symex_only_checkert::operator()
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
Definition: multi_path_symex_only_checker.cpp:42
multi_path_symex_only_checkert::generate_equation
virtual void generate_equation()
Generates the equation by running goto-symex.
Definition: multi_path_symex_only_checker.cpp:72