Uses of Interface
dev.civl.mc.model.IF.statement.Statement

Packages that use Statement

Package	Description
dev.civl.mc.analysis.IF	Module analysis provides a list of analyzers for static/runtime analyzing of a program.
dev.civl.mc.kripke.IF	Module kripke provides the definition of various transitions and the enabler and state manager of CIVL.
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.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.semantics.IF	Module semantics implements the semantics of CIVL-C.

Uses of Statement in dev.civl.mc.analysis.IF

Methods in dev.civl.mc.analysis.IF with parameters of type Statement

Modifier and Type	Method	Description
static void	Analysis.staticAnalysis(Statement statement, List<CodeAnalyzer> analyzers)	performs static analysis on the given statement to decide if any code analysis provided by the specified code analyzers is needed.
void	CodeAnalyzer.staticAnalysis(Statement statement)	Static analysis of the given statement.

Uses of Statement in dev.civl.mc.kripke.IF

Methods in dev.civl.mc.kripke.IF with parameters of type Statement

Modifier and Type	Method	Description
dev.civl.sarl.IF.expr.BooleanExpression	Enabler.getGuard(Statement statement, int pid, State state)	Computes the guard of a statement.

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

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

Modifier and Type	Method	Description
Statement	ModelFactory.atomicEnter(Location loc)	Generate an atomic enter statement
Statement	ModelFactory.atomicExit(Location loc)	Generate an atomic exit statement
Statement	Fragment.uniqueFinalStatement()	Precondition: finalStatements().size() == 1

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

Modifier and Type	Method	Description
Set<Statement>	Fragment.finalStatements()
Set<Statement>	CIVLFunction.statements()

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

Modifier and Type	Method	Description
void	ModelFactory.addAnonStatement(Statement statment)	Add the given statement to the anonymous fragment.
void	Fragment.addFinalStatement(Statement statement)	Add a statement to the final statement set
void	Fragment.addNewStatement(Statement statement)	Add a new statement to the fragment, which will be considered the subsequent statement of the current final statements.s
void	CIVLFunction.addStatement(Statement statement)

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

Modifier and Type	Method	Description
void	Fragment.addFinalStatementSet(Set<Statement> stmtSet)	Add a set of statements to the final statement set
void	Fragment.setFinalStatements(Set<Statement> statements)	Update the last statement of this fragment
void	CIVLFunction.setStatements(Set<Statement> statements)

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

Methods in dev.civl.mc.model.IF.location that return Statement

Modifier and Type	Method	Description
Statement	Location.getIncoming(int i)
Statement	Location.getOutgoing(int i)
Statement	Location.getSoleOutgoing()	Returns the sole outgoing statement from this location.

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

Modifier and Type	Method	Description
Iterable<Statement>	Location.incoming()
Iterable<Statement>	Location.outgoing()

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

Modifier and Type	Method	Description
void	Location.addIncoming(Statement statement)
void	Location.addOutgoing(Statement statement)
void	Location.removeIncoming(Statement statement)	Remove a certain incoming statement
void	Location.removeOutgoing(Statement statement)	Remove a certain outgoing statement

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

Subinterfaces of Statement in dev.civl.mc.model.IF.statement

Modifier and Type	Interface	Description
interface	AssignStatement	An assignment statement.
interface	AtomicLockAssignStatement
interface	CallOrSpawnStatement	A function call or spawn.
interface	CivlParForSpawnStatement	This represents the first part of a $parfor construct, i.e., spawning processes according the specified domain.
interface	DomainIteratorStatement	Updates the loop variables with the next element of a domain.
interface	LoopBranchStatement
interface	MallocStatement	A statement for dynamic allocation of objects.
interface	NoopStatement	Marker interface for a noop statement.
interface	ParallelAssignStatement
interface	ReturnStatement	A return statement.
interface	UpdateStatement

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

Modifier and Type	Method	Description
Statement	Statement.replaceWith(ConditionalExpression oldExpression, Expression newExpression)	Return a new statement by copying this statement and modifying it as well as its guard by replacing a certain conditional expression with a expression, used when translating away conditional expression WITHOUT introducing temporary variables.

Uses of Statement in dev.civl.mc.semantics.IF

Methods in dev.civl.mc.semantics.IF that return Statement

Modifier and Type	Method	Description
Statement	Transition.statement()	The statement that this transition is to execute, which should be atomic, deterministic, and enabled in the context of the path condition.

Methods in dev.civl.mc.semantics.IF with parameters of type Statement

Modifier and Type	Method	Description
static dev.civl.mc.semantics.common.NoopTransition	Semantics.newNoopTransition(int pid, dev.civl.sarl.IF.expr.BooleanExpression assumption, Statement statement, boolean symplifyState)	Create a new NoopTransition whose statement will not be executed.
static Transition	Semantics.newTransition(int pid, dev.civl.sarl.IF.expr.BooleanExpression clause, Statement statement)	Creates a new regular Transition whose statement will be executed by executor.
static Transition	Semantics.newTransition(int pid, dev.civl.sarl.IF.expr.BooleanExpression clause, Statement statement, boolean simplifyState)	Creates a new regular Transition whose statement will be executed by executor.
StringBuffer	SymbolicAnalyzer.statementEvaluation(State preState, State postState, int pid, Statement statement)