| edu.udel.cis.vsl.civl |
The main package for CIVL, providing a command line interface and a
class "CIVL" that invokes all the components in the CIVL tool chain
to perform requested tasks.
|
| edu.udel.cis.vsl.civl.analysis.IF |
Module analysis provides a list of analyzers for static/runtime analyzing of a program.
|
| edu.udel.cis.vsl.civl.config.IF |
Module config provides static configurations of the CIVL tool.
|
| edu.udel.cis.vsl.civl.dynamic.IF |
Module dynamic provides general computations of symbolic expressions,
including the pretty printing method.
|
| edu.udel.cis.vsl.civl.kripke.IF |
Module kripke provides the definition of various
transitions and the enabler and state manager of CIVL.
|
| edu.udel.cis.vsl.civl.log.IF |
Module log provides the data structure for logging errors during verification.
|
| edu.udel.cis.vsl.civl.model.IF |
Module model defines a static model, i.e., the control flow graph, representation of a CIVL-C program.
|
| edu.udel.cis.vsl.civl.model.IF.contract |
|
| edu.udel.cis.vsl.civl.model.IF.expression |
Submodule model.expression defines expression in CIVL.
|
| edu.udel.cis.vsl.civl.model.IF.expression.reference |
|
| edu.udel.cis.vsl.civl.model.IF.location |
Submodule model.location defines a location in the control flow graph of CIVL.
|
| edu.udel.cis.vsl.civl.model.IF.statement |
Submodule model.statement defines a statement of a CIVL-C program.
|
| edu.udel.cis.vsl.civl.model.IF.type |
Submodule model.type defines types in CIVL.
|
| edu.udel.cis.vsl.civl.model.IF.variable |
Submodule model.variable defines variables in CIVL.
|
| edu.udel.cis.vsl.civl.predicate.IF |
Module predicate defines predicates that are required to hold for any CIVL-C programs.
|
| edu.udel.cis.vsl.civl.run.IF |
Module run parses command line inputs and initializes the tool.
|
| edu.udel.cis.vsl.civl.semantics.IF |
Module semantics implements the semantics of CIVL-C.
|
| edu.udel.cis.vsl.civl.slice.IF |
|
| edu.udel.cis.vsl.civl.state.IF |
Module state is responsible for the creation and manipulation of
states of a CIVL model.
|
| edu.udel.cis.vsl.civl.transform.IF |
Module transform defines various kinds of
transformations of an AST into a CIVL AST.
|
| edu.udel.cis.vsl.civl.util.IF |
Module util provides various general-purpose utilities used by
CIVL.
|