Module dev.civl.mc

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

Interface CIVLScopeType

All Superinterfaces:

CIVLPrimitiveType, CIVLType

public interface CIVLScopeType
extends CIVLPrimitiveType

The $scope type in the CIVL-C language.

For any object of $scope type, its value has a SymbolicType which is called the dynamic scope type and is uniquely associated with the $scope type. The definition of the dynamic scope type is defined in this class as well.

The definition of a dynamic scope type is up to the implementation of this interface but it must satisfy one restriction: a symbolic value of dynamic scope type must be associated with an integer. The integer is called the identity of a scope value. Two scope values are equivalent iff their identities are equal.

Nested Class Summary

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

CIVLPrimitiveType.PrimitiveTypeKind

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

CIVLType.TypeKind

Method Summary

Modifier and Type	Method	Description
Function<Integer,dev.civl.sarl.IF.expr.SymbolicExpression>	scopeIdentityToValueOperator(dev.civl.sarl.IF.SymbolicUniverse universe)
Function<dev.civl.sarl.IF.expr.SymbolicExpression,dev.civl.sarl.IF.number.IntegerNumber>	scopeValueToIdentityOperator(dev.civl.sarl.IF.SymbolicUniverse universe)

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

getFacts, getSizeof, 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

scopeValueToIdentityOperator

Function<dev.civl.sarl.IF.expr.SymbolicExpression,dev.civl.sarl.IF.number.IntegerNumber> scopeValueToIdentityOperator(dev.civl.sarl.IF.SymbolicUniverse universe)

Parameters:

universe - a reference to SymbolicUniverse

Returns:

A java Function which maps a scope value to its integral identity.

scopeIdentityToValueOperator

Function<Integer,dev.civl.sarl.IF.expr.SymbolicExpression> scopeIdentityToValueOperator(dev.civl.sarl.IF.SymbolicUniverse universe)

Parameters:

universe - a reference to SymbolicUniverse

Returns:

A java Function which maps an integral identity to a scope value.