Uses of Package
dev.civl.mc.model.IF.contract

Packages that use dev.civl.mc.model.IF.contract

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.

Classes in dev.civl.mc.model.IF.contract used by dev.civl.mc.model.IF

Class	Description
FunctionContract	This represents a block of ACSL contract for a function.
LoopContract	This class represents a group of loop annotations for a loop, including loop invariants, loop assigns and loop variants.

Classes in dev.civl.mc.model.IF.contract used by dev.civl.mc.model.IF.contract

Class	Description
CallEvent	This represents a function call event of a depends clause.
CompositeEvent	This represents a composite event, which could be a union/difference/intersect of another two depends events.
CompositeEvent.CompositeEventOperator
DependsEvent	This represents an event which is used as one argument of the depends clause.
DependsEvent.DependsEventKind
FunctionBehavior	This represents a non-named behavior of the ACSL function contract.
FunctionContract	This represents a block of ACSL contract for a function.
FunctionContract.ContractKind	ContractKind: This kind is used to denotes all kinds of contracts.
MemoryEvent	This represents a \read or \write event of a depends clause.
NamedFunctionBehavior	A named behavior contains a name and assumptions in addition to those components contained by FunctionBehavior.

Classes in dev.civl.mc.model.IF.contract used by dev.civl.mc.model.IF.statement

Class	Description
LoopContract	This class represents a group of loop annotations for a loop, including loop invariants, loop assigns and loop variants.