Uses of Interface
dev.civl.mc.model.IF.type.CIVLType

Packages that use CIVLType

Package	Description
dev.civl.mc.dynamic.IF	Module dynamic provides general computations of symbolic expressions, including the pretty printing method.
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.model.IF.expression	Submodule model.expression defines expression in CIVL.
dev.civl.mc.model.IF.statement	Submodule model.statement defines a statement of a CIVL-C program.
dev.civl.mc.model.IF.type	Submodule model.type defines types in CIVL.
dev.civl.mc.model.IF.variable	Submodule model.variable defines variables in CIVL.
dev.civl.mc.semantics.IF	Module semantics implements the semantics of CIVL-C.

Uses of CIVLType in dev.civl.mc.dynamic.IF

Methods in dev.civl.mc.dynamic.IF with parameters of type CIVLType

Modifier and Type	Method	Description
dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference	ValueSetUtility.getVSReferenceToSequenceOrNoop(CIVLType variableOrMallocElementType, boolean isMallocElementType, dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference vsRef)	This method over-approximates vsRef if it references into sequence elements.

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

Methods in dev.civl.mc.model.IF that return CIVLType

Modifier and Type	Method	Description
CIVLType	CIVLTypeFactory.getStaticTypeOfDynamicType(dev.civl.sarl.IF.expr.SymbolicExpression typeId)	Given a symbolic expression returned by the method CIVLTypeFactory.expressionOfType(dev.civl.mc.model.IF.type.CIVLType, dev.civl.sarl.IF.type.SymbolicType), this returns the CIVLType which is associated to the dynamic type that was used to create the given expression.
CIVLType	Model.mesageType()
CIVLType	Model.queueType()
CIVLType	CIVLTypeFactory.rangeType()	Returns the range type of the system.
CIVLType	CIVLFunction.returnType()
CIVLType	CIVLTypeFactory.systemType(String name)	Obtains the CIVL type by the given name.

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

Modifier and Type	Method	Description
AbstractFunction	ModelFactory.abstractFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, int continuity, String attribute)	Generate an abstract function.
void	CIVLTypeFactory.addHeapFieldObjectType(CIVLType type, int id)	Add the given type as the object type of one of the heap field.
void	CIVLTypeFactory.addSystemType(String name, CIVLType type)	Added a type in map of system type, which is the map of types of system libraries, e.g., $gcomm/$comm for comm, $file for stdio, $gbarrier/$barrier for concurrency, etc.
BoundVariableExpression	ModelFactory.boundVariableExpression(CIVLSource source, Identifier name, CIVLType type)	An expression for a bound variable.
CastExpression	ModelFactory.castExpression(CIVLSource source, CIVLType type, Expression expression)	Create a cast expression
CIVLSetType	CIVLTypeFactory.civlSetType(CIVLType elementType)	Returns the CIVLSetType.
CIVLCompleteArrayType	CIVLTypeFactory.completeArrayType(CIVLType elementType, Expression extent)	Returns a new complete array type with specified extent (length expression) and element type.
CIVLCompleteDomainType	CIVLTypeFactory.completeDomainType(CIVLType rangeType, int dim)	Creates a complete regular domain type, which is has the given dimension and is composed by the given range type.
CompoundLiteralExpression	ModelFactory.compoundLiteralExpression(CIVLSource source, Scope exprScope, CIVLType type, boolean isStringLiteral)	Creates a new instance of a compound literal expression.
CIVLDomainType	CIVLTypeFactory.domainType(CIVLType rangeType)	This returns the universal domain type ($domain).
DynamicTypeOfExpression	ModelFactory.dynamicTypeOfExpression(CIVLSource source, CIVLType type)	Returns a "DynamicTypeOf" expression with the given type argument.
dev.civl.sarl.IF.expr.SymbolicExpression	CIVLTypeFactory.expressionOfType(CIVLType civlType, dev.civl.sarl.IF.type.SymbolicType type)	Given a symbolic type, returns a canonical symbolic expression which somehow wraps that type so it can be used as a value.
ExtendedQuantifiedExpression	ModelFactory.extendedQuantifiedExpression(CIVLSource source, CIVLType type, dev.civl.abc.ast.node.IF.acsl.ExtendedQuantifiedExpressionNode.ExtendedQuantifier quant, Expression lo, Expression hi, Expression function)
CIVLFunction	ModelFactory.function(CIVLSource source, boolean isAtomic, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, Location startLocation)	Create a new function.
CIVLFunctionType	CIVLTypeFactory.functionType(CIVLType returnType, CIVLType[] paraTypes)	Creates a new instance of function type, which contains a return type and a list of parameter types.
int	CIVLTypeFactory.getHeapFieldId(CIVLType type)	Returns the type of the heap field of the given index.
CIVLArrayType	CIVLTypeFactory.incompleteArrayType(CIVLType elementType)	Get a new incomplete array type.
LogicFunction	ModelFactory.logicFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType outputType, int[] pointerToHeapMap, Scope containingScope, Expression definition)	Create a new logic function (LogicFunction).
MallocStatement	ModelFactory.mallocStatement(CIVLSource civlSource, Location source, LHSExpression lhs, CIVLType staticElementType, Expression scopeExpression, Expression sizeExpression, int mallocId, Expression guard)	Create a new malloc statement
MemoryUnitExpression	ModelFactory.memoryUnitExpression(CIVLSource source, Variable variable, CIVLType objetType, MemoryUnitReference reference, boolean writable, boolean hasPinterRef)	creates a memory unit expression.
Variable	ModelFactory.newAnonymousVariable(CIVLSource sourceOf, Scope scope, CIVLType type)	Create a variable of the given type and add it to the given scope.
CIVLFunction	ModelFactory.nondetFunction(CIVLSource source, Identifier name, CIVLType returnType, Scope containingScope)
VariableExpression	ModelFactory.parProcsVariable(CIVLSource source, CIVLType type, Scope scope)
CIVLPointerType	CIVLTypeFactory.pointerType(CIVLType baseType)	Get a new pointer type.
RecDomainLiteralExpression	ModelFactory.recDomainLiteralExpression(CIVLSource source, List<Expression> ranges, CIVLType type)	Create a rectangular domain expression, which has the form {r1, r2, ..., rm}, where m is the dimension of the domain, and ri (where 1 invalid input: '<'= i invalid input: '<'= m) is a range expression (either regular range or literal range).
void	Model.setMessageType(CIVLType messageType)
void	CIVLFunction.setParameterTypes(CIVLType[] types)	updates the types of the parameters of this function
void	Model.setQueueType(CIVLType queueType)
void	CIVLFunction.setReturnType(CIVLType returnType)	updates the return type of this function
SizeofTypeExpression	ModelFactory.sizeofTypeExpression(CIVLSource source, CIVLType type)	Returns a new "sizeof(t)" expression.
StructOrUnionField	CIVLTypeFactory.structField(Identifier name, CIVLType type, int index, boolean isAnonymous, CIVLStructOrUnionType enclosingType)	Returns a new struct field, used to complete a struct type.
SystemFunction	ModelFactory.systemFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, String libraryName)	Generate the system function
Variable	ModelFactory.variable(CIVLSource source, CIVLType type, Identifier name, int vid)	Create a new variable.
Variable	ModelFactory.variableAsParameter(CIVLSource source, CIVLType type, Identifier name, int vid)	Create a new variable which is also a parameter of some function.
WildcardExpression	ModelFactory.wildcardExpression(CIVLSource source, CIVLType type)	Creates a wildcard expression ..., which is only used in contract.

Method parameters in dev.civl.mc.model.IF with type arguments of type CIVLType

Modifier and Type	Method	Description
void	CIVLTypeFactory.completeBundleType(CIVLBundleType bundleType, List<CIVLType> eleTypes, Collection<dev.civl.sarl.IF.type.SymbolicType> types)	Completes the bundle type by specifying the list of all dynamic types which can occur as bundle elements.

Uses of CIVLType in dev.civl.mc.model.IF.expression

Methods in dev.civl.mc.model.IF.expression that return CIVLType

Modifier and Type	Method	Description
CIVLType	CastExpression.getCastType()
CIVLType	Expression.getExpressionType()
CIVLType	DynamicTypeOfExpression.getType()
CIVLType	SizeofTypeExpression.getTypeArgument()	Returns the CIVL type, which is the sole argument of the sizeof operator.
CIVLType	AddressOfExpression.getTypeForOffset()
CIVLType	MemoryUnitExpression.objectType()
CIVLType	CompoundLiteralExpression.CIVLLiteralObject.type()
CIVLType	CompoundLiteralExpression.type()

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

Modifier and Type	Method	Description
CompoundLiteralExpression.CIVLCompoundLiteralObject	CompoundLiteralExpression.createCompoundLiteralObject(CIVLType type, List<CompoundLiteralExpression.CIVLLiteralObject> elements)
CompoundLiteralExpression.CIVLLiteralObject	CompoundLiteralExpression.createScalarLiteralObject(CIVLType type, Expression expr)
void	FunctionCallExpression.setExpressionType(CIVLType returnType)
void	AddressOfExpression.setTypeForOffset(CIVLType type)

Uses of CIVLType in dev.civl.mc.model.IF.statement

Methods in dev.civl.mc.model.IF.statement that return CIVLType

Modifier and Type	Method	Description
CIVLType	MallocStatement.getStaticElementType()	Returns the static type of the elements that are to be allocated.

Uses of CIVLType in dev.civl.mc.model.IF.type

Subinterfaces of CIVLType in dev.civl.mc.model.IF.type

Modifier and Type	Interface	Description
interface	CIVLArrayType	The type for an array of T.
interface	CIVLBundleType
interface	CIVLCompleteArrayType	The type for an array of T where the extent is specified.
interface	CIVLCompleteDomainType
interface	CIVLDomainType	This is the only one CIVLDomainType associated to the $domain type in program.
interface	CIVLEnumType	An enumeration type.
interface	CIVLFunctionType
interface	CIVLHeapType
interface	CIVLMemType	A CIVLType representing a set of memory locations.
interface	CIVLPointerType	Type of a pointer.
interface	CIVLPrimitiveType	A primitive type is a type of which there is only one instance.
interface	CIVLRegularRangeType
interface	CIVLScopeType	The $scope type in the CIVL-C language.
interface	CIVLSetType	A CIVLType representing a set of a non-set kind CIVLType.
interface	CIVLStateType
interface	CIVLStructOrUnionType	Represents a "record" type (i.e.

Methods in dev.civl.mc.model.IF.type that return CIVLType

Modifier and Type	Method	Description
CIVLType	CIVLPointerType.baseType()	Returns the type of element pointed to.
CIVLType	CIVLType.copyAs(CIVLPrimitiveType type, dev.civl.sarl.IF.SymbolicUniverse universe)
CIVLType	CIVLArrayType.elementType()
CIVLType	CIVLSetType.elementType()
CIVLType	CIVLBundleType.getStaticElementType(int index)
CIVLType[]	CIVLFunctionType.parameterTypes()
CIVLType	CIVLFunctionType.returnType()
CIVLType	StructOrUnionField.type()

Methods in dev.civl.mc.model.IF.type that return types with arguments of type CIVLType

Modifier and Type	Method	Description
List<CIVLType>	CIVLBundleType.types()

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

Modifier and Type	Method	Description
boolean	CIVLType.isSetTypeOf(CIVLType elementType)
boolean	CIVLType.isSuperTypeOf(CIVLType subtype)	Is this type the super type of the given sub-type? If subtype is the same as this type, return true.
void	CIVLFunctionType.setParameterTypes(CIVLType[] types)
void	CIVLFunctionType.setReturnType(CIVLType type)

Method parameters in dev.civl.mc.model.IF.type with type arguments of type CIVLType

Modifier and Type	Method	Description
void	CIVLBundleType.complete(List<CIVLType> types, Collection<dev.civl.sarl.IF.type.SymbolicType> elementTypes, dev.civl.sarl.IF.type.SymbolicUnionType dynamicType)

Uses of CIVLType in dev.civl.mc.model.IF.variable

Methods in dev.civl.mc.model.IF.variable that return CIVLType

Modifier and Type	Method	Description
CIVLType	Variable.type()

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

Modifier and Type	Method	Description
void	Variable.setType(CIVLType type)

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

Methods in dev.civl.mc.semantics.IF that return CIVLType

Modifier and Type	Method	Description
CIVLType	SymbolicAnalyzer.civlTypeOfObjByPointer(CIVLSource soruce, State state, dev.civl.sarl.IF.expr.SymbolicExpression pointer)	Computes the CIVL type of the object referring to by the given pointer.
CIVLType	SymbolicAnalyzer.getArrayBaseType(State state, CIVLSource source, dev.civl.sarl.IF.expr.SymbolicExpression arrayPtr)	pre-condition: "arrayPtr" must point to an array "source" is the @{link CIVLSource} of the pointer expression post-condition: the returned CIVLType must not be an array type the returned object cannot be null Get the type of the non-array element of an array by given a pointer to an array

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

Modifier and Type	Method	Description
Evaluation	Evaluator.evaluateCastWorker(State state, int pid, String process, CIVLType castType, Expression arg)
Evaluation	Evaluator.evaluateSizeofType(CIVLSource source, State state, int pid, CIVLType type)	Evaluate the size of a CIVL type.
TypeEvaluation	Evaluator.getDynamicType(State state, int pid, CIVLType type, CIVLSource source, boolean isDefinition)	Evaluates the dynamic type of a given CIVL type at a certain state.
Evaluation	Evaluator.initialValueOfType(State state, int pid, CIVLType type)	Given a CIVLType t, returns the default initial value of an object of t as if the object has static storage.
List<dev.civl.sarl.IF.expr.ReferenceExpression>	Evaluator.leafNodeReferencesOfType(CIVLSource source, State state, int pid, CIVLType type)
Evaluation	Executor.malloc(CIVLSource source, State state, int pid, String process, Expression scopeExpression, dev.civl.sarl.IF.expr.SymbolicExpression scopeValue, CIVLType objectType, dev.civl.sarl.IF.expr.SymbolicExpression objectValue)	Adds a new object to the heap of a certain scope; returns the pointer of the object in the heap.
String	SymbolicAnalyzer.symbolicExpressionToString(CIVLSource source, State state, CIVLType type, dev.civl.sarl.IF.expr.SymbolicExpression symbolicExpression)	Computes the user-friendly string representation of a symbolic expression.