Module dev.civl.mc

Package dev.civl.mc.dynamic.IF

Interface DynamicMemoryLocationSetFactory

public interface DynamicMemoryLocationSetFactory

Method Summary

Modifier and Type	Method	Description
DynamicMemoryLocationSet	addReference(DynamicMemoryLocationSet writeSet, dev.civl.sarl.IF.expr.SymbolicExpression memValue)	Add references in a "memValue" into the given "writeSet", returns a new write set
DynamicMemoryLocationSet	empty()

Method Details

empty

DynamicMemoryLocationSet empty()

Returns:

an empty DynamicMemoryLocationSet

addReference

DynamicMemoryLocationSet addReference(DynamicMemoryLocationSet writeSet,
 dev.civl.sarl.IF.expr.SymbolicExpression memValue)

Add references in a "memValue" into the given "writeSet", returns a new write set

Parameters:

writeSet - a DynamicWriteSet

memValue - a symbolic expression of CIVLType.getDynamicType(dev.civl.sarl.IF.SymbolicUniverse) type

Returns: