Module dev.civl.mc

Package dev.civl.mc.model.IF

Interface SystemFunction

All Superinterfaces:

CIVLFunction, Sourceable

public interface SystemFunction
extends CIVLFunction

A system function is a function that is implemented in a library executor, not in source code.

Method Summary

Modifier and Type	Method	Description
String	getLibrary()
boolean	needsEnabler()	returns true iff this system function needs special handling from the library enabler.
void	setLibrary(String libraryName)

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

Method Details

getLibrary

String getLibrary()

Returns:

The name of the library containing this system function.

setLibrary

void setLibrary(String libraryName)

Parameters:

libraryName - The name of the library containing this system function.

needsEnabler

boolean needsEnabler()

returns true iff this system function needs special handling from the library enabler.

Returns:

true iff this system function needs special handling from the library enabler.