Uses of Interface
dev.civl.mc.model.IF.Scope
Packages that use Scope
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.
Submodule model.type defines types in CIVL.
Submodule model.variable defines variables in CIVL.
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 Scope in dev.civl.mc.model.IF
Methods in dev.civl.mc.model.IF that return ScopeModifier and TypeMethodDescriptionCIVLFunction.containingScope()ModelFactory.leastCommonAncestor(Scope s0, Scope s1) CIVLFunction.outerScope()Scope.parent()ModelFactory.scope(CIVLSource source, Scope parent, List<Variable> variables, CIVLFunction function) Create a new scope.Model.staticConstantScope()returns the scope for constantsModelFactory.staticConstantScope()returns the static scope for constantsMethods in dev.civl.mc.model.IF that return types with arguments of type ScopeMethods in dev.civl.mc.model.IF with parameters of type ScopeModifier and TypeMethodDescriptionModelFactory.abstractFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, int continuity, String attribute) Generate an abstract function.AccuracyAssumptionBuilder.accuracyAssumptions(Expression assumption, Scope scope) Analyze an assumption.voidModelFactory.compoundLiteralExpression(CIVLSource source, Scope exprScope, CIVLType type, boolean isStringLiteral) Creates a new instance of a compound literal expression.ModelFactory.domSizeVariable(CIVLSource source, Scope scope) ModelFactory.function(CIVLSource source, boolean isAtomic, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, Location startLocation) Create a new function.booleanScope.isDescendantOf(Scope anc) Return true if the scope is a descendant of the scope ancModelFactory.leastCommonAncestor(Scope s0, Scope s1) ModelFactory.location(CIVLSource source, Scope scope) Create a new location.ModelFactory.logicFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType outputType, int[] pointerToHeapMap, Scope containingScope, Expression definition) Create a new logic function (LogicFunction).ModelFactory.newAnonymousVariable(CIVLSource sourceOf, Scope scope, CIVLType type) Create a variable of the given type and add it to the given scope.ModelFactory.newAnonymousVariableForArrayLiteral(CIVLSource sourceOf, Scope scope, CIVLArrayType type) Creates an anonymous variable of array type in a certain scope.ModelFactory.nondetFunction(CIVLSource source, Identifier name, CIVLType returnType, Scope containingScope) ModelFactory.parProcsVariable(CIVLSource source, CIVLType type, Scope scope) ModelFactory.scope(CIVLSource source, Scope parent, List<Variable> variables, CIVLFunction function) Create a new scope.voidCIVLFunction.setContainingScope(Scope containingScope) voidCIVLFunction.setOuterScope(Scope outerScope) voidvoidSet the system scope, which is the root (static) scope of the model.ModelFactory.systemFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, String libraryName) Generate the system functionCIVLFunction.variableAddressedOf(Scope scope) returns the variables that are used as the operand of the address-of operator and are visible from the given lexical scope.Method parameters in dev.civl.mc.model.IF with type arguments of type Scope -
Uses of Scope in dev.civl.mc.model.IF.contract
Methods in dev.civl.mc.model.IF.contract that return ScopeModifier and TypeMethodDescriptionFunctionContract.scope()The static scope in which the function contract exists.Methods in dev.civl.mc.model.IF.contract with parameters of type ScopeModifier and TypeMethodDescriptionContractFactory.newFunctionContract(CIVLSource source, Scope scope) Creates a new function contract. -
Uses of Scope in dev.civl.mc.model.IF.expression
Methods in dev.civl.mc.model.IF.expression that return ScopeModifier and TypeMethodDescriptionExpression.expressionScope()Expression.lowestScope()FunctionIdentifierExpression.scope()Methods in dev.civl.mc.model.IF.expression with parameters of type ScopeModifier and TypeMethodDescriptionvoidExpression.purelyLocalAnalysisOfVariables(Scope funcScope) Analyzes if variables accessed by this expression are purely localExpression.variableAddressedOf(Scope scope) Compute the set of variables visible from a certain scope that appear in an address-of expression.LHSExpression.variableWritten(Scope scope) Return the variable that is visible from the given scope, which is possible the left hand side of an assignment statement. -
Uses of Scope in dev.civl.mc.model.IF.location
Methods in dev.civl.mc.model.IF.location that return ScopeModifier and TypeMethodDescriptionLocation.impactScopeOfAtomicOrAtomBlock()The impact scope of a location is required in the enabler when an atomic/atom block is encountered, in which case the impact scope of all statements in the atomic block should be considered.Location.scope()Methods in dev.civl.mc.model.IF.location with parameters of type ScopeModifier and TypeMethodDescriptionvoidLocation.setImpactScopeOfAtomicOrAtomBlock(Scope scope) set the impact scope of a location, only called when this.AtomicKind == ATOM_ENTER or ATOMIC_ENTER.void -
Uses of Scope in dev.civl.mc.model.IF.statement
Methods in dev.civl.mc.model.IF.statement that return ScopeModifier and TypeMethodDescriptionStatement.lowestScope()Obtains the lowest scope of expression accessed by this statement.Statement.statementScope()Methods in dev.civl.mc.model.IF.statement with parameters of type ScopeModifier and TypeMethodDescriptionvoidStatement.purelyLocalAnalysisOfVariables(Scope funcScope) if an invalid input: '&'(var) is encountered, then var is considered as no purely local if a statement inside a function with fscope is accessing some variable that is declared in the scope vscope such that fscope.isDescendantOf(vscope), then that variable is not purely localStatement.variableAddressedOf(Scope scope) Obtain the set of variables visible from a certain scope that are possible to be written in the future. -
Uses of Scope in dev.civl.mc.model.IF.type
Methods in dev.civl.mc.model.IF.type that return Scope -
Uses of Scope in dev.civl.mc.model.IF.variable
Methods in dev.civl.mc.model.IF.variable that return ScopeMethods in dev.civl.mc.model.IF.variable with parameters of type Scope -
Uses of Scope in dev.civl.mc.semantics.IF
Method parameters in dev.civl.mc.semantics.IF with type arguments of type ScopeModifier and TypeMethodDescriptionMemoryUnitExpressionEvaluator.evaluateMemoryUnit(State state, Pair<Scope, dev.civl.sarl.IF.expr.SymbolicExpression[]> parameterScope, int pid, Expression muExpr) Evaluates the memory unit represented by an expression in a contract. -
Uses of Scope in dev.civl.mc.state.IF
Methods in dev.civl.mc.state.IF that return ScopeModifier and TypeMethodDescriptionDynamicScope.lexicalScope()Returns the lexical (static) scope of which this dynamic scope is an instance.Methods in dev.civl.mc.state.IF with parameters of type ScopeModifier and TypeMethodDescriptionintState.getDyscope(int pid, Scope scope) Given a PID and a static scope, returns the ID of the first dyscope corresponding to the static scope and reachable from the given process.