Uses of Interface
dev.civl.mc.model.IF.location.Location

Packages that use Location

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.contract
dev.civl.mc.model.IF.statement	Submodule model.statement defines a statement of a CIVL-C program.
dev.civl.mc.state.IF	Module state is responsible for the creation and manipulation of states of a CIVL model.

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

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

Modifier and Type	Method	Description
Location	ModelFactory.location(CIVLSource source, Scope scope)	Create a new location.
Location	Model.sleepLocation()
Location	CIVLFunction.startLocation()
Location	Fragment.startLocation()

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

Modifier and Type	Method	Description
Set<Location>	CIVLFunction.locations()

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

Modifier and Type	Method	Description
void	CIVLFunction.addLocation(Location location)
AssignStatement	ModelFactory.assignStatement(CIVLSource civlSource, Location source, LHSExpression lhs, Expression rhs, boolean isInitializer)	An assignment statement.
Statement	ModelFactory.atomicEnter(Location loc)	Generate an atomic enter statement
Statement	ModelFactory.atomicExit(Location loc)	Generate an atomic exit statement
Fragment	ModelFactory.atomicFragment(Fragment fragment, Location start, Location end)	Generate an atomic fragment based on a certain fragment, by adding one location at before and after the fragment to denote the boundary of the atomic block
CallOrSpawnStatement	ModelFactory.callOrSpawnStatement(CIVLSource sourceOf, Location location, boolean isCall, Expression function, List<Expression> arguments, Expression guard, boolean isInitializer)	Creates a call or spawn statement.
Fragment	ModelFactory.civlForEnterFragment(CIVLSource source, Location src, Expression dom, List<Variable> variables, Variable counter)	Returns a new fragment containing a CivlForStatement.
CivlParForSpawnStatement	ModelFactory.civlParForEnterStatement(CIVLSource source, Location location, Expression domain, VariableExpression domSize, VariableExpression procsVar, CIVLFunction parProcFunc)	creates a $parfor enter statement to start the execution of the $parfor.
void	ModelFactory.computeImpactScopeOfLocation(Location location)	Computes the impact scope of a location, which is the highest scope that the location accesses.
CIVLFunction	ModelFactory.function(CIVLSource source, boolean isAtomic, Identifier name, Scope parameterScope, List<Variable> parameters, CIVLType returnType, Scope containingScope, Location startLocation)	Create a new function.
NoopStatement	ModelFactory.gotoBranchStatement(CIVLSource civlSource, Location source, String label)	A goto branch statement is of the form goto label; .
NoopStatement	ModelFactory.ifElseBranchStatement(CIVLSource civlSource, Location source, Expression guard, boolean isIf)	An if-else branch statement is introduced to translate if-else statement.
NoopStatement	ModelFactory.loopBranchStatement(CIVLSource civlSource, Location source, Expression guard, boolean isTrue, LoopContract loopContract)	An loop branch statement is introduced when translating a loop.
LoopContract	ModelFactory.loopContract(CIVLSource civlSource, Location loopLocation, List<Expression> loopInvariants, List<LHSExpression> loopAssigns, List<Expression> loopVariants)	Creates a LoopContract instance
MallocStatement	ModelFactory.mallocStatement(CIVLSource civlSource, Location source, LHSExpression lhs, CIVLType staticElementType, Expression scopeExpression, Expression sizeExpression, int mallocId, Expression guard)	Create a new malloc statement
NoopStatement	ModelFactory.noopStatement(CIVLSource civlSource, Location source, Expression expression)	A noop statement with the default guard of true.
NoopStatement	ModelFactory.noopStatementForVariableDeclaration(CIVLSource civlSource, Location source)	A temporary noop statement with the true guard
NoopStatement	ModelFactory.noopStatementTemporary(CIVLSource civlSource, Location source)	A temporary noop statement with the true guard
NoopStatement	ModelFactory.noopStatementWtGuard(CIVLSource civlSource, Location source, Expression guard)	A noop statement with an explicit guard expression.
Fragment	ModelFactory.returnFragment(CIVLSource civlSource, Location source, Expression expression, CIVLFunction function)	Create a one-statement fragment that contains the return statement.
void	Model.setSleepLocation(Location sleep)
void	CIVLFunction.setStartLocation(Location startLocation)
void	Fragment.setStartLocation(Location location)	Update the start location of this fragment
NoopStatement	ModelFactory.switchBranchStatement(CIVLSource civlSource, Location source, Expression guard)	Creates a switch branch statement for the default case, which is a subclass of no-op statement.
NoopStatement	ModelFactory.switchBranchStatement(CIVLSource civlSource, Location source, Expression guard, Expression label)	Creates a switch branch statement for a labeled case.
void	Fragment.updateStartLocation(Location newLocation)	Update the start location with a new location
UpdateStatement	ModelFactory.updateStatement(CIVLSource source, Location srcLoc, Expression guard, Expression collator, CIVLFunction function, Expression[] arguments)
UpdateStatement	ModelFactory.updateStatement(CIVLSource source, Location srcLoc, Expression guard, Expression collator, CallOrSpawnStatement call)	Creates an $update statement.

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

Modifier and Type	Method	Description
void	CIVLFunction.setLocations(Set<Location> locations)

Uses of Location in dev.civl.mc.model.IF.contract

Methods in dev.civl.mc.model.IF.contract that return Location

Modifier and Type	Method	Description
Location	LoopContract.loopLocation()	Returns the location which identifies the corresponding loop.

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

Modifier and Type	Method	Description
void	LoopContract.setLocation(Location loopLocation)	Set the location which identifies a loop statement.

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

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

Modifier and Type	Method	Description
Location	Statement.source()
Location	Statement.target()

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

Modifier and Type	Method	Description
void	Statement.setSource(Location source)
void	Statement.setSourceTemp(Location source)	updates the source location of this statement, but never add this statement to the outgoing set of the source location
void	Statement.setTarget(Location target)
void	Statement.setTargetTemp(Location target)	updates the target location of this statement, but never add this statement to the incoming set of the target location

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

Methods in dev.civl.mc.state.IF that return Location

Modifier and Type	Method	Description
Location	ProcessState.getLocation()	Returns the location at the top of the call stack of this process.
Location	StackEntry.location()	Returns the static location component of this activation frame.

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

Modifier and Type	Method	Description
State	StateFactory.setLocation(State state, int pid, Location location)	Sets the location of a process.
State	StateFactory.setLocation(State state, int pid, Location location, boolean accessChanged)	Sets the location of a process.