Uses of Interface
dev.civl.mc.model.IF.contract.LoopContract

Packages that use LoopContract

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.statement	Submodule model.statement defines a statement of a CIVL-C program.

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

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

Modifier and Type	Method	Description
LoopContract	ModelFactory.loopContract(CIVLSource civlSource, Location loopLocation, List<Expression> loopInvariants, List<LHSExpression> loopAssigns, List<Expression> loopVariants)	Creates a LoopContract instance

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

Modifier and Type	Method	Description
NoopStatement	ModelFactory.loopBranchStatement(CIVLSource civlSource, Location source, Expression guard, boolean isTrue, LoopContract loopContract)	An loop branch statement is introduced when translating a loop.

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

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

Modifier and Type	Method	Description
LoopContract	LoopBranchStatement.getLoopContract()	Returns an instance of LoopContract if LoopBranchStatement.isContracted() returns true, otherwise, returns null.