Module dev.civl.mc

Package dev.civl.mc.semantics.IF

Interface MemoryUnitExpressionEvaluator

public interface MemoryUnitExpressionEvaluator

Method Summary

Modifier and Type	Method	Description
MemoryUnitSet	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.
MemoryUnitSet	evaluates(State state, int pid, MemoryUnitExpression memUnit, MemoryUnitSet muSet)	evaluates the static impact memory unit expression which is the result of static analysis

Method Details

evaluates

MemoryUnitSet evaluates(State state,
 int pid,
 MemoryUnitExpression memUnit,
 MemoryUnitSet muSet)
                 throws UnsatisfiablePathConditionException

evaluates the static impact memory unit expression which is the result of static analysis

Parameters:

state - the current state

pid - the PID of the process that triggers this evaluation

memUnit - the impact memory unit expression

muSet -

Returns:

Throws:

UnsatisfiablePathConditionException

evaluateMemoryUnit

MemoryUnitSet evaluateMemoryUnit(State state,
 Pair<Scope,dev.civl.sarl.IF.expr.SymbolicExpression[]> parameterScope,
 int pid,
 Expression muExpr)
                          throws UnsatisfiablePathConditionException

Evaluates the memory unit represented by an expression in a contract. A memory unit expression should be side-effect free.

Parameters:

state -

pid -

muExpr -

Returns:

Throws:

UnsatisfiablePathConditionException