Uses of Interface
dev.civl.mc.model.IF.statement.CallOrSpawnStatement
Packages that use CallOrSpawnStatement
Package
Description
Module analysis provides a list of analyzers for static/runtime analyzing of a program.
Module kripke provides the definition of various
transitions and the enabler and state manager of CIVL.
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.
-
Uses of CallOrSpawnStatement in dev.civl.mc.analysis.IF
Methods in dev.civl.mc.analysis.IF with parameters of type CallOrSpawnStatementModifier and TypeMethodDescriptionvoidCodeAnalyzer.analyze(State state, int pid, CallOrSpawnStatement statement, dev.civl.sarl.IF.expr.SymbolicExpression[] argumentValues) Analyzes a call statement.static voidAnalysis.analyzeCall(List<CodeAnalyzer> analyzers, State state, int pid, CallOrSpawnStatement statement, dev.civl.sarl.IF.expr.SymbolicExpression[] arguments) Analyzes a call statement at a certain state. -
Uses of CallOrSpawnStatement in dev.civl.mc.kripke.IF
Methods in dev.civl.mc.kripke.IF with parameters of type CallOrSpawnStatementModifier and TypeMethodDescriptionLibraryEnabler.ampleSet(State state, int pid, CallOrSpawnStatement statement, MemoryUnitSet[] setsReachableRead, MemoryUnitSet[] setsReachableWrite) Computes the ample set process IDs from a system function call at a given state for a given process.LibraryEnabler.enabledTransitions(State state, CallOrSpawnStatement call, dev.civl.sarl.IF.expr.BooleanExpression pathCondition, int pid) Computes the enabled transitions of a given function call. -
Uses of CallOrSpawnStatement in dev.civl.mc.model.IF
Methods in dev.civl.mc.model.IF that return CallOrSpawnStatementModifier and TypeMethodDescriptionModelFactory.callOrSpawnStatement(CIVLSource sourceOf, Location location, boolean isCall, Expression function, List<Expression> arguments, Expression guard, boolean isInitializer) Creates a call or spawn statement.Methods in dev.civl.mc.model.IF with parameters of type CallOrSpawnStatementModifier and TypeMethodDescriptionModelFactory.functionCallExpression(CallOrSpawnStatement callStatement) creates a system function call expressionModelFactory.systemGuardExpression(CallOrSpawnStatement sysCall) Creates the system guard expression for the given system call statement.ModelFactory.updateStatement(CIVLSource source, Location srcLoc, Expression guard, Expression collator, CallOrSpawnStatement call) Creates an$updatestatement. -
Uses of CallOrSpawnStatement in dev.civl.mc.model.IF.expression
Methods in dev.civl.mc.model.IF.expression that return CallOrSpawnStatement -
Uses of CallOrSpawnStatement in dev.civl.mc.model.IF.location
Methods in dev.civl.mc.model.IF.location that return types with arguments of type CallOrSpawnStatementMethod parameters in dev.civl.mc.model.IF.location with type arguments of type CallOrSpawnStatementModifier and TypeMethodDescriptionvoidLocation.setSystemCalls(Set<CallOrSpawnStatement> systemCalls) -
Uses of CallOrSpawnStatement in dev.civl.mc.model.IF.statement
Methods in dev.civl.mc.model.IF.statement that return CallOrSpawnStatementModifier and TypeMethodDescriptionUpdateStatement.call()CallOrSpawnStatement.replaceWith(ConditionalExpression oldExpression, Expression newExpression) -
Uses of CallOrSpawnStatement in dev.civl.mc.semantics.IF
Methods in dev.civl.mc.semantics.IF with parameters of type CallOrSpawnStatementModifier and TypeMethodDescriptionLibraryExecutor.execute(State state, int pid, CallOrSpawnStatement statement, String functionName) Executes the given call statement for a certain process at the given state.