Package edu.udel.cis.vsl.abc.ast.node.IF.acsl

package edu.udel.cis.vsl.abc.ast.node.IF.acsl

Related Packages

Package	Description
edu.udel.cis.vsl.abc.ast.node.IF	Submodule ast.node defines every kind of node in an AST.

Class	Description
AllocationNode	This represents an ACSL allocation clause, which has the syntax allocates p1, p2, p3; or frees p1, p2, p3;
AnyactNode	This represents ACSL-CIVLC \anyact action to be used in depends contract clauses.
AssignsOrReadsNode	An ACSL assigns or ACSL-CIVLC reads clause specifies a set of existing memory units.
AssumesNode	This represents an ACSL assumes clause, which has the following syntax:
BehaviorNode	This represents a named behavior of the ACSL specification.
CallEventNode	An event that represents a function call with certain arguments, which is a kind of Depends Event.
CompletenessNode	This represents the completeness clause of ACSL, which could be either complete or disjoint
CompositeEventNode	An composite event
CompositeEventNode.EventOperator	The operator of a composite event
ContractNode	A contract node represents an element that may occur in a procedure contract.
ContractNode.ContractKind	The kinds of contract nodes
DependsEventNode	This represents an event of the depends clause.
DependsEventNode.DependsEventNodeKind
DependsNode	A depends clause specifies part of the dependence relation used in partial order reduction (POR).
EnsuresNode	An "ensures" clause in a procedure contract represents a post-condition.
ExtendedQuantifiedExpressionNode	This represents an ACSL extended quantification expression.
ExtendedQuantifiedExpressionNode.ExtendedQuantifier
GuardsNode	This represents a guards clause that specifies a guard for a function.
InvariantNode
MemoryEventNode	A depends event which specifies reading or writing a list of memory units.
MemoryEventNode.MemoryEventNodeKind
MPICollectiveBlockNode	An contract block introduced by the mpi_collective(MPI_Comm, Kind): contract constructor.
MPICollectiveBlockNode.MPICommunicatorMode
MPIContractAbsentEventNode	This ContractNode represents an "mpi event", which represents a set of specific actions that a process performs during runtime.
MPIContractAbsentEventNode.MPIAbsentEventKind	The kinds of the events.
MPIContractAbsentNode	This MPIContractExpressionNode denotes an MPI absent expression, which states a path predicate for an MPI collective-style function.
MPIContractConstantNode
MPIContractConstantNode.MPIConstantKind
MPIContractExpressionNode
MPIContractExpressionNode.MPIContractExpressionKind
NoactNode	This represents the no-act event \noact, which is an event of depends clauses.
NothingNode	Constant $nothing, argument of $assigns / $reads contract clauses.
ObjectOrRegionOfNode	This represents a $object_of of $region_of expression.
PredicateNode	The ACSL predicate node, which in the view of ABC, is just a function with a boolean return type.
RequiresNode	A requires clause in a CIVL-C procedure contract.
WaitsforNode