Module dev.civl.mc

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

package dev.civl.mc.model.IF.contract

Related Packages

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.expression	Submodule model.expression defines expression in CIVL.
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.model.IF.type	Submodule model.type defines types in CIVL.
dev.civl.mc.model.IF.variable	Submodule model.variable defines variables in CIVL.

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
ContractFactory	This factory is to create new instances of function contract components.
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.
LoopContract	This class represents a group of loop annotations for a loop, including loop invariants, loop assigns and loop variants.
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.