Uses of Class
dev.civl.mc.config.IF.CIVLConfiguration

Packages that use CIVLConfiguration

Package	Description
dev.civl.mc.analysis.IF	Module analysis provides a list of analyzers for static/runtime analyzing of a program.
dev.civl.mc.config.IF	Module config provides static configurations of the CIVL tool.
dev.civl.mc.kripke.IF	Module kripke provides the definition of various transitions and the enabler and state manager of CIVL.
dev.civl.mc.log.IF	Module log provides the data structure for logging errors during verification.
dev.civl.mc.model.IF	Module model defines a static model, i.e., the control flow graph, representation of a CIVL-C program.
dev.civl.mc.semantics.IF	Module semantics implements the semantics of CIVL-C.
dev.civl.mc.state.IF	Module state is responsible for the creation and manipulation of states of a CIVL model.
dev.civl.mc.transform.IF	Module transform defines various kinds of transformations of an AST into a CIVL AST.

Uses of CIVLConfiguration in dev.civl.mc.analysis.IF

Methods in dev.civl.mc.analysis.IF with parameters of type CIVLConfiguration

Modifier and Type	Method	Description
static List<CodeAnalyzer>	Analysis.getAnalyzers(CIVLConfiguration config, dev.civl.sarl.IF.SymbolicUniverse universe)	gets all code analyzers as required in the configuration.

Uses of CIVLConfiguration in dev.civl.mc.config.IF

Constructors in dev.civl.mc.config.IF with parameters of type CIVLConfiguration

Modifier	Constructor	Description
	CIVLConfiguration(CIVLConfiguration config)

Uses of CIVLConfiguration in dev.civl.mc.kripke.IF

Methods in dev.civl.mc.kripke.IF with parameters of type CIVLConfiguration

Modifier and Type	Method	Description
static Enabler	Kripkes.newEnabler(StateFactory stateFactory, Evaluator evaluator, Executor executor, SymbolicAnalyzer symbolicAnalyzer, MemoryUnitFactory memUnitFactory, LibraryEnablerLoader libLoader, CIVLErrorLogger errorLogger, CIVLConfiguration civlConfig, dev.civl.gmc.GMCConfiguration gmcConfig)	Creates a new instance of enabler.
static LibraryEnablerLoader	Kripkes.newLibraryEnablerLoader(LibraryEvaluatorLoader libEvaluatorLoader, CIVLConfiguration civlConfig)	Creates a new instance of library enabler loader.
static CIVLStateManager	Kripkes.newStateManager(Enabler enabler, Executor executor, SymbolicAnalyzer symbolicAnalyzer, CIVLErrorLogger errorLogger, CIVLConfiguration config)	Creates a new instance of state manager.

Uses of CIVLConfiguration in dev.civl.mc.log.IF

Constructors in dev.civl.mc.log.IF with parameters of type CIVLConfiguration

Modifier	Constructor	Description
	CIVLErrorLogger(File directory, String sessionName, PrintStream out, CIVLConfiguration civlConfig, dev.civl.gmc.GMCConfiguration gmcConfig, StateFactory stateFactory, dev.civl.sarl.IF.SymbolicUniverse universe, boolean solve)	creates a new instance of error logger.
	CIVLLogEntry(CIVLConfiguration civlConfig, dev.civl.gmc.GMCConfiguration gmcConfig, CIVLExecutionException problem, dev.civl.sarl.IF.SymbolicUniverse universe)

Uses of CIVLConfiguration in dev.civl.mc.model.IF

Methods in dev.civl.mc.model.IF with parameters of type CIVLConfiguration

Modifier and Type	Method	Description
static ModelBuilder	Models.newModelBuilder(dev.civl.sarl.IF.SymbolicUniverse universe, CIVLConfiguration config)	Creates a new instance of model builder.

Uses of CIVLConfiguration in dev.civl.mc.semantics.IF

Methods in dev.civl.mc.semantics.IF with parameters of type CIVLConfiguration

Modifier and Type	Method	Description
static Evaluator	Semantics.newErrorSideEffectFreeEvaluator(ModelFactory modelFactory, StateFactory stateFactory, LibraryEvaluatorLoader loader, LibraryExecutorLoader loaderExec, SymbolicUtility symbolicUtil, SymbolicAnalyzer symbolicAnalyzer, MemoryUnitFactory memUnitFactory, CIVLErrorLogger errLogger, CIVLConfiguration config)	Creates a new instance of ErrorSideEffectFreeEvaluator.
static Evaluator	Semantics.newEvaluator(ModelFactory modelFactory, StateFactory stateFactory, LibraryEvaluatorLoader loader, LibraryExecutorLoader loaderExec, SymbolicUtility symbolicUtil, SymbolicAnalyzer symbolicAnalyzer, MemoryUnitFactory memUnitFactory, CIVLErrorLogger errLogger, CIVLConfiguration config)	Creates a new instance of CIVL evaluator.
static Executor	Semantics.newExecutor(ModelFactory modelFactory, StateFactory stateFactory, LibraryExecutorLoader loader, Evaluator evaluator, SymbolicAnalyzer symbolicAnalyzer, CIVLErrorLogger errLogger, CIVLConfiguration civlConfig)	Creates a new instance of CIVL executor.
static LibraryEvaluatorLoader	Semantics.newLibraryEvaluatorLoader(CIVLConfiguration civlConfig)	Creates a new instance of library evaluator loader.
static LibraryExecutorLoader	Semantics.newLibraryExecutorLoader(LibraryEvaluatorLoader libEvaluatorLoader, CIVLConfiguration civlConfig)	Creates a new instance of library executor loader.
static SymbolicAnalyzer	Semantics.newSymbolicAnalyzer(CIVLConfiguration civlConfig, CIVLErrorLogger errorLogger, dev.civl.sarl.IF.SymbolicUniverse universe, ModelFactory modelFactory, SymbolicUtility symbolicUtil)	Creates a new instance of symbolic analyzer.
void	Evaluator.setConfiguration(CIVLConfiguration config)
void	Executor.setConfiguration(CIVLConfiguration config)

Uses of CIVLConfiguration in dev.civl.mc.state.IF

Methods in dev.civl.mc.state.IF with parameters of type CIVLConfiguration

Modifier and Type	Method	Description
static StateFactory	States.newImmutableStateFactory(ModelFactory modelFactory, MemoryUnitFactory memFactory, CIVLConfiguration config)	Returns a new immutable state factory based on the given model factory.
void	StateFactory.setConfiguration(CIVLConfiguration config)

Uses of CIVLConfiguration in dev.civl.mc.transform.IF

Methods in dev.civl.mc.transform.IF with parameters of type CIVLConfiguration

Modifier and Type	Method	Description
dev.civl.abc.transform.IF.TransformRecord	TransformerFactory.getContractTransformerRecord(String targetFunction, CIVLConfiguration civlConfig)
dev.civl.abc.transform.IF.TransformRecord	TransformerFactory.getIntOperationTransformerRecord(Map<String,String> macros, CIVLConfiguration config)
dev.civl.abc.transform.IF.TransformRecord	TransformerFactory.getIOTransformerRecord(CIVLConfiguration config)
dev.civl.abc.transform.IF.TransformRecord	TransformerFactory.getLoopContractTransformerRecord(CIVLConfiguration civlConfig)
dev.civl.abc.transform.IF.Transformer	TransformerFactory.getOpenMP2CIVLTransformer(CIVLConfiguration config)
dev.civl.abc.transform.IF.TransformRecord	TransformerFactory.getOpenMP2CIVLTransformerRecord(CIVLConfiguration config)
dev.civl.abc.transform.IF.Transformer	TransformerFactory.getOpenMPSimplifier(CIVLConfiguration config)
dev.civl.abc.transform.IF.TransformRecord	TransformerFactory.getOpenMPSimplifierRecord(CIVLConfiguration config)
dev.civl.abc.transform.IF.TransformRecord	TransformerFactory.getShortCircuitTransformerRecord(CIVLConfiguration config)	Creates a new instance of a ShortCircuitTransformer

Constructors in dev.civl.mc.transform.IF with parameters of type CIVLConfiguration

Modifier	Constructor	Description
	ContractTransformer(dev.civl.abc.ast.IF.ASTFactory astFactory, String targetFunction, CIVLConfiguration civlConfig)
	IntOperationTransformer(dev.civl.abc.ast.IF.ASTFactory astFactory, Map<String,String> macros, CIVLConfiguration config)
	IOTransformer(dev.civl.abc.ast.IF.ASTFactory astFactory, CIVLConfiguration config)	Creates a new instance of IO transformer.
protected	LoopContractTransformer(dev.civl.abc.ast.IF.ASTFactory astFactory, CIVLConfiguration civlConfig)
	OpenMP2CIVLTransformer(dev.civl.abc.ast.IF.ASTFactory astFactory, CIVLConfiguration config)	Creates a new instance of OpenMP2CIVLTransformer.
	OpenMPSimplifier(dev.civl.abc.ast.IF.ASTFactory astFactory, CIVLConfiguration config)