Module dev.civl.mc

Package dev.civl.mc.dynamic.IF

Interface ValueSetUtility

public interface ValueSetUtility

Method Summary

Modifier and Type	Method	Description
dev.civl.sarl.IF.expr.BooleanExpression	buildFrameCondition(dev.civl.sarl.IF.type.SymbolicType varType, dev.civl.sarl.IF.expr.SymbolicExpression oldVal, dev.civl.sarl.IF.expr.SymbolicExpression newVal, dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate)	Builds an assertion stating that all the objects in a variable of varType NOT referred by valueSetTemplate preserve their old values.
List<dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference>	extendToFull(dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference vsRef, dev.civl.sarl.IF.type.SymbolicType varType)	Extends the ValueSetReference vsRef to an equivalent set of references to primitives
dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference	getVSReferenceToSequenceOrNoop(CIVLType variableOrMallocElementType, boolean isMallocElementType, dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference vsRef)	This method over-approximates vsRef if it references into sequence elements.
Iterable<List<dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference>>	toDisjointGroups(dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate)	Divides ValueSetReferences in a value set template to a number of groups.

Method Details

extendToFull

List<dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference> extendToFull(dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference vsRef,
 dev.civl.sarl.IF.type.SymbolicType varType)

Extends the ValueSetReference vsRef to an equivalent set of references to primitives

Parameters:

vsRef - a ValueSetReference

varType - the type of variables where vsRef applies

Returns:

an set of references to primitives equivalent to the given vsRef

toDisjointGroups

Iterable<List<dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference>> toDisjointGroups(dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate)

Divides ValueSetReferences in a value set template to a number of groups. Every pair of groups are referring to disjoint objects in a variable.

buildFrameCondition

dev.civl.sarl.IF.expr.BooleanExpression buildFrameCondition(dev.civl.sarl.IF.type.SymbolicType varType,
 dev.civl.sarl.IF.expr.SymbolicExpression oldVal,
 dev.civl.sarl.IF.expr.SymbolicExpression newVal,
 dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate)

Builds an assertion stating that all the objects in a variable of varType NOT referred by valueSetTemplate preserve their old values. (i.e., their newVal equals to their oldVal).

Parameters:

varType - the type of the variable associated to valueSetTemplate

oldVal - old value of the variable

newVal - new value of the variable

valueSetTemplate - a value set template associated to varType

Returns:

an assertion as described above.

getVSReferenceToSequenceOrNoop

dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference getVSReferenceToSequenceOrNoop(CIVLType variableOrMallocElementType,
 boolean isMallocElementType,
 dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference vsRef)

This method over-approximates vsRef if it references into sequence elements. In this case, the returned value is an ancestor that references to the outer-most sequence object that encloses what vsRef references to.

The parameter variableOrMallocElementType is the CIVLType of the variable where vsRef references, if vsRef does NOT reference to a heap object. Otherwise, variableOrMallocElementType is the element type statically determined by the corresponding malloc statement. In this case, the root ancestor of vsRef references to the heap object instead of the heap variable.

The reason of why this method analyzes vsRef with respect to CIVLType instead of dynamic types is that sequence type is invisible to dynamic types. The reason of why we treat variables and heap objects differently is that there is no CIVLType exisiting in the model for a heap object. There are only CIVLType of static element types extracted from malloc statement.