Uses of Interface
dev.civl.mc.model.IF.Sourceable

Packages that use Sourceable

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.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.variable	Submodule model.variable defines variables in CIVL.

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

Subinterfaces of Sourceable in dev.civl.mc.model.IF

Modifier and Type	Interface	Description
interface	AbstractFunction	An abstract function is an uninterpreted mathematical function.
interface	CIVLFunction	A CIVL function.
interface	Identifier	An identifier.
interface	LogicFunction	A logic function is a function whose definition (body) is either absent (i.e.
interface	Model	A model of a CIVL program.
interface	Scope	A scope.
interface	SystemFunction	A system function is a function that is implemented in a library executor, not in source code.

Constructors in dev.civl.mc.model.IF with parameters of type Sourceable

Modifier	Constructor	Description
	CIVLInternalException(String s, Sourceable sourceable)
	CIVLSyntaxException(String message, Sourceable sourceable)
	CIVLUnimplementedFeatureException(String feature, Sourceable sourceable)

Uses of Sourceable in dev.civl.mc.model.IF.contract

Subinterfaces of Sourceable in dev.civl.mc.model.IF.contract

Modifier and Type	Interface	Description
interface	CallEvent	This represents a function call event of a depends clause.
interface	CompositeEvent	This represents a composite event, which could be a union/difference/intersect of another two depends events.
interface	DependsEvent	This represents an event which is used as one argument of the depends clause.
interface	FunctionBehavior	This represents a non-named behavior of the ACSL function contract.
interface	FunctionContract	This represents a block of ACSL contract for a function.
interface	LoopContract	This class represents a group of loop annotations for a loop, including loop invariants, loop assigns and loop variants.
interface	MemoryEvent	This represents a \read or \write event of a depends clause.
interface	NamedFunctionBehavior	A named behavior contains a name and assumptions in addition to those components contained by FunctionBehavior.

Uses of Sourceable in dev.civl.mc.model.IF.expression

Subinterfaces of Sourceable in dev.civl.mc.model.IF.expression

Modifier and Type	Interface	Description
interface	AbstractFunctionCallExpression	An expression representing a call of an abstract function.
interface	AddressOfExpression	This represents an address-of expression, which contains one operand, and has the format: invalid input: '&x', where invalid input: '&' is the address-of operator and x is the operand.
interface	ArrayLambdaExpression	A CIVL-C quantified expression, including three components, bound variable declaration list, (optional) restriction and expression.
interface	BinaryExpression	A binary operation.
interface	BooleanLiteralExpression	A literal boolean value.
interface	BoundVariableExpression	A bound variable is a variable used in a quantified expression.
interface	CastExpression	A cast of an expression to a different type.
interface	CharLiteralExpression
interface	CompoundLiteralExpression	This class represents compound literal expressions, including string literals.
interface	ConditionalExpression	The ternary conditional expression ("?" in C).
interface	DereferenceExpression
interface	DerivativeCallExpression	An uninterpreted call to the derivative of an abstract function.
interface	DifferentiableExpression	This expression encodes the claim that a real, abstract function is differentiable.
interface	DomainGuardExpression	This is the guard expression of CIVL for loops ($for).
interface	DotExpression	A dot expression is a reference to a field in a struct or union.
interface	DynamicTypeOfExpression	A "DynamicTypeOf" expression.
interface	Expression	The parent of all expressions.
interface	ExtendedQuantifiedExpression	The representation for the "fold expression" in ACSL, e.g.
interface	FunctionCallExpression
interface	FunctionGuardExpression	A function guard expression is the guard expression of a function call with a function pointer.
interface	FunctionIdentifierExpression
interface	HereOrRootExpression
interface	InitialValueExpression	An expression yielding the initial value of a variable.
interface	IntegerLiteralExpression	An integer literal.
interface	LambdaExpression	A CIVL-C quanti, bound variable declaration list, (optional) restriction and expression.
interface	LHSExpression	A left-hand-side expression.
interface	LiteralExpression	The parent of all literal expressions.
interface	MemoryUnitExpression	A memory unit expression is an expression that represents (part of) the memory related to some variable.
interface	Nothing
interface	ProcnullExpression
interface	QuantifiedExpression	A CIVL-C quantified expression, including three components, bound variable declaration list, (optional) restriction and expression.
interface	RealLiteralExpression	A real literal.
interface	RecDomainLiteralExpression	This is a rectangular domain literal expression, which is the Cartesian product of a number of ranges, e.g., {range1, range2, range3, ...}.
interface	RegularRangeExpression	Represents a CIVL-C regular range expression, which has the form lo ..
interface	ScopeofExpression	A scopeof expression is "$scopeof(expr)".
interface	SelfExpression	Self expression.
interface	SizeofExpression	An expression of the form "sizeof(e)" where e is an expression.
interface	SizeofTypeExpression	An expression of the form "sizeof(t)" where t is a type.
interface	StatenullExpression	This class represents a $state_null constant expression.
interface	SubscriptExpression	a[i], where "a" is an array and "i" is an expression evaluating to an integer.
interface	SystemGuardExpression	A system guard expression is a pseudo guard expression for system function calls.
interface	UnaryExpression	A unary operation.
interface	UndefinedProcessExpression	Self expression.
interface	VariableExpression	A use of a variable in an expression.
interface	WildcardExpression	This represents the expression ..., which is used only in contracts and stands for an expression of any type whose value is ignored.

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

Subinterfaces of Sourceable in dev.civl.mc.model.IF.location

Modifier and Type	Interface	Description
interface	Location	The parent of all locations.

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

Subinterfaces of Sourceable 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	Statement	The parent of all statements.
interface	UpdateStatement

Uses of Sourceable in dev.civl.mc.model.IF.variable

Subinterfaces of Sourceable in dev.civl.mc.model.IF.variable

Modifier and Type	Interface	Description
interface	Variable	A static variable.