Uses of Interface
dev.civl.mc.model.IF.variable.Variable

Packages that use Variable

Package	Description
dev.civl.mc.model.IF	Module model defines a static model, i.e., the control flow graph, representation of a CIVL-C program.
dev.civl.mc.model.IF.expression	Submodule model.expression defines expression in CIVL.
dev.civl.mc.model.IF.location	Submodule model.location defines a location in the control flow graph of CIVL.
dev.civl.mc.model.IF.statement	Submodule model.statement defines a statement of a CIVL-C program.
dev.civl.mc.model.IF.type	Submodule model.type defines types in CIVL.
dev.civl.mc.state.IF	Module state is responsible for the creation and manipulation of states of a CIVL model.

Uses of Variable in dev.civl.mc.model.IF

Methods in dev.civl.mc.model.IF that return Variable

Modifier and Type	Method	Description
Variable	ModelFactory.brokenTimeVariable()
Variable	Scope.contains(Variable variable)	If a variable is already included in this scope, return the included variable.
Variable	ModelFactory.newAnonymousVariable(CIVLSource sourceOf, Scope scope, CIVLType type)	Create a variable of the given type and add it to the given scope.
Variable	ModelFactory.newAnonymousVariableForArrayLiteral(CIVLSource sourceOf, Scope scope, CIVLArrayType type)	Creates an anonymous variable of array type in a certain scope.
Variable	ModelFactory.newAnonymousVariableForConstantArrayLiteral(CIVLSource sourceOf, CIVLArrayType type, dev.civl.sarl.IF.expr.SymbolicExpression value)	Creates an anonymous variable of array type in the static constant scope.
Variable	ModelFactory.timeCountVariable()
Variable	ModelFactory.variable(CIVLSource source, CIVLType type, Identifier name, int vid)	Create a new variable.
Variable	Scope.variable(int vid)	Get the variable at the specified array index.
Variable	Scope.variable(Identifier name)	Get the variable associated with an identifier.
Variable	Scope.variable(String name)
Variable	ModelFactory.variableAsParameter(CIVLSource source, CIVLType type, Identifier name, int vid)	Create a new variable which is also a parameter of some function.
Variable[]	Scope.variables()	Important notice: Never ever modify the variable!

Methods in dev.civl.mc.model.IF that return types with arguments of type Variable

Modifier and Type	Method	Description
Map<String,Variable>	Model.externVariables()
Set<Variable>	CIVLFunction.getAccessesAtomicFunction()
List<Variable>	ModelFactory.inputVariables()
List<Variable>	Model.outputVariables()	Return the output variables of this model, which all belong to the root scope.
List<Variable>	CIVLFunction.parameters()
Set<Variable>	CIVLFunction.variableAddressedOf()	returns the variables that are used as the operand of the address-of operator.
Set<Variable>	CIVLFunction.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.
Collection<Variable>	Scope.variablesWithPointers()	A variable contains a pointer type if it is of type PointerType, if it is an array with elements containing pointer type, or if it is a struct with fields containing pointer type.
Collection<Variable>	Scope.variablesWithProcrefs()	A variables has a "procRefType" if it is of type Process, if it is an array with element of procRefType, or if it is a struct with fields of procRefType.
Collection<Variable>	Scope.variablesWithScoperefs()	A variables has a "scopeRefType" if it is of type Scope, if it is an array with element of scopeRefType, if it is a struct with fields of scopeRefType, or if it contains a pointer.
Collection<Variable>	Scope.variablesWithStaterefs()	A variables has a "$state" type, if it is of type $state, if it is an array with element of type $state, or if it is a struct with fields of type $state.
Collection<Variable>	Scope.varsNeedSymbolicConstant()	A variable whose type is not a primitive type.

Methods in dev.civl.mc.model.IF with parameters of type Variable

Modifier and Type	Method	Description
void	ModelFactory.addInputVariable(Variable variable)
void	Scope.addVariable(Variable variable)	A new variable in this scope.
Fragment	ModelFactory.civlForEnterFragment(CIVLSource source, Location src, Expression dom, List<Variable> variables, Variable counter)	Returns a new fragment containing a CivlForStatement.
Variable	Scope.contains(Variable variable)	If a variable is already included in this scope, return the included variable.
DomainGuardExpression	ModelFactory.domainGuard(CIVLSource source, List<Variable> vars, Variable counter, Expression domain)	Returns a domain guard expression which is boolean expression whose arguments consists of loop variables in a CIVL $for loop and the original domain associate to the loop.
int	Scope.getVid(Variable staticVariable)
static String	LogicFunction.heapVariableName(Variable formal)
InitialValueExpression	ModelFactory.initialValueExpression(CIVLSource source, Variable variable)	Returns an "initial value" expression for the given variable.
LambdaExpression	ModelFactory.lambdaExpression(CIVLSource source, CIVLFunctionType functionType, Variable variable, Expression expression)	Creates a new lambda expression.
MemoryUnitExpression	ModelFactory.memoryUnitExpression(CIVLSource source, Variable variable, CIVLType objetType, MemoryUnitReference reference, boolean writable, boolean hasPinterRef)	creates a memory unit expression.
VariableExpression	ModelFactory.variableExpression(CIVLSource source, Variable variable)	A variable expression.

Method parameters in dev.civl.mc.model.IF with type arguments of type Variable

Modifier and Type	Method	Description
AbstractFunction	ModelFactory.abstractFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, int continuity, String attribute)	Generate an abstract function.
ArrayLambdaExpression	ModelFactory.arrayLambdaExpression(CIVLSource source, CIVLArrayType arrayType, List<Pair<List<Variable>,Expression>> boundVariableList, Expression restriction, Expression expression)	Creates a new array lambda expression.
Fragment	ModelFactory.civlForEnterFragment(CIVLSource source, Location src, Expression dom, List<Variable> variables, Variable counter)	Returns a new fragment containing a CivlForStatement.
DerivativeCallExpression	ModelFactory.derivativeCallExpression(CIVLSource source, AbstractFunction function, List<Pair<Variable,IntegerLiteralExpression>> partials, List<Expression> arguments)	An expression for a call to the derivative of an abstract function.
DomainGuardExpression	ModelFactory.domainGuard(CIVLSource source, List<Variable> vars, Variable counter, Expression domain)	Returns a domain guard expression which is boolean expression whose arguments consists of loop variables in a CIVL $for loop and the original domain associate to the loop.
CIVLFunction	ModelFactory.function(CIVLSource source, boolean isAtomic, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, Location startLocation)	Create a new function.
LogicFunction	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).
QuantifiedExpression	ModelFactory.quantifiedExpression(CIVLSource source, QuantifiedExpression.Quantifier quantifier, List<Pair<List<Variable>,Expression>> boundVariableList, Expression restriction, Expression expression)	Creates a new quantified expression.
Scope	ModelFactory.scope(CIVLSource source, Scope parent, List<Variable> variables, CIVLFunction function)	Create a new scope.
void	CIVLFunction.setAccessesAtomicFunction(Set<Variable> set)
void	Model.setExternVariables(Map<String,Variable> externVariables)
void	CIVLFunction.setParameters(List<Variable> parameters)
void	Scope.setVariables(Set<Variable> variables)
SystemFunction	ModelFactory.systemFunction(CIVLSource source, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, String libraryName)	Generate the system function

Uses of Variable in dev.civl.mc.model.IF.expression

Methods in dev.civl.mc.model.IF.expression that return Variable

Modifier and Type	Method	Description
Variable	LambdaExpression.freeVariable()	TODO: shouldn't this be called the "bound variable"? It is the opposite of free.
Variable	DomainGuardExpression.getLiteralDomCounter()	The counter variable for iterating a literal domain step by step.
Variable	InitialValueExpression.variable()
Variable	MemoryUnitExpression.variable()
Variable	VariableExpression.variable()
Variable	DomainGuardExpression.variableAt(int index)	Returns the iteration variable of the given index.
Variable	LHSExpression.variableWritten()	Return the variable that is possible the left hand side of an assignment statement.
Variable	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.

Methods in dev.civl.mc.model.IF.expression that return types with arguments of type Variable

Modifier and Type	Method	Description
List<Pair<List<Variable>,Expression>>	ArrayLambdaExpression.boundVariableList()	The list of bound variables.
List<Pair<List<Variable>,Expression>>	QuantifiedExpression.boundVariableList()	The list of bound variables.
Set<Variable>	Expression.freeVariables()	Computes the set of variables which occur freely in this expression.
List<Pair<Variable,IntegerLiteralExpression>>	DerivativeCallExpression.partials()
Set<Variable>	Expression.variableAddressedOf()	Compute the set of variables that appear in an address-of expression.
Set<Variable>	Expression.variableAddressedOf(Scope scope)	Compute the set of variables visible from a certain scope that appear in an address-of expression.

Methods in dev.civl.mc.model.IF.expression with parameters of type Variable

Modifier and Type	Method	Description
void	VariableExpression.setVariable(Variable variable)

Uses of Variable in dev.civl.mc.model.IF.location

Methods in dev.civl.mc.model.IF.location that return types with arguments of type Variable

Modifier and Type	Method	Description
Set<Variable>	Location.writableVariables()

Method parameters in dev.civl.mc.model.IF.location with type arguments of type Variable

Modifier and Type	Method	Description
void	Location.computeWritableVariables(Set<Variable> addressedOfVariables)

Uses of Variable in dev.civl.mc.model.IF.statement

Methods in dev.civl.mc.model.IF.statement that return Variable

Modifier and Type	Method	Description
Variable	DomainIteratorStatement.getLiteralDomCounter()	Returns a counter variable used for iterating on a literal domain step by step.

Methods in dev.civl.mc.model.IF.statement that return types with arguments of type Variable

Modifier and Type	Method	Description
Set<Variable>	Statement.freeVariables()	Returns all free (not bound) variables that are referenced in this statement.
Set<Variable>	AtomicLockAssignStatement.getVariables()	Returns the set of all external variables that could be accessed in an execution of an atomic block.
List<Variable>	DomainIteratorStatement.loopVariables()	Returns the list of loop variables, ordered from left to right.
Set<Variable>	Statement.variableAddressedOf()	Obtain the set of variables whose addresses are referenced.
Set<Variable>	Statement.variableAddressedOf(Scope scope)	Obtain the set of variables visible from a certain scope that are possible to be written in the future.

Uses of Variable in dev.civl.mc.model.IF.type

Methods in dev.civl.mc.model.IF.type that return Variable

Modifier and Type	Method	Description
Variable	CIVLType.getStateVariable()	If a type is defined using a struct, union, or typedef, and it contains state, it may have to be evaluated and stored in a variable of type CIVLDynamicType.

Methods in dev.civl.mc.model.IF.type that return types with arguments of type Variable

Modifier and Type	Method	Description
Set<Variable>	CIVLType.freeVariables()

Methods in dev.civl.mc.model.IF.type with parameters of type Variable

Modifier and Type	Method	Description
void	CIVLType.setStateVariable(Variable variable)	Sets this type's state variable to the given variable

Uses of Variable in dev.civl.mc.state.IF

Methods in dev.civl.mc.state.IF that return types with arguments of type Variable

Modifier and Type	Method	Description
Map<Variable,dev.civl.sarl.IF.expr.SymbolicExpression>	StateFactory.inputVariableValueMap(State state)	Returns the map of input variable and their value at the given state; empty map if there are no input variables.

Methods in dev.civl.mc.state.IF with parameters of type Variable

Modifier and Type	Method	Description
int	State.getDyscopeID(int pid, Variable variable)	Given a process ID and a variable, finds the first dyscope containing the variable in the path starting from the dyscope of the current (top) frame of the process call stack and following the parent edges of the dyscope tree.
State	StateFactory.setVariable(State state, Variable variable, int pid, dev.civl.sarl.IF.expr.SymbolicExpression value)	Updates the value assigned to a variable in the state.
dev.civl.sarl.IF.expr.SymbolicExpression	State.valueOf(int pid, Variable variable)	Given a process ID and a variable, returns the value of the variable.