bddExec.c
This module contains the function to support BDD basd trace re-execution
satExec.c
This module contains the functions to support SAT basd trace re-execution
traceExec.c
This module contains the functions needed to support trace re-execution
TraceExecInfo.c
Implementation of class 'TraceExecInfo'

bddExec.c

This module contains the function to support BDD basd trace re-execution

By: Marco Pensallorto

optional

See Alsooptional

trace_bdd_execute_trace()
Executes a trace on the given fsm using BDDs
trace_bdd_execute_partial_trace()
Executes a trace on the given fsm using BDDs
extract_bdd_trace()
Extracts a complete trace Description [This function is a private service of trace_bdd_execute_partial_trace

satExec.c

This module contains the functions to support SAT basd trace re-execution

By: Marco Pensallorto

optional

See Alsooptional

trace_sat_execute_trace()
Executes a trace on the given fsm using SAT solver
trace_exec_get_initial_state()
Builds the initial state formula
trace_exec_get_transition_relation()
Builds the transition relation formula
bmc_add_be_into_solver()
Converts Be into CNF, and adds it into a group of a solver.
bmc_add_be_into_solver_positively()
Converts Be into CNF, and adds it into a group of a solver, sets polarity to 1, and then destroys the CNF.

traceExec.c

This module contains the functions needed to support trace re-execution

By: Marco Pensallorto

This module contains the functions needed to support trace re-execution

TracePkg_execution_engine_from_string()
Converts an engine name into an engine identifier
Trace_execute_trace()
Complete trace re-execution
Trace_execute_partial_trace()
Partial trace re-execution and fill-in

TraceExecInfo.c

Implementation of class 'TraceExecInfo'

By: Alessandro Mariotti, Marco Pensallorto

See AlsoTraceExecInfo.h


Last updated on 2010/05/19 22h:26