Module dev.civl.mc

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

Interface CIVLMemType

All Superinterfaces:

CIVLSetType, CIVLType

public interface CIVLMemType
extends CIVLSetType

A CIVLType representing a set of memory locations.

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static interface	CIVLMemType.MemoryLocationReference	Implementations of CIVLMemType.MemoryLocationReference represent references to a subset of a value of a variable/heap object

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.UnaryOperator<dev.civl.sarl.IF.expr.SymbolicExpression>	memValueCollector(dev.civl.sarl.IF.SymbolicUniverse u, dev.civl.sarl.IF.expr.SymbolicExpression collectedScopeValue)	Returns a UnaryOperator to $mem values that will clean up references in the $mem value.
Function<List<dev.civl.sarl.IF.expr.SymbolicExpression[]>,dev.civl.sarl.IF.expr.SymbolicExpression>	memValueCreator(dev.civl.sarl.IF.SymbolicUniverse u)
Function<dev.civl.sarl.IF.expr.SymbolicExpression,Iterable<CIVLMemType.MemoryLocationReference>>	memValueIterator()

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

elementType

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

memValueIterator

Function<dev.civl.sarl.IF.expr.SymbolicExpression,Iterable<CIVLMemType.MemoryLocationReference>> memValueIterator()

Returns:

a Function that maps dynamic $mem type values to a set of CIVLMemType.MemoryLocationReference.

memValueCreator

Function<List<dev.civl.sarl.IF.expr.SymbolicExpression[]>,dev.civl.sarl.IF.expr.SymbolicExpression> memValueCreator(dev.civl.sarl.IF.SymbolicUniverse u)

Parameters:

u - a reference to SymbolicUniverse

Returns:

a Function that maps a set of symbolic expression arrays, to a value of dynamic $mem type. Each symbolic expression array must have five elements, each of which represents: 1. variable ID, 2. heap ID, 3. malloc ID, 4. scopeValue and 5. value set template respectively. Such five elements will form a reference to a subset of a variable/heap object.

heap ID is the ID of a lexical malloc statement which creates the heap object; malloc ID is the ID of a run-time call to a malloc statement which creates the heap object. When the symbolic expression array represents a reference to a subset of a variable value (not heap object), heapID and mallocID are not significant.

memValueCollector

dev.civl.sarl.IF.UnaryOperator<dev.civl.sarl.IF.expr.SymbolicExpression> memValueCollector(dev.civl.sarl.IF.SymbolicUniverse u,
 dev.civl.sarl.IF.expr.SymbolicExpression collectedScopeValue)

Returns a UnaryOperator to $mem values that will clean up references in the $mem value. The references in the $mem value that refer to the variable/heap objects, that are no longer alive, will be collected.

Parameters:

u - a reference to SymbolicUniverse

collectedScopeValue - the unique scope value representing a collected scope. Once a scope is collected, its scope value must equal to this parameter.

Returns:

a UnaryOperator to $mem values that will clean up references in the $mem value.