Uses of Interface
dev.civl.mc.model.IF.CIVLFunction
Packages that use CIVLFunction
Package
Description
Module model defines a static model, i.e., the control flow graph, representation of a CIVL-C program.
Submodule model.expression defines expression in CIVL.
Submodule model.location defines a location in the control flow graph of CIVL.
Submodule model.statement defines a statement of a CIVL-C program.
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 CIVLFunction in dev.civl.mc.model.IF
Subinterfaces of CIVLFunction in dev.civl.mc.model.IFModifier and TypeInterfaceDescriptioninterfaceAn abstract function is an uninterpreted mathematical function.interfaceA logic function is a function whose definition (body) is either absent (i.e.interfaceA system function is a function that is implemented in a library executor, not in source code.Methods in dev.civl.mc.model.IF that return CIVLFunctionModifier and TypeMethodDescriptionGet a function based on its name.ModelFactory.function(CIVLSource source, boolean isAtomic, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, Location startLocation) Create a new function.Scope.function()Scope.getFunction(int fid) Scope.getFunction(Identifier name) Scope.getFunction(String name) ModelFactory.nondetFunction(CIVLSource source, Identifier name, CIVLType returnType, Scope containingScope) Model.rootFunction()Methods in dev.civl.mc.model.IF that return types with arguments of type CIVLFunctionMethods in dev.civl.mc.model.IF with parameters of type CIVLFunctionModifier and TypeMethodDescriptionvoidModel.addFunction(CIVLFunction function) voidScope.addFunction(CIVLFunction function) ModelFactory.civlParForEnterStatement(CIVLSource source, Location location, Expression domain, VariableExpression domSize, VariableExpression procsVar, CIVLFunction parProcFunc) creates a$parforenter statement to start the execution of the$parfor.ModelFactory.functionIdentifierExpression(CIVLSource source, CIVLFunction function) creates a function identifier expression.ModelFactory.model(CIVLSource source, CIVLFunction system, dev.civl.abc.program.IF.Program program) Create a new model.ModelFactory.returnFragment(CIVLSource civlSource, Location source, Expression expression, CIVLFunction function) Create a one-statement fragment that contains the return statement.ModelFactory.scope(CIVLSource source, Scope parent, List<Variable> variables, CIVLFunction function) Create a new scope.voidScope.setFunction(CIVLFunction function) voidModel.setRootFunction(CIVLFunction root) ModelFactory.updateStatement(CIVLSource source, Location srcLoc, Expression guard, Expression collator, CIVLFunction function, Expression[] arguments) Method parameters in dev.civl.mc.model.IF with type arguments of type CIVLFunction -
Uses of CIVLFunction in dev.civl.mc.model.IF.contract
Methods in dev.civl.mc.model.IF.contract that return CIVLFunctionModifier and TypeMethodDescriptionCallEvent.function()The function (i.e., the callee) of this call event.Methods in dev.civl.mc.model.IF.contract with parameters of type CIVLFunctionModifier and TypeMethodDescriptionContractFactory.newCallEvent(CIVLSource source, CIVLFunction function, List<Expression> arguments) Creates a new instance of call event.voidCallEvent.setFunction(CIVLFunction function) Sets the callee of this event -
Uses of CIVLFunction in dev.civl.mc.model.IF.expression
Methods in dev.civl.mc.model.IF.expression that return CIVLFunction -
Uses of CIVLFunction in dev.civl.mc.model.IF.location
Methods in dev.civl.mc.model.IF.location that return CIVLFunction -
Uses of CIVLFunction in dev.civl.mc.model.IF.statement
Methods in dev.civl.mc.model.IF.statement that return CIVLFunctionModifier and TypeMethodDescriptionCallOrSpawnStatement.function()TODO: get rid of itUpdateStatement.function()CivlParForSpawnStatement.parProcFunction()returns the function to be executed by the spawned processes, which is equivalent to the body of the $parfor.Methods in dev.civl.mc.model.IF.statement with parameters of type CIVLFunctionModifier and TypeMethodDescriptionvoidCivlParForSpawnStatement.setParProcFunction(CIVLFunction function) updates the function which will be executed by spawned processes. -
Uses of CIVLFunction in dev.civl.mc.semantics.IF
Methods in dev.civl.mc.semantics.IF that return types with arguments of type CIVLFunctionModifier and TypeMethodDescriptionEvaluator.evaluateFunctionIdentifier(State state, int pid, Expression functionPointer, CIVLSource source) Evaluates a function pointer expression. -
Uses of CIVLFunction in dev.civl.mc.state.IF
Methods in dev.civl.mc.state.IF with parameters of type CIVLFunctionModifier and TypeMethodDescriptionStateFactory.addProcess(State state, CIVLFunction function, int functionParentDyscope, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments, int callerPid, boolean isSelfDestructable) Adds a new process.StateFactory.addProcess(State state, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments, int callerPid, boolean isSelfDestructable) Adds a new process.StateFactory.pushCallStack(State state, int pid, CIVLFunction function, int functionParentDyscope, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments) Pushes a new entry onto the call stack for a process.StateFactory.pushCallStack(State state, int pid, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments) Pushes a new entry onto the call stack for a process.StateFactory.pushContract(State state, int pid, CIVLFunction function, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments) Pushes a new frame onto the call stack where static scope of the frame is the contract scope of a function.