single_loop_incremental_symex_checker.h File Reference

Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop. More...

#include <goto-symex/path_storage.h>
#include <goto-instrument/unwindset.h>
#include "goto_symex_property_decider.h"
#include "goto_trace_provider.h"
#include "incremental_goto_checker.h"
#include "symex_bmc_incremental_one_loop.h"
#include "witness_provider.h"

Include dependency graph for single_loop_incremental_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_loop_incremental_symex_checkert
	Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and calls a SAT/SMT solver to check the status of the properties after each iteration. More...

Detailed Description

Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.

Definition in file single_loop_incremental_symex_checker.h.