Module dev.civl.mc

Package dev.civl.mc.model.IF

Interface LogicFunction

All Superinterfaces:

CIVLFunction, Sourceable

public interface LogicFunction
extends CIVLFunction

A logic function is a function whose definition (body) is either absent (i.e. uninterpreted) or a side-effect free expression.

A function call to a logic function f(formal-param) will be evaluated to f(actual-param). The function will be interpreted , if it has a definition, when a formula is sent to theorem provers. Inlining the function definition is possible but currently not supported.

A set of axioms can be define over a logic function which come up a "theory". Theorem provers will have the knowledge about theories whenever they are called.

A call to a logic function is side-effect free as well hence login function can be recursively defined. To keep logic function calls side-effect free, function pointers are not allowed to refer to logic functions.

Field Summary

Fields

Modifier and Type	Field	Description
static final String	RESERVED_PERMUT	A reserved logic function (int *a, int *b, int l, int h) : bool has a dynamic type (int a[], int oft_a, int b[], int oft_b, int l, int h) : bool after stateless transformation.
static final Set<String>	ReservedLogicFunctionNames	Reserved logic functions are defined by CIVL/SARL

Method Summary

Modifier and Type	Method	Description
Expression	definition()
dev.civl.sarl.prove.IF.ProverFunctionInterpretation	getConstantValue()
static String	heapVariableName(Variable formal)
boolean	isReservedFunction()
int[]	pointerToHeapVidMap()
void	setConstantValue(dev.civl.sarl.prove.IF.ProverFunctionInterpretation constantValue)	Caching the evaluation of a logic function since the definition of a logic function is suppose to be stateless, there is no need to repeatedly evaluate it.

Methods inherited from interface dev.civl.mc.model.IF.CIVLFunction

addLocation, addPossibleValidConsequence, addStatement, computePathconditionOfLocations, containingScope, dependsNoact, fid, functionContract, functionType, getAccessesAtomicFunction, getPossibleValidConsequences, isAbstractFunction, isAtomicFunction, isContracted, isFreeOfUnsafeloop, isLogic, isNondet, isNormalFunction, isPureFunction, isPurelyLocal, isRootFunction, isStateFunction, isSystemFunction, locations, model, name, outerScope, parameters, print, purelyLocalAnalysis, purelyLocalAnalysisForVariables, returnType, scopes, setAccessesAtomicFunction, setContainingScope, setFreeOfUnsafeloop, setFunctionContract, setLocations, setLogic, setModel, setName, setOuterScope, setParameters, setParameterTypes, setPureFunction, setReturnType, setScopes, setStartLocation, setStateFunction, setStatements, simplify, startLocation, statements, unreachedCode, variableAddressedOf, variableAddressedOf

Methods inherited from interface dev.civl.mc.model.IF.Sourceable

getSource, setCIVLSource

Field Details

RESERVED_PERMUT

static final String RESERVED_PERMUT

A reserved logic function (int *a, int *b, int l, int h) : bool has a dynamic type (int a[], int oft_a, int b[], int oft_b, int l, int h) : bool after stateless transformation.

See Also:

• Constant Field Values

ReservedLogicFunctionNames

static final Set<String> ReservedLogicFunctionNames

Reserved logic functions are defined by CIVL/SARL

Method Details

heapVariableName

static String heapVariableName(Variable formal)

definition

Expression definition()

Returns:

the definition of a logic function. Optional. If a logic function has no definition, this method returns null.

setConstantValue

void setConstantValue(dev.civl.sarl.prove.IF.ProverFunctionInterpretation constantValue)

Caching the evaluation of a logic function since the definition of a logic function is suppose to be stateless, there is no need to repeatedly evaluate it.

Parameters:

constantValue - an instance of ProverFunctionInterpretation.

getConstantValue

dev.civl.sarl.prove.IF.ProverFunctionInterpretation getConstantValue()

Returns:

the cached evaluation of this logic function, which is an instance of ProverFunctionInterpretation.

Pointer type formal parameters will be replaced with array type symbolic constants to achieve the statelessness.

pointerToHeapVidMap

int[] pointerToHeapVidMap()

Returns:

a map which maps indices of pointer-type formal parameters to variable IDs of their dummy heap in the same parameter scope. Logic function is state-independent, but the pointer-type formal parameters must point to a some array, CIVL model allocates some spot in the parameter scope for these pointers to point to.

isReservedFunction

boolean isReservedFunction()

Returns:

true iff this logic function is defined in CIVL/SARL instead of being defined by programmers