Module dev.civl.mc
Package dev.civl.mc.semantics.IF
package dev.civl.mc.semantics.IF
Module semantics implements the semantics of CIVL-C.
-
ClassDescriptionThis interface provides methods for dealing with array slices, e.g.This class provides methods for reshaping arrays.This interface provides a collection of methods that manipulating symbolic expressions whose symbolic type has ARRAY kind.The data structure for describing array shapes, including dimensions, extent for each dimension and slice size for each sub-array with lower dimension.the data structure for describing array slices.Represents the result of evaluating an expression in two parts: the (possibly) new state resulting from side-effects arising from the evaluation, and the value resulting from the evaluation.This is the CIVL main evaluator.A Library Evaluator provides a method to "evaluate" the guard of each system function call.The library evaluator loader provides the mechanism for loading the library evaluator of a certain library.A Library Executor provides the semantics for system functions defined in a library.The library executor loader provides the mechanism for loading the library executor of a certain library.A library loader exception is produced by errors occur during when a library executor/evaluator/enabler loader attempts to load a specific library executor/evaluator/enabler.Entry point of the module civl.semantics.This class provides methods dealing with symbolic expressions and states, which represent some common-used operations like obtaining a sub-array from a given array, etc.This represents a CIVL transition, which is deterministic and enabled at a certain state.Represents the result of evaluating something that returns a symbolic type, but in two parts: the (possibly) new state resulting from side-effects arising from the evaluation, and the symbolic type resulting from the evaluation.