goto-symex Directory Reference

Directory dependency graph for goto-symex:

Files
	auto_objects.cpp
	Symbolic Execution of ANSI-C.
	build_goto_trace.cpp
	Traces of GOTO Programs.
	build_goto_trace.h
	Traces of GOTO Programs.
	call_stack.h
	complexity_limiter.cpp
	complexity_limiter.h
	Symbolic Execution.
	complexity_violation.h
	expr_skeleton.cpp
	Expression skeleton.
	expr_skeleton.h
	Expression skeleton.
	field_sensitivity.cpp
	field_sensitivity.h
	frame.h
	Class for stack frames.
	goto_state.cpp
	goto_state.h
	goto_statet class definition
	goto_symex.cpp
	Symbolic Execution.
	goto_symex.h
	Symbolic Execution.
	goto_symex_can_forward_propagate.h
	GOTO Symex constant propagation.
	goto_symex_state.cpp
	Symbolic Execution.
	goto_symex_state.h
	Symbolic Execution.
	memory_model.cpp
	Memory model for partial order concurrency.
	memory_model.h
	Memory models for partial order concurrency.
	memory_model_pso.cpp
	Memory model for partial order concurrency.
	memory_model_pso.h
	Memory models for partial order concurrency.
	memory_model_sc.cpp
	Memory model for partial order concurrency.
	memory_model_sc.h
	Memory models for partial order concurrency.
	memory_model_tso.cpp
	Memory model for partial order concurrency.
	memory_model_tso.h
	Memory models for partial order concurrency.
	partial_order_concurrency.cpp
	Add constraints to equation encoding partial orders on events.
	partial_order_concurrency.h
	Add constraints to equation encoding partial orders on events.
	path_storage.cpp
	path_storage.h
	Storage of symbolic execution paths to resume.
	postcondition.cpp
	Symbolic Execution.
	postcondition.h
	Generate Equation using Symbolic Execution.
	precondition.cpp
	Symbolic Execution.
	precondition.h
	Generate Equation using Symbolic Execution.
	renamed.h
	Class for expressions or types renamed up to a given level.
	renaming_level.cpp
	Renaming levels.
	renaming_level.h
	Renaming levels.
	shadow_memory.cpp
	Symex Shadow Memory Instrumentation.
	shadow_memory.h
	Symex Shadow Memory Instrumentation.
	shadow_memory_field_definitions.h
	Symex Shadow Memory Field Definitions.
	shadow_memory_state.h
	Symex Shadow Memory Instrumentation State.
	shadow_memory_util.cpp
	Symex Shadow Memory Instrumentation Utilities.
	shadow_memory_util.h
	Symex Shadow Memory Instrumentation Utilities.
	show_program.cpp
	Output of the program (SSA) constraints.
	show_program.h
	Output of the program (SSA) constraints.
	show_vcc.cpp
	Output of the verification conditions (VCCs)
	show_vcc.h
	Output of the verification conditions (VCCs)
	simplify_expr_with_value_set.cpp
	simplify_expr_with_value_set.h
	slice.cpp
	Slicer for symex traces.
	slice.h
	Slicer for symex traces.
	solver_hardness.cpp
	solver_hardness.h
	ssa_step.cpp
	ssa_step.h
	symex_assign.cpp
	Symbolic Execution.
	symex_assign.h
	Symbolic Execution of assignments.
	symex_atomic_section.cpp
	Symbolic Execution.
	symex_builtin_functions.cpp
	Symbolic Execution of ANSI-C.
	symex_catch.cpp
	Symbolic Execution.
	symex_clean_expr.cpp
	Symbolic Execution of ANSI-C.
	symex_complexity_limit_exceeded_action.h
	symex_config.h
	Symbolic Execution.
	symex_dead.cpp
	Symbolic Execution.
	symex_decl.cpp
	Symbolic Execution.
	symex_dereference.cpp
	Symbolic Execution of ANSI-C.
	symex_dereference_state.cpp
	Symbolic Execution of ANSI-C.
	symex_dereference_state.h
	Symbolic Execution of ANSI-C.
	symex_function_call.cpp
	Symbolic Execution of ANSI-C.
	symex_goto.cpp
	Symbolic Execution.
	symex_main.cpp
	Symbolic Execution.
	symex_other.cpp
	Symbolic Execution.
	symex_set_return_value.cpp
	Symbolic Execution of ANSI-C.
	symex_slice_class.h
	Slicer for symex traces.
	symex_start_thread.cpp
	Symbolic Execution.
	symex_target.cpp
	Symbolic Execution.
	symex_target.h
	Generate Equation using Symbolic Execution.
	symex_target_equation.cpp
	Symbolic Execution Implementation of functions to build SSA equation.
	symex_target_equation.h
	Generate Equation using Symbolic Execution.
	symex_throw.cpp
	Symbolic Execution.