Module dev.civl.mc

Package dev.civl.mc.model.IF.type

Interface CIVLPrimitiveType

All Superinterfaces:

CIVLType

All Known Subinterfaces:

CIVLScopeType, CIVLStateType

public interface CIVLPrimitiveType
extends CIVLType

A primitive type is a type of which there is only one instance. In addition, there is a single symbolic type corresponding to each primitive type.

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static enum	CIVLPrimitiveType.PrimitiveTypeKind

Nested classes/interfaces inherited from interface dev.civl.mc.model.IF.type.CIVLType

CIVLType.TypeKind

Method Summary

Modifier and Type	Method	Description
dev.civl.sarl.IF.expr.BooleanExpression	getFacts()	Returns facts about this primitive type that should be added to the path condition whenever it is used.
dev.civl.sarl.IF.expr.NumericExpression	getSizeof()	Returns the symbolic value representing the size of this primitive type, i.e., the value of "sizeof(t)".
CIVLPrimitiveType.PrimitiveTypeKind	primitiveTypeKind()

Methods inherited from interface dev.civl.mc.model.IF.type.CIVLType

analyze, areSubtypesScalar, copyAs, freeVariables, getDynamicType, getDynamicTypeIndex, getStateVariable, hasReferences, hasState, isArrayType, isBoolType, isBundleType, isCharType, isDomainType, isEnumerationType, isFunction, isHeapType, isIncompleteArrayType, isIntegerType, isNumericType, isPointerType, isProcessType, isRangeType, isRealType, isScalar, isScopeType, isSetType, isSetTypeOf, isStructType, isSuperTypeOf, isUnionType, isVoidType, setStateVariable, typeKind

Method Details

primitiveTypeKind

CIVLPrimitiveType.PrimitiveTypeKind primitiveTypeKind()

Returns:

The kind of this primitive type, an element of the enumerated type

getSizeof

dev.civl.sarl.IF.expr.NumericExpression getSizeof()

Returns the symbolic value representing the size of this primitive type, i.e., the value of "sizeof(t)".

Returns:

the size of this type

getFacts

dev.civl.sarl.IF.expr.BooleanExpression getFacts()

Returns facts about this primitive type that should be added to the path condition whenever it is used. For example, that "sizeof(t)>0".

Returns:

predicate which must hold concerning this type