All Packages
Package Summary
Package
Description
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.
Module analysis provides a list of analyzers for static/runtime analyzing of a program.
Module config provides static configurations of the CIVL tool.
Module dynamic provides general computations of symbolic expressions,
including the pretty printing method.
Module kripke provides the definition of various
transitions and the enabler and state manager of CIVL.
Module log provides the data structure for logging errors during verification.
Module model defines a static model, i.e., the control flow graph, representation of a CIVL-C program.
Submodule model.expression defines expression in CIVL.
Submodule model.location defines a location in the control flow graph of CIVL.
Submodule model.statement defines a statement of a CIVL-C program.
Submodule model.type defines types in CIVL.
Submodule model.variable defines variables in CIVL.
Module predicate defines predicates that are required to hold for any CIVL-C programs.
Module run parses command line inputs and initializes the tool.
Module semantics implements the semantics of CIVL-C.
Module state is responsible for the creation and manipulation of
states of a CIVL model.
Module transform defines various kinds of
transformations of an AST into a CIVL AST.
Module util provides various general-purpose utilities used by
CIVL.