Module dev.civl.abc
Package dev.civl.abc.ast.node.IF.acsl
package dev.civl.abc.ast.node.IF.acsl
-
ClassDescriptionThis represents an ACSL allocation clause, which has the syntax
allocates p1, p2, p3;
or
frees p1, p2, p3;This represents ACSL-CIVLC\anyactaction to be used independscontract clauses.An ACSLassignsor ACSL-CIVLCreadsclause specifies a set of existing memory units.This represents an ACSLassumesclause, which has the following syntax:This represents a named behavior of the ACSL specification.An event that represents a function call with certain arguments, which is a kind of Depends Event.This represents the completeness clause of ACSL, which could be eithercompleteordisjointAn composite eventThe operator of a composite eventA contract node represents an element that may occur in a procedure contract.The kinds of contract nodesThis represents an event of thedependsclause.Adependsclause specifies part of the dependence relation used in partial order reduction (POR).An "ensures" clause in a procedure contract clause that represents a post-condition.This represents an ACSL extended quantification expression.This represents aguardsclause that specifies a guard for a function.A depends event which specifies reading or writing a list of memory units.This represents the no-act event\noact, which is an event ofdependsclauses.Constant$nothing, argument of$assigns / $readscontract clauses.This represents a$object_ofof$region_ofexpression.The ACSL predicate node, which in the view of ABC, is just a function with a boolean return type.Arequiresclause in a CIVL-C procedure contract.