Uses of Interface
dev.civl.mc.state.IF.MemoryUnitSet
Packages that use MemoryUnitSet
Package
Description
Module kripke provides the definition of various
transitions and the enabler and state manager of CIVL.
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 MemoryUnitSet in dev.civl.mc.kripke.IF
Methods in dev.civl.mc.kripke.IF with parameters of type MemoryUnitSetModifier and TypeMethodDescriptionLibraryEnabler.ampleSet(State state, int pid, CallOrSpawnStatement statement, MemoryUnitSet[] setsReachableRead, MemoryUnitSet[] setsReachableWrite) Computes the ample set process IDs from a system function call at a given state for a given process. -
Uses of MemoryUnitSet in dev.civl.mc.semantics.IF
Methods in dev.civl.mc.semantics.IF that return MemoryUnitSetModifier and TypeMethodDescriptionMemoryUnitExpressionEvaluator.evaluateMemoryUnit(State state, Pair<Scope, dev.civl.sarl.IF.expr.SymbolicExpression[]> parameterScope, int pid, Expression muExpr) Evaluates the memory unit represented by an expression in a contract.MemoryUnitExpressionEvaluator.evaluates(State state, int pid, MemoryUnitExpression memUnit, MemoryUnitSet muSet) evaluates the static impact memory unit expression which is the result of static analysisMethods in dev.civl.mc.semantics.IF with parameters of type MemoryUnitSetModifier and TypeMethodDescriptionMemoryUnitExpressionEvaluator.evaluates(State state, int pid, MemoryUnitExpression memUnit, MemoryUnitSet muSet) evaluates the static impact memory unit expression which is the result of static analysis -
Uses of MemoryUnitSet in dev.civl.mc.state.IF
Methods in dev.civl.mc.state.IF that return MemoryUnitSetModifier and TypeMethodDescriptionMemoryUnitFactory.canonic(MemoryUnitSet muSet) Return the "canonical" version of the given memory unit set.MemoryUnitFactory.intersects(MemoryUnitSet muSet1, MemoryUnitSet muSet2) This is an over-approximation method of intersection.MemoryUnitFactory.newMemoryUnitSet()MemoryUnitFactory.union(MemoryUnitSet muSet1, MemoryUnitSet muSet2) This is an over-approximation method of union.Methods in dev.civl.mc.state.IF with parameters of type MemoryUnitSetModifier and TypeMethodDescriptionvoidMemoryUnitFactory.add(MemoryUnitSet muSet, MemoryUnit mu) Adds a memory unit to a memory unit set.voidMemoryUnitFactory.add(MemoryUnitSet muSet, dev.civl.sarl.IF.expr.SymbolicExpression pointer, StateFactory stateFactory) MemoryUnitFactory.canonic(MemoryUnitSet muSet) Return the "canonical" version of the given memory unit set.MemoryUnitFactory.intersects(MemoryUnitSet muSet1, MemoryUnitSet muSet2) This is an over-approximation method of intersection.booleanMemoryUnitFactory.isJoint(MemoryUnitSet muSet, MemoryUnit mu) This is an over-approximation method of membership testing.booleanMemoryUnitFactory.isJoint(MemoryUnitSet muSet1, MemoryUnitSet muSet2) This is an over-approximation method to test if two memory unit sets have any intersection.MemoryUnitFactory.union(MemoryUnitSet muSet1, MemoryUnitSet muSet2) This is an over-approximation method of union.