Module dev.civl.mc

module dev.civl.mc

Packages

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

Indirect Exports

From

Packages

antlr3runtime

org.antlr.runtime org.antlr.runtime.debug org.antlr.runtime.misc org.antlr.runtime.tree

antlr4runtime

org.antlr.v4.runtime org.antlr.v4.runtime.atn org.antlr.v4.runtime.dfa org.antlr.v4.runtime.misc org.antlr.v4.runtime.tree org.antlr.v4.runtime.tree.pattern

dev.civl.abc

dev.civl.abc.analysis.IF dev.civl.abc.analysis.pointsTo.IF dev.civl.abc.ast.conversion.IF dev.civl.abc.ast.entity.IF dev.civl.abc.ast.IF dev.civl.abc.ast.node.common.acsl dev.civl.abc.ast.node.common.expression dev.civl.abc.ast.node.IF dev.civl.abc.ast.node.IF.acsl dev.civl.abc.ast.node.IF.compound dev.civl.abc.ast.node.IF.declaration dev.civl.abc.ast.node.IF.expression dev.civl.abc.ast.node.IF.label dev.civl.abc.ast.node.IF.omp dev.civl.abc.ast.node.IF.statement dev.civl.abc.ast.node.IF.type dev.civl.abc.ast.type.common dev.civl.abc.ast.type.IF dev.civl.abc.ast.util dev.civl.abc.ast.value.IF dev.civl.abc.config.IF dev.civl.abc.err.IF dev.civl.abc.front.c.parse dev.civl.abc.front.c.preproc dev.civl.abc.front.IF dev.civl.abc.main dev.civl.abc.program.IF dev.civl.abc.token.IF dev.civl.abc.transform.common dev.civl.abc.transform.IF dev.civl.abc.util.IF

dev.civl.gmc

dev.civl.gmc dev.civl.gmc.seq

dev.civl.sarl

dev.civl.sarl dev.civl.sarl.expr.cnf dev.civl.sarl.expr.IF dev.civl.sarl.ideal.IF dev.civl.sarl.IF dev.civl.sarl.IF.config dev.civl.sarl.IF.expr dev.civl.sarl.IF.expr.valueSetReference dev.civl.sarl.IF.number dev.civl.sarl.IF.object dev.civl.sarl.IF.type dev.civl.sarl.number.IF dev.civl.sarl.object.common dev.civl.sarl.object.IF dev.civl.sarl.preuniverse.IF dev.civl.sarl.prove.IF dev.civl.sarl.prove.z3 dev.civl.sarl.simplify.IF dev.civl.sarl.type.IF dev.civl.sarl.util

java.base

com.sun.crypto.provider com.sun.security.ntlm java.io java.lang java.lang.annotation java.lang.constant java.lang.invoke java.lang.module java.lang.ref java.lang.reflect java.lang.runtime java.math java.net java.net.spi java.nio java.nio.channels java.nio.channels.spi java.nio.charset java.nio.charset.spi java.nio.file java.nio.file.attribute java.nio.file.spi java.security java.security.cert java.security.interfaces java.security.spec java.text java.text.spi java.time java.time.chrono java.time.format java.time.temporal java.time.zone java.util java.util.concurrent java.util.concurrent.atomic java.util.concurrent.locks java.util.function java.util.jar java.util.random java.util.regex java.util.spi java.util.stream java.util.zip javax.crypto javax.crypto.interfaces javax.crypto.spec javax.net javax.net.ssl javax.security.auth javax.security.auth.callback javax.security.auth.login javax.security.auth.spi javax.security.auth.x500 javax.security.cert jdk.internal.access jdk.internal.access.foreign jdk.internal.event jdk.internal.invoke jdk.internal.javac jdk.internal.jimage jdk.internal.jimage.decompressor jdk.internal.jmod jdk.internal.loader jdk.internal.logger jdk.internal.misc jdk.internal.module jdk.internal.org.objectweb.asm jdk.internal.org.objectweb.asm.commons jdk.internal.org.objectweb.asm.tree jdk.internal.org.objectweb.asm.util jdk.internal.org.xml.sax jdk.internal.org.xml.sax.helpers jdk.internal.perf jdk.internal.platform jdk.internal.ref jdk.internal.reflect jdk.internal.util jdk.internal.util.jar jdk.internal.util.random jdk.internal.util.xml jdk.internal.util.xml.impl jdk.internal.vm jdk.internal.vm.annotation jdk.internal.vm.vector sun.invoke.util sun.net sun.net.dns sun.net.ext sun.net.util sun.net.www sun.net.www.protocol.http sun.nio.ch sun.nio.cs sun.nio.fs sun.reflect.annotation sun.reflect.generics.reflectiveObjects sun.reflect.misc sun.security.action sun.security.internal.interfaces sun.security.internal.spec sun.security.jca sun.security.pkcs sun.security.provider sun.security.provider.certpath sun.security.rsa sun.security.timestamp sun.security.tools sun.security.util sun.security.util.math sun.security.util.math.intpoly sun.security.validator sun.security.x509 sun.util.cldr sun.util.locale.provider sun.util.logging sun.util.resources

Indirect Opens

From

Packages

dev.civl.abc

dev.civl.abc.include dev.civl.abc.include.sys

Modules

Requires

Modifier

Module

Description

antlr3runtime

antlr4runtime

dev.civl.abc

dev.civl.gmc

dev.civl.sarl

java.base