Uses of Interface
dev.civl.mc.state.IF.MemoryUnit
Packages that use MemoryUnit
Package
Description
Module semantics implements the semantics of CIVL-C.
Module state is responsible for the creation and manipulation of
states of a CIVL model.
-
Uses of MemoryUnit in dev.civl.mc.semantics.IF
Methods in dev.civl.mc.semantics.IF with parameters of type MemoryUnitModifier and TypeMethodDescriptionSymbolicAnalyzer.memoryUnitToString(State state, MemoryUnit mu) Pretty representation of a memory unit. -
Uses of MemoryUnit in dev.civl.mc.state.IF
Methods in dev.civl.mc.state.IF that return MemoryUnitModifier and TypeMethodDescriptionMemoryUnitFactory.extendReference(MemoryUnit mu, dev.civl.sarl.IF.expr.ReferenceExpression extraRef) extends a memory unit with extra references.MemoryUnitFactory.newMemoryUnit(int dyscopeID, int varID, dev.civl.sarl.IF.expr.ReferenceExpression reference) MemoryUnit.setReference(dev.civl.sarl.IF.expr.ReferenceExpression ref) updates the reference of this memory unitMethods in dev.civl.mc.state.IF that return types with arguments of type MemoryUnitMethods in dev.civl.mc.state.IF with parameters of type MemoryUnitModifier and TypeMethodDescriptionvoidMemoryUnitFactory.add(MemoryUnitSet muSet, MemoryUnit mu) Adds a memory unit to a memory unit set.voidMemoryUnitSet.add(MemoryUnit mu) booleanMemoryUnitFactory.contains(MemoryUnit mu1, MemoryUnit mu2) Does mu1 contains mu2? returns true iff mu1 equals mu2, or mu1 and mu2 are referring to the same object and mu1 is containing mu2.MemoryUnitFactory.extendReference(MemoryUnit mu, dev.civl.sarl.IF.expr.ReferenceExpression extraRef) extends a memory unit with extra references.booleanMemoryUnitFactory.isJoint(MemoryUnit mu1, MemoryUnit mu2) This is an over-approximation method to test if two memory units have any intersection.booleanMemoryUnitFactory.isJoint(MemoryUnitSet muSet, MemoryUnit mu) This is an over-approximation method of membership testing.