Module dev.civl.mc

Package dev.civl.mc.model.IF.statement

Interface LoopBranchStatement

All Superinterfaces:

NoopStatement, Sourceable, Statement

public interface LoopBranchStatement
extends NoopStatement

Nested Class Summary

Nested classes/interfaces inherited from interface dev.civl.mc.model.IF.statement.NoopStatement

NoopStatement.NoopKind

Nested classes/interfaces inherited from interface dev.civl.mc.model.IF.statement.Statement

Statement.StatementKind

Method Summary

Modifier and Type	Method	Description
LoopContract	getLoopContract()	Returns an instance of LoopContract if isContracted() returns true, otherwise, returns null.
boolean	isContracted()	Returns true if and only if this loop is attached with LoopContract
boolean	isEnter()	Is this the loop enter or exit statement?

Methods inherited from interface dev.civl.mc.model.IF.statement.NoopStatement

expression, isRemovable, isTemporary, isVariableDeclaration, noopKind, setRemovable

Methods inherited from interface dev.civl.mc.model.IF.Sourceable

getSource

Methods inherited from interface dev.civl.mc.model.IF.statement.Statement

calculateConstantValue, calculateDerefs, containsHere, freeVariables, guard, hasDerefs, isPurelyLocal, locationStepString, lowestScope, model, purelyLocalAnalysisOfVariables, reachable, reached, replaceWith, replaceWith, setCIVLSource, setGuard, setModel, setSource, setSourceTemp, setTarget, setTargetTemp, source, statementKind, statementScope, summaryOfSource, target, toStepString, variableAddressedOf, variableAddressedOf

Method Details

isEnter

boolean isEnter()

Is this the loop enter or exit statement?

Returns:

True iff this is the loop enter branch.

isContracted

boolean isContracted()

Returns true if and only if this loop is attached with LoopContract

Returns:

getLoopContract

LoopContract getLoopContract()

Returns an instance of LoopContract if isContracted() returns true, otherwise, returns null.

Returns: