|
CBMC
|
#include <chrono>#include "goto_symex_property_decider.h"#include "goto_trace_provider.h"#include "single_path_symex_only_checker.h"#include "witness_provider.h"
Include dependency graph for single_path_symex_checker.h:
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | single_path_symex_checkert |
| Uses goto-symex to symbolically execute each path in the goto model and calls a solver to find property violations. More... | |
Goto Checker using Single Path Symbolic Execution
Definition in file single_path_symex_checker.h.