Module dev.civl.abc
Package dev.civl.abc.ast.node.IF

Interface NodeFactory

public interface NodeFactory

The factory used to construct the nodes of Abstract Syntax Trees.

The user constructs the nodes of an AST using the methods in this class. These nodes have the structure of a tree, the root node being the node representing the translation unit or program; the children of the root node correspond to the "external definitions" of the unit. Once these have been constructed, the ASTFactory.newAST(dev.civl.abc.ast.node.IF.SequenceNode<dev.civl.abc.ast.node.IF.statement.BlockItemNode>, java.util.Collection<dev.civl.abc.token.IF.SourceFile>, boolean) method is invoked on the root node to actually construct the AST object. This performs a number of analyses and stores additional information about the AST. A number of errors can be detected and reported at this stage. Among other things, this also computes the abstract "type" of every variable, function, and expression. It also computes the scope and linkage of all identifiers.

After the AST is created, the AST (and all of its nodes) become immutable. Every node has an "owner" (originally null), which is set to the new AST object at this time. If you want to modify the tree, you must first invoke the AST.release() method, which frees the nodes from ownership by the AST object, setting the "owner" fields again to null. They can then be modified, and then ASTFactory.newAST(dev.civl.abc.ast.node.IF.SequenceNode<dev.civl.abc.ast.node.IF.statement.BlockItemNode>, java.util.Collection<dev.civl.abc.token.IF.SourceFile>, boolean) called again to re-analylze and re-build an AST. Alternatively, you can also clone the tree, if you want to keep the old AST around for some reason.

Finally, one or more ASTs can be combined to form a complete "program" using the newProgram method. This corresponds to "linking" in the usual compiler sense. (Not yet implemented.)

  • Method Details

    • getCivlOmpDependKey

      AttributeKey getCivlOmpDependKey(Boolean isSource)
      Parameters:
      isSource - if true then returns the AttributeKey of CIVL OpenMP depend source; otherwise depend target
      Returns:
      the AttributeKey which stores CIVL OpenMP dependency relationship

    • getTempCountKey

      AttributeKey getTempCountKey()
      Returns:
      the AttributeKey which stores the number of temporary variables in an AST.

    • newAttribute

      AttributeKey newAttribute(String attributeName, Class<? extends Object> attributeClass)
      Creates an attribute slot for all AST nodes. This is a mechanism for extending the functionality of nodes. This may be used to hang any kind of data onto nodes. Initially, the attribute value associated to the new key will be null in every node.
      Parameters:
      attributeName - a name for the new attribute, unique among all attribute names
      attributeClass - the class to which attribute values of the new kind will belong
      Returns:
      a new attribute key which can be used to assign attribute values to nodes

    • newSequenceNode

      <T extends ASTNode> SequenceNode<T> newSequenceNode(Source source, String name, List<T> nodes)
      Creates a new sequence node, i.e., a node which has some finite ordered sequence of children belonging to a particular class.
      Parameters:
      source - source information for the whole sequence
      name - a name to use when printing this sequence node
      nodes - a list of nodes that will form the children of the new sequence node
      Returns:
      the new sequence node with the children set

    • newPairNode

      <S extends ASTNode, T extends ASTNode> PairNode<S,T> newPairNode(Source source, S node1, T node2)
      Creates a new ordered pair node, i.e., a node with exactly two children belonging to two specific classes.
      Parameters:
      node1 - the first child node
      node2 - the second child node
      Returns:
      the new pair node with the children set

    • newIdentifierNode

      IdentifierNode newIdentifierNode(Source source, String name)
      Constructs and returns a new identifier node with given source object and name.
      Parameters:
      source - source information for the identifier use
      name - the name of this identifier
      Returns:
      a new identifier node

    • newBasicTypeNode

      BasicTypeNode newBasicTypeNode(Source source, StandardBasicType.BasicTypeKind kind)
      Returns a new type node for a basic type.
      Parameters:
      source - source information for the occurrence of the basic type
      kind - the kind of the basic type
      Returns:
      the new basic type node

    • newVoidTypeNode

      TypeNode newVoidTypeNode(Source source)
      Returns a new void type node.
      Parameters:
      source - source information for the occurrence of "void"
      Returns:
      the new void type node

    • newEnumerationTypeNode

      EnumerationTypeNode newEnumerationTypeNode(Source source, IdentifierNode tag, SequenceNode<EnumeratorDeclarationNode> enumerators)
      Constructs and returns a new enumeration type node.
      Parameters:
      source - source information for the occurrence of the enumeration type
      tag - the enumeration tag, i.e., the name of the enumeration, the string that follows enum
      enumerators -
      Returns:
      the new enumeration type node

    • newArrayTypeNode

      ArrayTypeNode newArrayTypeNode(Source source, TypeNode elementType, ExpressionNode extent)
      Constructs and returns a new array type node.
      Parameters:
      source - source information for the occurrence of the array type
      elementType - the node representing the element type
      extent - the node representing the expression in square brackets, i.e., the array length or "extent"
      Returns:
      the new array type node

    • newArrayTypeNode

      ArrayTypeNode newArrayTypeNode(Source source, TypeNode elementType, ExpressionNode extent, ExpressionNode startIndex)
      Constructs and returns a new array type node.
      Parameters:
      source - source information for the occurrence of the array type
      elementType - the node representing the element type
      extent - the node representing the expression in square brackets, i.e., the array length or "extent"
      startIndex - the node representing the expression in square brackets, i.e, the array starting index
      Returns:
      the new array type node

    • newAtomicTypeNode

      AtomicTypeNode newAtomicTypeNode(Source source, TypeNode baseType)
      Constructs and returns a new atomic type node.
      Parameters:
      source - the source information for the occurrence of the atomic type
      baseType - the base type, i.e., the type modified by the "atomic"
      Returns:
      the new atomic type node

    • newPointerTypeNode

      PointerTypeNode newPointerTypeNode(Source source, TypeNode referencedType)
      Constructs and returns a new pointer type node.
      Parameters:
      source - source information for the occurrence of the pointer type
      referencedType - the type pointed to
      Returns:
      the new pointer type node

    • newStructOrUnionTypeNode

      StructureOrUnionTypeNode newStructOrUnionTypeNode(Source source, boolean isStruct, IdentifierNode tag, SequenceNode<FieldDeclarationNode> structDeclList)
      Constructs and returns a new structure or union type node.
      Parameters:
      source - source information for the occurrence of the structure or union type node
      isStruct - true for a structure type, false for a union type
      tag - the tag of the structure or union, i.e., the string that follows struct or union. Maybe null.
      structDeclList - the sequence of field declarations; may be null
      Returns:
      the new structure or union type node

    • newFunctionTypeNode

      FunctionTypeNode newFunctionTypeNode(Source source, TypeNode returnType, SequenceNode<VariableDeclarationNode> formals, boolean hasIdentifierList)
      Constructs and returns a new function type node.
      Parameters:
      source - source information for the occurrence of the function type
      returnType - the node representing the return type of the function type
      formals - the sequence of formal parameter declaration nodes for the function type. This parameter cannot be null. If there are no formals then it must be a sequence node with an empty list.
      hasIdentifierList - true if the function is declared using an identifier list (i.e., without types associated to the parameters); false if the function is declared with a parameter declaration list
      Returns:
      the function type node

    • newScopeTypeNode

      TypeNode newScopeTypeNode(Source source)
      Returns a new scope type node ("$scope"). This is a CIVL-C type.
      Parameters:
      source - source information for the occurrence of $scope
      Returns:
      the new instance of scope type

    • newMemTypeNode

      TypeNode newMemTypeNode(Source source)
      Returns a new mem type node ("$mem"). This is a CIVL-C type.
      Parameters:
      source - source information for the occurrence of $mem
      Returns:
      the new instance of mem type node

    • newTypedefNameNode

      TypedefNameNode newTypedefNameNode(IdentifierNode name, SequenceNode<ExpressionNode> scopeList)
      Returns a new instance of a typedef name node. This is a use of a typedef name. The source is the same as that of the identifier name.
      Parameters:
      name - the identifier node representing the use of the typedef name
      scopeList - optional CIVL-C construct: list of scope parameters used to instantiate a scope-parameterized typedef
      Returns:
      the new typedef name node wrapping the given identifier node

    • newRangeTypeNode

      TypeNode newRangeTypeNode(Source source)
      Returns a new instance of range type node; this is the CIVL-C type $range.
      Parameters:
      source - source information for the occurrence of $domain
      Returns:
      the new range type node

    • newDomainTypeNode

      DomainTypeNode newDomainTypeNode(Source source)
      Returns a new instance of domain type node, with no dimension specified; this is the CIVL-C type $domain.
      Parameters:
      source - source information for the occurrence of $domain
      Returns:
      the new domain type node instance

    • newLambdaTypeNode

      LambdaTypeNode newLambdaTypeNode(Source source, TypeNode freeVariableType, TypeNode lambdaFunctionType)

    • newDomainTypeNode

      DomainTypeNode newDomainTypeNode(Source source, ExpressionNode dimension)
      Returns a new instance of the domain type node with given integer dimension; this is the CIVL-C type $domain(n), where n is the domain dimension. This is a subtype of $domain.
      Parameters:
      source - source information for the occurrence of $domain
      dimension - the dimension of the domain, i.e., the arity of the tuples which comprise the domain
      Returns:
      the new domain type node instance

    • getConstantValue

      Value getConstantValue(ExpressionNode expression) throws SyntaxException
      If the expression can be evaluated statically to yield a constant value, this method returns that value, else it returns null. Every "constant expression" will yield a (non-null) value, but other expressions not strictly considered "constant expressions" may also yield non-null constant values. Hence if method isConstantExpression() returns true, this method should return a non-null value; if isConstantExpression() returns false, this method may or may not return a non-null value.
      Parameters:
      expression - an expression node
      Returns:
      the constant value obtained by evaluating this expression, or null if the expression cannot be evaluated
      Throws:
      SyntaxException

    • setConstantValue

      void setConstantValue(ExpressionNode expression, Value value)
      If for some reason you know what the constant value of a node is supposed to be, tell it by invoking this method.
      Parameters:
      expression - the expression node that has been determined to have a constant value
      value - the constant vale to associate to that expression node

    • newCharacterConstantNode

      CharacterConstantNode newCharacterConstantNode(Source source, String representation, ExecutionCharacter character)
      Returns a new character constant node. A character constant is a literal charcter in a program, something like 'a'. C distinguishes between characters in the source code, and "execution characters" which are encoded in various ways by source code elements. Unicode characters can all be encoded using appropriate escape sequences.
      Parameters:
      source - the source information for the occurrence of the character constant
      representation - the way the character literal actually appears in the program source code
      character - the execution character represented by the character constant
      Returns:
      the new character constant node

    • newStringLiteralNode

      StringLiteralNode newStringLiteralNode(Source source, String representation, StringLiteral literal)
      Constructs a new string literal node. A string literal occurs in the program source code as "...".
      Parameters:
      source - the source information for the occurrence of the string literal. The string literal is usually a single token.
      representation - the way the string literal actually appears in the program source code, with escape sequences intact
      literal - the string literal object obtained by interpreting the representation
      Returns:
      the new string literal node

    • newIntegerConstantNode

      IntegerConstantNode newIntegerConstantNode(Source source, String representation) throws SyntaxException
      Constructs a new integer constant node. An integer constant is an occurrence of a literal integer in the source, which encodes a concrete integer value. The C11 Standard specifies the format for integer constants, which includes various letter suffixes that can occur at the end of the constant, in Sec. 6.4.4.1. The integer constant value is constructed by interpreting the representation.
      Parameters:
      source - the source information for the integer constant
      representation - the way the integer actually appears in the program source code
      Returns:
      the new integer constant node
      Throws:
      SyntaxException - if the representation does not conform to the format specified in the C11 Standard

    • newIntConstantNode

      IntegerConstantNode newIntConstantNode(Source source, int value)
      A special case of newIntegerConstantNode(Source, String) where the 2nd arg is an integer, and the type of this IntegerConstantNode is int.
      Parameters:
      source - The source information for the integer constant
      value - The value of the integer constant.
      Returns:
      The new integer constant node

    • newFloatingConstantNode

      FloatingConstantNode newFloatingConstantNode(Source source, String representation, String wholePart, String fractionPart, String exponent, FloatingValue value)
      Constructs a new floating constant node. A floating constant is an occurrence of a literal floating point number in the source, which encodes a concrete floating point value. The C Standard specifies the format for floating constants, which includes various letter suffixes that can occur at the end of the constant, in Sec. 6.4.4.2.

    • newFloatingConstantNode

      FloatingConstantNode newFloatingConstantNode(Source source, String representation) throws SyntaxException
      Constructs a new floating constant node. A floating constant is an occurrence of a literal floating point number in the source, which encodes a concrete floating point value. The C11 Standard specifies the format for floating constants, which includes various letter suffixes that can occur at the end of the constant, in Sec. 6.4.4.2. The floating constant value is constructed by interpreting the representation.
      Parameters:
      source - the source information for the floating constant
      representation - the way the floating constant actually appears in the program source code
      Returns:
      the new floating constant node
      Throws:
      SyntaxException - if the representation does not conform to the format specified in the C11 Standard

    • newEnumerationConstantNode

      EnumerationConstantNode newEnumerationConstantNode(IdentifierNode name)
      Constructs a new enumeration constant node. This represents an occurrence of an enumeration constant, i.e., a use of a previously declared enumerator, in the program. This node just wraps an identifier node. The source is same as that of identifier.
      Parameters:
      name - the identifier node which is the occurrence of the enumeration constant
      Returns:
      the new enumeration constant node

    • newCompoundLiteralNode

      CompoundLiteralNode newCompoundLiteralNode(Source source, TypeNode typeNode, CompoundInitializerNode initializerList)
      Returns a new compound literal node. A compound literal is a C construct used to represent a literal array, structure, or union value. Compound literals are described in the C11 Standard in Secs. 6.5.2.5 and 6.7.9. From Sec. 6.5.2, the syntax is: 
       ( type-name ) { initializer-list }
 ( type-name ) { initializer-list , }
      and from Sec. 6.7.9: 
       initializer:
   assignment-expression
   { initializer-list } { initializer-list , }
 
 initializer-list:
   designationopt initializer
   initializer-list , designationopt initializer
 
 designation:
   designator-list =
 
 designator-list:
   designator
   designator-list designator
 
 designator:
   [ constant-expression ]
   . identifier
      Parameters:
      source - source information for the entire compound literal construct
      typeNode - node representing the type name portion of the compound literal
      initializerList - node representing the initializer list portion of the compound literal
      Returns:
      the new compound literal node

    • newBooleanConstantNode

      ConstantNode newBooleanConstantNode(Source source, boolean value)
      Constructs a new node representing a CIVL-C boolean constant, " $true" or "$false".
      Parameters:
      source - source information for the occurrence of the boolean constant
      value - true for $true, false for $false
      Returns:
      the new boolean constant node

    • newSelfNode

      ExpressionNode newSelfNode(Source source)
      Constructs a new node representing an occurrence of the CIVL-C "self" process constant, written "$self".
      Parameters:
      source - source information for the occurrence of the constant $self
      Returns:
      the new expression node representing the constant

    • newProcnullNode

      ExpressionNode newProcnullNode(Source source)
      Constructs a new node representing an occurrence of the CIVL-C "null process" constant, written $proc_null.
      Parameters:
      source - source information for the occurrence of the constant $proc_null
      Returns:
      the new expression node representing the constant

    • newResultNode

      ExpressionNode newResultNode(Source source)
      Constructs a new node representing an occurrence of the CIVL-C expression "$result", used in function constracts to represent the result returned by the function.
      Parameters:
      source - source information for the occurrence of the expression $result
      Returns:
      the new expression node

    • newIdentifierExpressionNode

      IdentifierExpressionNode newIdentifierExpressionNode(Source source, IdentifierNode identifier)
      Constructs a new identifier expression node. This is an expression node which just wraps an identifier. Identifiers can be used as expressions in various ways in C: a variable or the name of a function, for example. The source is not necessarily the same as the identifier because you might want to include surrounding parentheses in the expression.
      Parameters:
      identifier - the identifier node being wrapped
      Returns:
      the new identifier expression node

    • newAlignOfNode

      AlignOfNode newAlignOfNode(Source source, TypeNode type)
      Constructs a new "align-of" node. This represents an occurrence of the C11 construct _Alignof(typename). See C11 Sec. 6.5.3.4. The value is considered an integer constant, i.e., it is known at compile-time.
      Parameters:
      source - source information for the occurrence of the expression
      type - the type name portion of the expression
      Returns:
      the new align-of node

    • newCastNode

      CastNode newCastNode(Source source, TypeNode type, ExpressionNode argument)
      Constructs a new cast node. This represents an occurrence of a cast expression (typename)argument.
      Parameters:
      source - source information for the occurrence of the complete cast expression
      type - node representing the type name
      argument - the argument part of the expression
      Returns:
      the new cast node

    • newFunctionCallNode

      FunctionCallNode newFunctionCallNode(Source source, ExpressionNode function, List<ExpressionNode> arguments, SequenceNode<ExpressionNode> scopeList)
      Constructs a new function call node. A function call in C is an expression (with side effects) that has the form f(arg0, arg1, ...).
      Parameters:
      source - source information for the occurrence of the entire function call expression
      function - the expression of function type which evaluates to the function being called. Typically this is just an identifier expression (naming the function), but it can be a function pointer or any expression evaluating to a function type or pointer to function type
      arguments - the list of actual arguments to be evaluated and passed to the function in this function call
      scopeList - the optional scope list (to be deprecated)
      Returns:
      the new function call node

    • newFunctionCallNode

      FunctionCallNode newFunctionCallNode(Source source, ExpressionNode function, List<ExpressionNode> contextArguments, List<ExpressionNode> arguments, SequenceNode<ExpressionNode> scopeList)
      Constructs a new kernel function call node. A kernel function call in Cuda-C is an expression (with side effects) that has the form kernelFinvalid input: '<'invalid input: '<'invalid input: '<'cArg0, cArg1[, cArg2]>>>(arg0, arg1, ...). It represents the enqueueing of a kernel to execute on the Cuda device.
      Parameters:
      source - source information for the occurrence of the entire function call expression
      function - the expression of function type which evaluates to the function being called. Typically this is just an identifier expression (naming the function), but it can be a function pointer or any expression evaluating to a function type or pointer to function type
      contextArguments - the list of arguments passed as the execution context (appearing between invalid input: '<'invalid input: '<'invalid input: '<' and >>>) [It is only for CUDA programs]
      arguments - the list of actual arguments to be evaluated and passed to the function in this function call
      scopeList - the optional scope list (to be deprecated)
      Returns:
      the new function call node

    • newGenericSelectionNode

      GenericSelectionNode newGenericSelectionNode(Source source, ExpressionNode controllingExpression, ExpressionNode defaultExpression, SequenceNode<GenericAssociationNode> genericAssociationList)
      Constructs a new generic selection node, used to select an expression to evaluate at compile time based on the type of the controlling expression.
      Parameters:
      source - source information for the occurrence of the entire generic selection expression
      controllingExpression - the (unevaluated) expression whose type determines which expression in the association list this generic selection expression evaluates to
      defaultExpression - the expression that this generic selection evaluates to if the type of the controlling expression is not compatible with any of the types in the association list. This may be null.
      genericAssociationList - the list of (non-default) associations between a typenode and an expression node
      Returns:
      the new generic selection node

    • newGenericAssociationNode

      GenericAssociationNode newGenericAssociationNode(Source source, TypeNode typeLabel, ExpressionNode associatedExpression)
      Constructs a new generic association node which acts as a binding between a type node and an expression for the purposes of a generic selection node
      Parameters:
      source - source information for the occurrence of this generic association node
      typeLabel - the type node which acts as a "key" for which a generic selection to determine whether to pick this association or not
      associatedExpression - the expression associated with the type label that, if selected, will be evaluated
      Returns:
      the new generic association node

    • newDotNode

      DotNode newDotNode(Source source, ExpressionNode structure, IdentifierNode fieldName)
      Constructs a new node for a "dot" expression, used in C for structure or union field navigation, as in myStruct.field.
      Parameters:
      source - source information for the occurrence of the entire dot expression
      structure - the expression of either structure or union type
      fieldName - an identifier which is the name of a field in the structure or union
      Returns:
      the new dot expression node

    • newArrowNode

      ArrowNode newArrowNode(Source source, ExpressionNode structurePointer, IdentifierNode fieldName)
      Constructs a new node for an "arrow" expression, used in C for structure or union field navigation starting from a pointer, as in myStructPtr->field.
      Parameters:
      source - source information for the occurrence of the entire arrow expression
      structurePointer - the expression which has type of the form pointer-to-structure or pointer-to-union
      fieldName - an identifier which is the name of a field in the structure or union
      Returns:
      the new arrow expression node

    • newOperatorNode

      OperatorNode newOperatorNode(Source source, OperatorNode.Operator operator, List<ExpressionNode> arguments)

      Constructs a new operator expression node using one of the standard operators provided in the enumerated type OperatorNode.Operator.

      Some operators are not included in the enumerated type, and instead have their own special class, because they either need to implement an interface that not all operator expressions should implement (e.g., because they are left-hand-side expressions) or because they need to implement some methods that do not apply to all operator expressions. Hence the operator enumerated type includes only those operators that can be treated in a single, generic way.

      Parameters:
      source - source information for the occurrence of the entire operator expression, including the operator itself and its arguments
      operator - the operator
      arguments - the ordered list of arguments to the operator. For binary operators, the left operand comes first, followed by the right operator
      Returns:
      the new operator expression node

    • newOperatorNode

      OperatorNode newOperatorNode(Source source, OperatorNode.Operator operator, ExpressionNode argument)
      Convenience method for constructing new unary operator node; equivalent to invoking newOperatorNode(Source, Operator, ExpressionNode) on the singleton list containing argument.
      Parameters:
      source - source information for the occurrence of the entire operator expression, including the operator itself and its arguments
      operator - the unary operator
      argument - the sole argument to the operator
      Returns:
      the new operator expression node

    • newOperatorNode

      OperatorNode newOperatorNode(Source source, OperatorNode.Operator operator, ExpressionNode arg0, ExpressionNode arg1)
      Convenience method for constructing new binary operator node; equivalent to invoking newOperatorNode(Source, Operator, ExpressionNode) on the list consisting of arg0 and arg1.
      Parameters:
      source - source information for the occurrence of the entire operator expression, including the operator itself and its arguments
      operator - the binary operator
      arg0 - the first argument to the binary operator
      arg1 - the second argument to the binary operator
      Returns:
      the new operator expression node

    • newOperatorNode

      OperatorNode newOperatorNode(Source source, OperatorNode.Operator operator, ExpressionNode arg0, ExpressionNode arg1, ExpressionNode arg2)
      Convenience method for constructing new ternary operator node; equivalent to invoking newOperatorNode(Source, Operator, ExpressionNode) on the list consisting of arg0, arg1, and arg2.
      Parameters:
      source - source information for the occurrence of the entire operator expression, including the operator itself and its arguments
      operator - the ternary operator
      arg0 - the first argument to the ternary operator
      arg1 - the second argument to the ternary operator
      arg2 - the third argument to the ternary operator
      Returns:
      the new operator expression node

    • newSizeofNode

      SizeofNode newSizeofNode(Source source, SizeableNode argument)
      Constrcts a new sizeof expression. This takes one argument, which can be either a type name or an expression.
      Parameters:
      source - source information for the occurrence of the entire sizeof expression, including the argument
      argument - the argument to the sizeof operator
      Returns:
      the new expression node

    • newSpawnNode

      SpawnNode newSpawnNode(Source source, FunctionCallNode callNode)
      Constructs a new CIVL-C spawn expression. A spawn expression has the form $spawn followed by a function call expression. Hence a spawn node has one argument, which is a function call node.
      Parameters:
      source - source information for the occurrence of the entire $spawn expression, including the entire function call
      callNode - the function call node
      Returns:
      the new spawn expression node

    • newRemoteOnExpressionNode

      RemoteOnExpressionNode newRemoteOnExpressionNode(Source source, ExpressionNode left, ExpressionNode right)
      Constructs a remote expression node, representing an expression of the form proc_expr@x. This refers to a variable in the process p referenced by the expression proc_expr. The static variable x can be determined statically now. Later it will be evaluated in a dynamic state in p's context.
      Parameters:
      source - source information for the entire remove expression, including both arguments
      left - the left argument, which is an expression of integer type.
      right - the right argument, which is a foreign expression that will evaluates on the process represented by the left expression.

    • newScopeOfNode

      ScopeOfNode newScopeOfNode(Source source, IdentifierExpressionNode variableExpression)
      Constructs a new CIVL-C $scopeof expression node. This is an expression which takes one argument, which is a variable expression. It returns a reference to the dynamic scope (a value of type $scope) containing the memory unit identified by that variable.
      Parameters:
      source - source information for the entire $scopeof expression
      variableExpression - the variable argument
      Returns:
      the new $scopeof expression

    • newQuantifiedExpressionNode

      QuantifiedExpressionNode newQuantifiedExpressionNode(Source source, QuantifiedExpressionNode.Quantifier quantifier, SequenceNode<PairNode<SequenceNode<VariableDeclarationNode>,ExpressionNode>> boundVariableDeclarationList, ExpressionNode restriction, ExpressionNode expression, SequenceNode<PairNode<ExpressionNode,ExpressionNode>> intervalSequence)
      Constructs a new quantified expression.
      Parameters:
      source - The source code information for the entire expression
      quantifier - The quantifier, one of (1) QuantifiedExpressionNode.Quantifier.EXISTS, the standard existential quantifier, (2) QuantifiedExpressionNode.Quantifier.FORALL , the standard universal quantifier, or (3) QuantifiedExpressionNode.Quantifier.UNIFORM, the CIVL-C quantifier representing a uniform universal condition
      boundVariableDeclarationList - The list of bound variable declarations.
      restriction - A boolean-valued expression that holds true when the quantified variables is in the domain
      expression - The quantified expression.
      intervalSequence - field for the $uniform operator---a sequence of real closed intervals that specify the domain of uniform convergence of a big-O expression; may be null
      Returns:
      The new quantified expression with the given children.

    • newArrayLambdaNode

      ArrayLambdaNode newArrayLambdaNode(Source source, TypeNode type, SequenceNode<PairNode<SequenceNode<VariableDeclarationNode>,ExpressionNode>> boundVariableDeclarationList, ExpressionNode restriction, ExpressionNode expression)
      Constructs a new array lambda expression.
      Parameters:
      source - The source code information for the entire expression
      type - the type of this array lambda
      boundVariableDeclarationList - The list of bound variable declarations.
      restriction - A boolean-valued expression that holds true when the quantified variables is in the domain
      expression - The body-expression
      Returns:
      The new array lambda expression with the given children.

    • newArrayLambdaNode

      ArrayLambdaNode newArrayLambdaNode(Source source, TypeNode type, List<VariableDeclarationNode> boundVariableDeclarationList, ExpressionNode restriction, ExpressionNode expression)
      Constructs a new array lambda expression.
      Parameters:
      source - The source code information for the entire expression
      type - the type of this array lambda
      boundVariableDeclarationList - The list of bound variable declarations.
      restriction - A boolean-valued expression that holds true when the quantified variables is in the domain
      expression - The body-expression
      Returns:
      The new array lambda expression with the given children.

    • newLambdaNode

      LambdaNode newLambdaNode(Source source, VariableDeclarationNode boundVariableDeclaration, ExpressionNode expression)
      Constructs a new lambda expression with a free (no restriction on the bound variable) variable.
      Parameters:
      source - The source code information for the entire expression
      boundVariableDeclaration - The bound variable declaration.
      expression - The body-expression
      Returns:
      The new array lambda expression with the given children.

    • newLambdaNode

      LambdaNode newLambdaNode(Source source, VariableDeclarationNode boundVariableDeclaration, ExpressionNode restriction, ExpressionNode expression)
      Constructs a new lambda expression with restriction on the bound variable.
      Parameters:
      source - The source code information for the entire expression
      boundVariableDeclaration - The bound variable declaration.
      restriction - A boolean restriction on the bound variable
      expression - The body-expression
      Returns:
      The new array lambda expression with the given children.

    • newDerivativeExpressionNode

      DerivativeExpressionNode newDerivativeExpressionNode(Source source, ExpressionNode function, SequenceNode<PairNode<IdentifierExpressionNode,IntegerConstantNode>> partials, SequenceNode<ExpressionNode> arguments)
      Constructs a new CIVL-C derivative expression, used to represent the (partial) derivative of a function with respect to any number of variables, evaluated at a point.
      Parameters:
      source - The source code elements.
      function - The abstract function whose derivative is being taken.
      partials - The list of partial derivatives.
      arguments - The arguments to the uninterpreted function evaluation.
      Returns:
      The new derivative expression with the given children.

    • newRegularRangeNode

      RegularRangeNode newRegularRangeNode(Source source, ExpressionNode low, ExpressionNode high)

      Constructs a new CIVL-C regular range expression, which has the form lo .. hi, where lo and hi are integer expressions. A range expression represents an (ordered) set of integers. This expression represents the set of integers that are greater than or equal to lo and less than or equal to hi. The order is from lowest to highest.

      See newRegularRangeNode(Source, ExpressionNode, ExpressionNode, ExpressionNode) for the more general expression which permits a "step" to be specified. The expression returned by this method is equivalent to using a step of 1.

      Parameters:
      source - source information for the entire expression
      low - the lower bound of the range (inclusive)
      high - the upper bound of the range (inclusive)
      Returns:
      the new range expression

    • newRegularRangeNode

      RegularRangeNode newRegularRangeNode(Source source, ExpressionNode low, ExpressionNode high, ExpressionNode step)

      Constructs a new CIVL-C regular range expression, which has the form lo .. hi # step, where lo, hi, and step are all integer expressions.

      A range expression represents an (ordered) set of integers. If step is positive, this expression represents the set of integers lo, lo+step, lo+2*step, and so on, up to and possibly including hi. That is also the order.

      If step is negative, this represents the ordered set of integers hi, hi+step, hi+2*step, and so on, down to and possibly including lo. That is also the order.

      Parameters:
      source - source information for the entire expression
      low - the lower bound of the range (inclusive)
      high - the upper bound of the range (inclusive)
      step - the step, i.e., the (positive or negative) distance between two consecutive elements in the range
      Returns:
      the new range expression

    • newVariableDeclarationNode

      VariableDeclarationNode newVariableDeclarationNode(Source source, IdentifierNode name, TypeNode type)
      Creates a new declaration of an "object" variable with no initializer.
      Parameters:
      source - the source information for the variable declaration
      name - the identifier node corresponding to the name of the variable in its declaration
      type - the node corresponding to the type in the declaration
      Returns:
      the new variable declaration node with the given chidren

    • newVariableDeclarationNode

      VariableDeclarationNode newVariableDeclarationNode(Source source, IdentifierNode name, TypeNode type, InitializerNode initializer)
      Creates a new declaration for an "object" variable with an initializer.
      Parameters:
      name - identifier being declared
      type - the type
      initializer - optional initializer (for variables only) or null
      Returns:
      a new declaration for an "ordinary identifier"

    • newFunctionDeclarationNode

      FunctionDeclarationNode newFunctionDeclarationNode(Source source, IdentifierNode name, TypeNode type, SequenceNode<ContractNode> contract)
      Creates a new function declaration with no body (so it is not a function "definition").
      Parameters:
      source - source information for this declaration
      name - the identifier node for the name of this function
      type - node representing the type of the function
      contract - sequence of contract elements or null
      Returns:
      the new function declaration node formed from given children

    • newEnumeratorDeclarationNode

      EnumeratorDeclarationNode newEnumeratorDeclarationNode(Source source, IdentifierNode name, ExpressionNode value)
      Creates new declaration of an enumerator, which is an element inside of a C enum definition. An enumerator declaration always contains an identifier, and may or may not contain an optional integer value.
      Parameters:
      source - source information for the entire enumerator declaration, including the value node if present
      name - the identifier which is the name of the enumerator
      value - the (optional) value to be assigned to this enumerator; if absent, use null
      Returns:
      the new enumerator declaration

    • newFieldDeclarationNode

      FieldDeclarationNode newFieldDeclarationNode(Source source, IdentifierNode name, TypeNode type)
      Consructs a new field declaration node. A field declaration occurs inside a struct or union definition in C. This declaration is similar to an ordinary variable declaration.
      Parameters:
      source - source information for the entire field declaration
      name - the identifier which is the name of the field being declared
      type - the type of the field
      Returns:
      the new field declaration node

    • newFieldDeclarationNode

      FieldDeclarationNode newFieldDeclarationNode(Source source, IdentifierNode name, TypeNode type, ExpressionNode bitFieldWidth)
      Consructs a new field declaration node which also includes a "bit width" argument. A field declaration occurs inside a struct or union definition in C. This declaration is similar to an ordinary variable declaration, but may include a bit width parameter.
      Parameters:
      source - source information for the entire field declaration
      name - the identifier which is the name of the field being declared
      type - the type of the field
      bitFieldWidth - the constant expression of integer type which specifies the number of bits in the field
      Returns:
      the new field declaration node

    • newStandardLabelDeclarationNode

      OrdinaryLabelNode newStandardLabelDeclarationNode(Source source, IdentifierNode name, StatementNode statement)

      Creates a new node representing a standard C label. An ordinary label is an identifier preceding a colon then a statement. It can be used as the target of a goto statement.

      A label declaration node has one child: an identifier node which is the name of the label. Note in particular that the statement (following the colon) is not a child of the label declaration node. The declaration node does contain a reference to that statement, but it is not a child, since both the label declaration and the statement will be children of a LabeledStatementNode. If the statement were a child of the label declaration node, the AST would not be a tree.

      The standard protocol for constructing a labled statement is as follows: first, construct the ordinary statement S. Then construct the label declaration node L using this method, using S as the statement argument. Finally, create a new LabeledStatementNode using method newLabeledStatementNode(Source, LabelNode, StatementNode) with arguments L and S.

      Parameters:
      source - source information for the label only (not the statement that follows)
      name - the name of the label
      statement - the statement that follows the label and colon
      Returns:
      the new label declaration node

    • newCaseLabelDeclarationNode

      SwitchLabelNode newCaseLabelDeclarationNode(Source source, ExpressionNode constantExpression, StatementNode statement)
      Constructs a new case-labeled declaration node. This node represents a C construct of the form case expr : which precedes a statement inside a switch statement body.
      Parameters:
      source - source information spanning the case and expr tokens
      constantExpression - the expression expr following case; must be a constant expression whose type is consistent with that of the argument to switch
      statement - the statement following the colon; that statement is not made a child of this node
      Returns:
      the new case-labeled declaration node

    • newDefaultLabelDeclarationNode

      SwitchLabelNode newDefaultLabelDeclarationNode(Source source, StatementNode statement)
      Constructs a new node representing the occurence of a default : label inside of a switch statement body.
      Parameters:
      source - the source information spanning the default token
      statement - the statement following the colon; this is not made a child of the new switch label node
      Returns:
      the new switch label node

    • newTypedefDeclarationNode

      TypedefDeclarationNode newTypedefDeclarationNode(Source source, IdentifierNode name, TypeNode type)
      Constructs a new typedef declaration node. If the typedef was scope parameterized, the type argument will be a ScopeParameterizedTypeNode.
      Parameters:
      source - source code reference
      name - the name of the typedef as an IdentifierNode
      type - the type node being bound to the identifier (this may be scope parameterized)
      Returns:
      a new typedef declaration node

    • newCompoundInitializerNode

      CompoundInitializerNode newCompoundInitializerNode(Source source, List<PairNode<DesignationNode,InitializerNode>> initList)

      Constructs new compound initializer node. A compound initializer in C is used to initialize an array or structure. It occurs inside curly braces. It consists of a list of designation-initializer pairs; each designation represents a "point" inside the structure or array; the initializer specifies a value to assign to that point. The definition is recursive, since the initializer in a pair may be a compound initializer.

      A designation in pair may be null. In this case the "point" is obtained by rules specified in the C Standard, essentially by increment one past the last point.

      Parameters:
      source - source information spanning the entire compound initializer, from the opening curly brace to the closing curly brace
      initList - the list of designation-initializer pairs.
      Returns:
      the new compound initializer nodes

    • newDesignationNode

      DesignationNode newDesignationNode(Source source, List<DesignatorNode> designators)
      Creates a new designation node, which can be used as part of a compound initializer. A designation consists of a sequence of designators. The designator sequence describes how to navigate to a particular point inside a complex structure or array.
      Parameters:
      source - source information spanning the entire designation
      designators - the sequence of designators
      Returns:
      the new designation node

    • newFieldDesignatorNode

      FieldDesignatorNode newFieldDesignatorNode(Source source, IdentifierNode name)
      Constructs a new field designator node. A field designator is a designator (used as part of a designation, which is part of a compound initializer) which represents navigation to a particular field in a structure or union. It essentially wraps a field name.
      Parameters:
      source - source information spanning this field designator
      name - the identifier which is the name of the field
      Returns:
      the new field designator node

    • newArrayDesignatorNode

      ArrayDesignatorNode newArrayDesignatorNode(Source source, ExpressionNode index)
      Constructs a new array designator node. An array designator is a designator (used as part of a designation, which is part of a compound initializer) which represents navigation to a particular element of an array. It essentially wraps an integer expression, which specifies an index.
      Parameters:
      source - source information spanning the array designator
      index - the integer expression specifying an index into the array
      Returns:
      the new array designator node

    • newCompoundStatementNode

      CompoundStatementNode newCompoundStatementNode(Source source, List<BlockItemNode> items)
      Constructs a new compound statement node. This is designated in C as { s1; s2; ...}, where each si is a block item (e.g., a statement, a declaration, or any other instance of
      invalid reference 
      BlockItermNode
      .
      Parameters:
      source - source information encompassing the entire compound statement, from the opening curly brace to the closing curly brace
      items - the list of block items comprising the compound statement
      Returns:
      the new compound statement node

    • newExpressionStatementNode

      ExpressionStatementNode newExpressionStatementNode(ExpressionNode expression)
      Constructs a new expression statement node. This is a statement which wraps an expression. The source is the same as that of the expression.
      Parameters:
      expression - the expression node
      Returns:
      the new expression statement node wrapping that expression

    • newNullStatementNode

      StatementNode newNullStatementNode(Source source)
      Constructs a new node representing a C "null" statement, also known as a "no-op" statement, and written as just a semicolon.
      Parameters:
      source - source specification encompassing the single semicolon character
      Returns:
      the new null statement node

    • newForLoopNode

      ForLoopNode newForLoopNode(Source source, ForLoopInitializerNode initializer, ExpressionNode condition, ExpressionNode incrementer, StatementNode body, SequenceNode<ContractNode> contracts)
      Constructs a new for loop node.
      Parameters:
      source - source information for the entire loop construct (including body)
      initializer - the initializer part of the for loop, an
      invalid reference 
      Expression
      or another instance of ForLoopInitializerNode, such as one produced from a list of delcarations; may be null
      condition - the condition part of the for loop
      incrementer - the incrementer part of the for loop
      body - the body of the for loop
      invariant - loop invariant: may be null
      Returns:
      the new for loop node

    • newForLoopInitializerNode

      DeclarationListNode newForLoopInitializerNode(Source source, List<VariableDeclarationNode> declarations)
      Construcs a new declaration list node, which is comprised of a sequence of variable declarations. Such a node can be used as the initializer part of a for loop, or as the variable list part of a CIVL-C $for or $parfor statement.
      Parameters:
      source - source specification encompassing the entire list of declarations
      declarations - list of variable declarations
      Returns:
      the new declaration list node

    • newWhileLoopNode

      LoopNode newWhileLoopNode(Source source, ExpressionNode condition, StatementNode body, SequenceNode<ContractNode> contracts)
      Constructs a new node representing a while loop. This is represented while (cond) body in C, but may also have an optional CIVL-C loop invariant.
      Parameters:
      source - source specification spanning the entire loop and all its components, including the invariant (if present) and the body
      condition - the boolean expression which determines whether control stays in the loop
      body - the loop body, a statement
      invariant - a boolean expression which is a loop invariant; may be null
      Returns:
      the new while loop node

    • newDoLoopNode

      LoopNode newDoLoopNode(Source source, ExpressionNode condition, StatementNode body, SequenceNode<ContractNode> contracts)
      Constructs a new node representing a do...while loop. This is represented in C as do body while (cond). This kind of loop guarantees that the body will be executed at least once, as the condition is checked after each execution of the body, rather than before. Otherwise it is the same as a while loop.
      Parameters:
      source - source specification spanning the entire loop, including the body, the invariant, and the condition
      condition - the boolean condition which determines whether control should return to the top of the loop body
      body - the loop body
      invariant - an optional boolean expression loop invariant which may be associated to this node; may be null
      Returns:
      the new do loop node
      See Also:
      • invalid reference 
        #newWhileLoopNode(Source, ExpressionNode, StatementNode, ExpressionNode)

    • newGotoNode

      GotoNode newGotoNode(Source source, IdentifierNode label)
      Constructs a new node representing a goto statement.
      Parameters:
      source - source specification spanning the whole goto statement, including the label
      label - identifier which is the name of the label to which control should "go"
      Returns:
      the new goto node

    • newIfNode

      IfNode newIfNode(Source source, ExpressionNode condition, StatementNode trueBranch)
      Creates new if statement node when there is no false ("else") branch.
      Parameters:
      source - source specification spanning the entire statement, including the entire "true" branch
      condition - the condition expression
      trueBranch - the body of the if statement
      Returns:
      the new if statement node formed from given children

    • newIfNode

      IfNode newIfNode(Source source, ExpressionNode condition, StatementNode trueBranch, StatementNode falseBranch)
      Creates a new if statement node. False branch may be null if there is no "else" clause.
      Parameters:
      source - source specification spanning the entire statement, including both branches in their entirety
      condition - the branch condition
      trueBranch - the statement for the "true" branch
      falseBranch - the statement for the "false" branch
      Returns:
      the new if statement node

    • newContinueNode

      JumpNode newContinueNode(Source source)
      Creates a new node representing the C continue statement, used in a loop body to direct control to the next loop iteration.
      Parameters:
      source - source specification for the continue token
      Returns:
      the new new continue node

    • newBreakNode

      JumpNode newBreakNode(Source source)
      Creates a new node representing the C break statement, used in a loop or switch body to direct control to the location just after the loop or switch construct.
      Parameters:
      source - source specification for the break token
      Returns:
      the new new break node

    • newReturnNode

      ReturnNode newReturnNode(Source source, ExpressionNode argument)
      Creates a new return statement node. Argument may be null.
      Parameters:
      argument - the expression being returned or null if there is none
      Returns:
      the new return statement node

    • newLabeledStatementNode

      LabeledStatementNode newLabeledStatementNode(Source source, LabelNode label, StatementNode statement)
      Constructs new node representing a labeled statement. The label and the statement being labeled must be constructed first, then used as arguments to this method.
      Parameters:
      source - source specification spanning the entire labeled statement, including the label and the statement being labeled
      label - the node representing the label
      statement - the statement to be labeled
      Returns:
      the new labeled statement node
      See Also:

    • newSwitchNode

      SwitchNode newSwitchNode(Source source, ExpressionNode condition, StatementNode body)
      Constructs a new node representing a C switch statement. The switch body must be created first, and this body includes all the case-labeled statements (and break statements) required. The condition must have a type appropriate for a swich statement, such as an integer type.
      Parameters:
      source - source specification spanning the entire switch statement, including the entire body
      condition - the expression that is evaluated to determine which case to switch to
      body - the body of the switch statement
      Returns:
      the new switch statement node

    • newCivlForNode

      CivlForNode newCivlForNode(Source source, boolean isParallel, DeclarationListNode variables, ExpressionNode domain, StatementNode body, SequenceNode<ContractNode> loopContract)
      Creates a new instance of the CIVL $for or $parfor node.
      Parameters:
      source - source information for the entire loop construct (including body)
      isParallel - if true create a $parfor statement, else create a $for statement
      variables - the list of loop variables or variable decls
      domain - the expression of domain type defining the iteration domain; the dimension of the domain must equal the number of loop variables
      body - the body of the loop statement
      loopContract - optional loop contracts node
      Returns:
      the new node

    • newWhenNode

      WhenNode newWhenNode(Source source, ExpressionNode guard, StatementNode body)
      Creates a new node representing a CIVL-C $when node, used to represent a guarded command. Such a statement blocks until the guard is true. Note that only the first atomic sub-statement of the statement body is guaranteed to execute atomically with the evaluation to true of the guard.
      Parameters:
      source - source specification spanning the entire $when statement, including the guard and the entire body
      guard - a boolean expression which determines when the statement is enabled
      body - a statement that may be executed once the guard holds
      Returns:
      the new $when statement node

    • newChooseStatementNode

      ChooseStatementNode newChooseStatementNode(Source source, List<StatementNode> statements)
      Constructs a new node representing a CIVL-C $choose statement. This statement has the form 
       $choose {
   $when (g1) s1
   $when (g2) s2
   ...
 }
      The statement is used to specify a nondeterministic choice. Whenever control is at the $choose location, the guards g1, g2, etc., are evaluated. Each that evaluates to true specifies one enabled transition. If none are enabled, the entire statement blocks. The order of these clauses is irrelevant.
      Parameters:
      source - source specification spanning the entire $choose statement, including the entire body
      statements - the guarded commands which form the clauses of the $choose statement
      Returns:
      the new $choose statement node

    • newStaticAssertionNode

      StaticAssertionNode newStaticAssertionNode(Source source, ExpressionNode expression, StringLiteralNode message)
      Creates a new C11 static assertion node. A static assertion is an assertion which is checked at compile time. The syntax is 
       _Static_assert(expr, message)
      Parameters:
      source - source specification spanning the entire static assertion statement
      expression - the integer constant expression which, if it evaluates to 0, yields an assertion violation. Note that the boolean type _Bool is an integer type in C, so a value of this type may be used.
      message - the message to be printed if the assertion is violated
      Returns:
      the new static assertion node

    • newPragmaNode

      PragmaNode newPragmaNode(Source source, IdentifierNode identifier, CivlcTokenSequence producer, CivlcToken newlineToken)
      Constructs a new pragma node, representing a C #pragma directive. The pragma is left uninterpreted in this representation. The first token following the #pragma must be an identifier, this identifier has a special role as it specifies a pragma domain, such as omp (for OpenMP). The remainder of the pragma is represented as a sequence of raw tokens. These can be parsed interpreted at a later stage of processing. Finally, every pragma must be terminated by the first newline character encountered, and the token for that newline is also specified.
      Parameters:
      source - source specification spanning the entire pragma line, from the #pragma up to and including the newline.
      identifier - the first token after the #pragma token specifying the pragma domain (e.g., omp)
      producer - a producer for producing new CivlcTokenSource objects which are essentially iterators over the tokens comprising the body, i.e., the sequence of tokens comprising the rest of the pragma body after the identifier, and not including the newline
      newlineToken - the newlinen token at the end of the pragma
      Returns:
      the new pragma node

    • newRequiresNode

      RequiresNode newRequiresNode(Source source, ExpressionNode expression)
      Constructs a new node representing a CIVL-C $requires contract clause. This is used to specify a pre-condition for a function. It is currently not used.
      Parameters:
      source - source specification spanning the entire $requires clause, including the entire expression
      expression - the boolean expression which specifies a pre-condition
      Returns:
      the new $requires clause node

    • newEnsuresNode

      EnsuresNode newEnsuresNode(Source source, ExpressionNode expression)
      Constructs a new node representing a CIVL-C $ensures contract clause. This is used to specify a post-condition for a function. It is currently not used.
      Parameters:
      source - source specification spanning the entire $ensures clause, including the entire expression
      expression - the boolean expression which specifies a post-condition
      Returns:
      the new $ensures clause node

    • newDependsNode

      DependsNode newDependsNode(Source source, ExpressionNode condition, SequenceNode<DependsEventNode> eventList)
      Constructs a new node representing a CIVL-C $depends contract clause. This is used to specify the dependency relationship between processes for a function.
      Parameters:
      source - source specification spanning the entire $depends clause, including the entire expression
      expression - the boolean expression which specifies a condition of dependency
      Returns:
      the new $depends clause node

    • newGuardNode

      GuardsNode newGuardNode(Source source, ExpressionNode expression)
      Constructs a new node representing a CIVL-C $guard contract clause. This is used to specify the guard of a function.
      Parameters:
      source - source specification spanning the entire $guard clause, including the entire expression
      expression - the boolean expression which specifies the the guard
      Returns:
      the new $guard clause node

    • newAssignsNode

      AssignsOrReadsNode newAssignsNode(Source source, SequenceNode<ExpressionNode> expressionList)
      Constructs a new node representing an ACSL assigns contract clause.
      Parameters:
      source - source specification spanning the entire $assigns clause, including the entire expression
      expressionList - the expression list which specifies the memory units associated with the assigns clause
      Returns:
      the new assigns clause node

    • newReadsNode

      AssignsOrReadsNode newReadsNode(Source source, SequenceNode<ExpressionNode> expressionList)
      Constructs a new node representing an ACSL reads contract clause.
      Parameters:
      source - source specification spanning the entire reads clause, including the entire expression
      expressionList - the expression list which specifies the memory units associated with the reads clause
      Returns:
      the new reads clause node

    • newFunctionDefinitionNode

      FunctionDefinitionNode newFunctionDefinitionNode(Source source, IdentifierNode name, FunctionTypeNode type, SequenceNode<ContractNode> contract, CompoundStatementNode body)
      Constructs a new node representing a function definition, i.e., a function declaration with body.
      Parameters:
      source - source specification spanning the entire function definition, including the entire function body
      name - the identifier which is the name of the function being defined
      type - the type of the function; note that a function type comprises a return type and some sequence of input types
      contract - the (optional) function contract; may be null
      body - the function body
      Returns:
      the new function definition node

    • newAbstractFunctionDefinitionNode

      AbstractFunctionDefinitionNode newAbstractFunctionDefinitionNode(Source source, IdentifierNode name, TypeNode type, SequenceNode<ContractNode> contract, int continuity, SequenceNode<PairNode<ExpressionNode,ExpressionNode>> intervals, StringLiteralNode attr)
      Creates a new CIVL abstract function definition. An abstract function is an unspecified mathematical function. In particular, if x1=y1 and ... and xn=yn then f(x1,...,xn)=f(y1,...,yn). In other words, the value "returned" by f is a deterministic function of its inputs. In cannot depend on any other variables values in the program, or other parts of the state. As a special case, note that if n=0, then f() is essentially a constant. In fact, the case n=0 is not allowed: if you want a constant, create instead an input variable ($input).
      Parameters:
      source - The source information for the abstract function definition.
      name - The name of the abstract function.
      type - The function type with the appropriate parameters and return type.
      contract - Any code contract associated with the function.
      continuity - The number of derivatives that may be taken; this applies to real valued functions of real variables only
      intervals - sequence of intervals whose Cartesian product specifies the domain on which this function is differentiable to the specified degree
      attr - nullable. The optional string literal representing the attribute attached to this abstract function.
      Returns:
      An abstract function definition with the specified properties.

    • newTranslationUnitNode

      SequenceNode<BlockItemNode> newTranslationUnitNode(Source source, List<BlockItemNode> definitions)
      Creates a new node representing an entire translation unit. The children of this node will be external definitions.
      Parameters:
      source - source specification spanning the entire translation unit, which is typically the entire token sequence emanating from the preprocessor
      definitions - the list of external definitions which form the children of the translation unit
      Returns:
      the new translation unit node

    • newProgramNode

      SequenceNode<BlockItemNode> newProgramNode(Source source, List<BlockItemNode> definitions)
      Creates a new node representing an entire program. The children of this node will be external definitions.
      Parameters:
      source - source specification for the whole program; typically a "fake" source
      definitions - the list of external definitions which form the children of the new node; typically obtained by concatenating those from the translation units, perhaps after some modifications
      Returns:
      the new program node

    • getValueFactory

      ValueFactory getValueFactory()
      Returns the value factory associated to this node factory. The value factory is used to reason about constants and constant expressions in a program.
      Returns:
      the value factory

    • newAtomicStatementNode

      AtomicNode newAtomicStatementNode(Source statementSource, StatementNode body)
      Creates a new CIVL-C $atomic statement node.
      Parameters:
      statementSource - source specification spanning the entire statement, including the body
      body - The body statement node of the atomic node
      Returns:
      The new atomic statement node

    • newHereNode

      ExpressionNode newHereNode(Source source)
      Creates a new constant expression node representing $here.
      Parameters:
      source - The source code element of the new node
      Returns:
      a new constant expression node representing $here

    • newRootNode

      ExpressionNode newRootNode(Source source)
      Creates a new constant expression node representing $root.
      Parameters:
      source - The source code element of the new node
      Returns:
      a new constant expression node representing $root

    • newScopeOfNode

      ScopeOfNode newScopeOfNode(Source source, ExpressionNode argument)
      Creates a new expression node representing $scopeof(expr).
      Parameters:
      source - The source code element of the new node.
      argument - The argument of the $scopeof(expr) expression.
      Returns:
      a new constant expression node representing $here

    • newOmpParallelNode

      OmpParallelNode newOmpParallelNode(Source source, StatementNode statement)
      Creates a new OpenMP parallel node, representing #pragma omp parallel.... The clauses of the node can be updated by calling the corresponding setters, e.g, setStatementNode(), setPrivateList(), etc.
      Parameters:
      source - The source code element of the new node.
      statement - The statement node of the parallel construct.
      Returns:
      The new OpenMP parallel statement node created.

    • newOmpForNode

      OmpForNode newOmpForNode(Source source, StatementNode statement)
      Creates a new OpenMP for node, representing #pragma omp for.... The clauses of the node can be updated by calling the corresponding setters, e.g, setStatementNode(), setPrivateList(), etc.
      Parameters:
      source - The source code element of the new node.
      statement - The statement node of the parallel construct.
      Returns:
      The new OpenMP for node created.

    • newOmpMasterNode

      OmpSyncNode newOmpMasterNode(Source source, StatementNode statement)
      Creates a new OpenMP master node, representing #pragma omp master.... A master node has exactly one child node, i.e., the statement node corresponding to the block affected by the master construct. The syntax of the master construct is:
      #pragma omp master new-line
      structured-block
      Parameters:
      source - The source code element of the new node.
      statement - The statement node of the master construct.
      Returns:
      The new OpenMP master node created.

    • newOmpAtomicNode

      OmpSyncNode newOmpAtomicNode(Source source, StatementNode statement, OmpAtomicNode.OmpAtomicClause clause, boolean seqConsistent)
      Creates a new OpenMP atomic node, representing #pragma omp atomic.... An atomic node has exactly one child node, i.e., the statement node corresponding to the block affected by the atomic construct. The syntax of the atomic construct is:
      #pragma omp atomic new-line
      structured-block
      Parameters:
      source - The source code element of the new node.
      statement - The statement node of the master construct.
      clause - the atomic clause associated with this atomic construct, either "read", "write", "update" or "capture". Absent of clause means "update"
      seqConsistent - true if this atomic construct is sequentially consistent
      Returns:
      The new OpenMP atomic node created.

    • newOmpCriticalNode

      OmpSyncNode newOmpCriticalNode(Source source, IdentifierNode name, StatementNode statement)
      Creates a new OpenMP critical node, representing #pragma omp critical.... A critical node has at most two children the name of the critical section and the statement node corresponding to the block affected by the critical construct. The syntax of the critical construct is:
      #pragma omp critical [(name)] new-line
      structured-block
      Parameters:
      source - The source code element of the new node.
      name - The name of the critical section.
      statement - The statement node of the critical construct.
      Returns:
      The new OpenMP critical node created.

    • newOmpBarrierNode

      OmpSyncNode newOmpBarrierNode(Source source)
      Creates a new OpenMP barrier node, representing #pragma omp barrier.... A barrier node has NO child node. The syntax of the barrier construct is:
      #pragma omp barrier new-line
      Parameters:
      source - The source code element of the new node.
      Returns:
      The new OpenMP barrier node created.

    • newOmpFlushNode

      OmpSyncNode newOmpFlushNode(Source source, SequenceNode<IdentifierExpressionNode> variables)
      Creates a new OpenMP flush node, representing #pragma omp flush.... A flush node has at most one child node: the list of variables of the flush operation. The syntax of the flush construct is:
      #pragma omp flush [(list)] new-line
      Parameters:
      source - The source code element of the new node.
      variables - The list of variables of the flush operation.
      Returns:
      The new OpenMP flush node created.

    • newOmpFlushNode

      OmpSyncNode newOmpFlushNode(Source source)
      Creates a new OpenMP flush node with no variable list
      Parameters:
      source - The source code element of the new node.
      Returns:
      The new OpenMP flush node created.

    • newOmpOrederedNode

      OmpSyncNode newOmpOrederedNode(Source source, StatementNode statement)
      Creates a new OpenMP ordered node, representing #pragma omp ordered.... An ordered node has exactly one child node, i.e., the statement node corresponding to the block affected by the ordered construct. The syntax of the ordered construct is:
      #pragma omp ordered new-line
      structured-block
      Parameters:
      source - The source code element of the new node.
      statement - The statement node of the ordered construct.
      Returns:
      The new OpenMP ordered node created.

    • newOmpSectionsNode

      OmpWorksharingNode newOmpSectionsNode(Source source, StatementNode statement)
      Creates a new OpenMP sections node, representing #pragma omp sections.... The clauses of the node can be updated by calling the corresponding setters, e.g, setStatementNode(), setPrivateList(), etc.
      Parameters:
      source - The source code element of the new node.
      statement - The statement node of the ordered construct.
      Returns:
      The new OpenMP sections statement node created.

    • newOmpSectionNode

      OmpWorksharingNode newOmpSectionNode(Source source, StatementNode statement)
      Creates a new OpenMP section node, representing #pragma omp section.... A section node has exactly one child node, i.e., the statement node corresponding to the block affected by the section construct. The syntax of the section construct is:
      #pragma omp section new-line
      structured-block
      Parameters:
      source - The source code element of the new node.
      statement - The statement node of the section construct.
      Returns:
      The new OpenMP section node created.

    • newOmpSingleNode

      OmpWorksharingNode newOmpSingleNode(Source source, StatementNode statement)
      Creates a new OpenMP single node, representing #pragma omp single.... The syntax of the single construct is as follows:
      #pragma omp single [clause[[,] clause] ...] new-line
      structured-block
      where clause is one of the following:
      private(list)
      firstprivate(list)
      copyprivate(list)
      nowait
      Parameters:
      source - The source code element of the new node.
      statement - The statement node of the section construct.
      Returns:
      The new OpenMP single node created.

    • newOmpSimdNode

      OmpSimdNode newOmpSimdNode(Source source, StatementNode statement)
      Creates a new OpenMP simd node, representing #pragma omp simd.... The syntax of the simd directive is as follows:
      #pragma omp simd [clause[[,] clause] ...] new-line
      structured-block
      where clause is one of the following:
      safelen
      simdlen
      private(list)
      firstprivate(list)
      copyprivate(list)
      nowait
      Parameters:
      source - The source code element of the new node.
      statement - The statement node of the simd construct.
      Returns:
      The new OpenMP simd node created.

    • newOmpThreadprivateNode

      OmpDeclarativeNode newOmpThreadprivateNode(Source source, SequenceNode<IdentifierExpressionNode> variables)
      Creates a new OpenMP threadprivate node.
      Parameters:
      source - The source code element of the new node.
      variables - The list of variables declared by the clause.
      Returns:
      The new OpenMP threadprivate node created.

    • newOmpFortranEndNode

      OmpEndNode newOmpFortranEndNode(Source source, OmpEndNode.OmpEndType endType)
      FORTRAN ONLY
      Creates a new OpenMP END node with its type, which indicates what previous OpenMP executable struct should end.
      Parameters:
      source - The source code element of the new node.
      endType - The end type of the new END node.
      Returns:
      The new OpenMP END node created.

    • newOmpSymbolReductionNode

      OmpSymbolReductionNode newOmpSymbolReductionNode(Source source, OmpReductionNode.OmpReductionOperator operator, SequenceNode<IdentifierExpressionNode> variables)
      Creates a new OpenMP reduction node with a standard operator.
      Parameters:
      source - The source code element of the new node.
      operator - The OmpReductionNode.OmpReductionOperator of the reduction node.
      variables - The variables of the reduction clause.
      Returns:
      The new OpenMP reduction node.

    • newOmpFunctionReductionNode

      OmpFunctionReductionNode newOmpFunctionReductionNode(Source source, IdentifierExpressionNode function, SequenceNode<IdentifierExpressionNode> variables)
      Creates a new OpenMP reduction node with an identifier operator (i.e., function names).
      Parameters:
      source - The source code element of the new node.
      function - The name of the function of the reduction node.
      variables - The variables of the reduction clause.
      Returns:
      The new OpenMP reduction node.

    • newWorksharingNode

      OmpWorksharingNode newWorksharingNode(Source source, OmpWorksharingNode.OmpWorksharingNodeKind kind)
      Creates a new OpenMP worksharing node with a specific kind. The kind could be:
      • SECTIONS
      • SINGLE
      • SECTION
      • FOR
      Parameters:
      source - The source code element of the new node.
      kind - The kind of the worksharing node, either FOR, SECTIONS, SECTION or SINGLE.
      Returns:
      The new OpenMP worksharing node.

    • configuration

      Configuration configuration()
      gets the configuration associated with this translation task.
      Returns:
      the configuration associated with this translation task.

    • newWildcardNode

      WildcardNode newWildcardNode(Source source)
      creates a new wildcard (...) node.
      Parameters:
      source -
      Returns:

    • newStatementExpressionNode

      StatementExpressionNode newStatementExpressionNode(Source source, CompoundStatementNode statement)
      creates a new statement expression node (GNU C extension).
      Parameters:
      source - the source of the node
      statement - the statement enclosed by the expression excluding the expression at end
      Returns:
      the new statement expression node (GNU C extension)

    • newTypeofNode

      TypeofNode newTypeofNode(Source source, ExpressionNode expression)
      creates a new typeof node (GNU C extension)
      Parameters:
      source -
      expression -
      Returns:

    • newMemoryEventNode

      MemoryEventNode newMemoryEventNode(Source source, MemoryEventNode.MemoryEventNodeKind kind, SequenceNode<ExpressionNode> memoryList)
      creates a new memory event node, which could be either \read , write or reach.
      Parameters:
      source -
      kind -
      memoryList -
      Returns:

    • newOperatorEventNode

      CompositeEventNode newOperatorEventNode(Source source, CompositeEventNode.EventOperator op, DependsEventNode left, DependsEventNode right)
      creates a new composite event node, which is composed by two events node and an operator.
      Parameters:
      source -
      op -
      left -
      right -
      Returns:

    • newNothingNode

      NothingNode newNothingNode(Source source)
      creates a \nothing node which represents an empty set of memory units.
      Parameters:
      source -
      Returns:

    • newBehaviorNode

      BehaviorNode newBehaviorNode(Source source, IdentifierNode name, SequenceNode<ContractNode> body)
      creates a behavior node. (ACSL contract)
      Parameters:
      source -
      name -
      body -
      Returns:

    • newCompletenessNode

      CompletenessNode newCompletenessNode(Source source, boolean isComplete, SequenceNode<IdentifierNode> idList)
      creates a completeness clause node, which could be complete or disjoint
      Parameters:
      source -
      isComplete - true if to create a complete clause node, otherwise, a disjoint clause node
      idList -
      Returns:

    • newAssumesNode

      AssumesNode newAssumesNode(Source source, ExpressionNode predicate)
      Creates a new assumes clause node
      Parameters:
      source -
      predicate -
      Returns:

    • newInvariantNode

      InvariantNode newInvariantNode(Source source, boolean isLoopInvariant, ExpressionNode expression)
      Creates a new invariant clause node
      Parameters:
      source -
      expression -
      Returns:

    • newNoactNode

      NoactNode newNoactNode(Source source)
      Creates a new \noact event node
      Parameters:
      source -
      Returns:

    • newAnyactNode

      AnyactNode newAnyactNode(Source source)
      Creates a new \anyact event node
      Parameters:
      source -
      Returns:

    • newCallEventNode

      CallEventNode newCallEventNode(Source source, IdentifierExpressionNode function, SequenceNode<ExpressionNode> args)
      Creates a new \call event node
      Parameters:
      source -
      function -
      args -
      Returns:

    • typeFactory

      TypeFactory typeFactory()
      Returns a reference to a TypeFactory
      Returns:

    • newUpdateNode

      UpdateNode newUpdateNode(Source source, ExpressionNode collator, FunctionCallNode call)
      Create a new UpdateNode
      Parameters:
      source - The Source attached to the $update expression
      collator - The expression has the $collator type
      call - The FunctionCallNode attached with this expression.
      Returns:
      A new UpdateNode

    • newRunNode

      RunNode newRunNode(Source source, StatementNode statement)
      Create a new RunNode
      Parameters:
      source - The Source attached to the $run statement
      statement - The statement attached with the $run statement
      Returns:
      A new RunNode

    • newObjectofNode

      ObjectOrRegionOfNode newObjectofNode(Source source, ExpressionNode operand)
      Creates a new $object_of node
      Parameters:
      source - the source of the $object_of node
      operand - the operand of the $object_of node, which shall have pointer type
      Returns:
      the new $object_of node

    • newRegionofNode

      ObjectOrRegionOfNode newRegionofNode(Source source, ExpressionNode operand)
      Creates a new $region_of node
      Parameters:
      source - the source of the $region_of node
      operand - the operand of the $region_of node, which shall have pointer type
      Returns:
      the new $region_of node

    • newAllocationNode

      AllocationNode newAllocationNode(Source source, boolean isAllocates, SequenceNode<ExpressionNode> memoryList)
      Creates a new allocation node, which represents either an allocates or frees clause.
      Parameters:
      source - the source of the allocation clause
      isAllocates - true if this is an allocates clause, otherwise, a frees clause
      memoryList - the list of memory units of the allocation clause
      Returns:
      the new allocation node

    • newExtendedQuantifiedExpressionNode

      ExtendedQuantifiedExpressionNode newExtendedQuantifiedExpressionNode(Source source, ExtendedQuantifiedExpressionNode.ExtendedQuantifier quant, ExpressionNode lo, ExpressionNode hi, ExpressionNode function)
      Creates a new extended quantified expression node.
      Parameters:
      source - the source of the node
      quant - the extended quantifier, which could be one of \sum, \max, \min, \numof, \product.
      lo - the lower bound argument
      hi - the upper bound argument
      function - the function argument
      Returns:
      the new extended quantified expression node.

    • newPredicateNode

      PredicateNode newPredicateNode(Source source, IdentifierNode identifier, SequenceNode<VariableDeclarationNode> parameters, ExpressionNode body)
      Creates a new PredicateNode for ACSL predicates
      Parameters:
      source - the source of the new node
      identifier - the IdentifierNode of the predicate identifier
      parameters - parameters used in the predicate definition
      body - the predicate body expression
      Returns:

    • newFocusLoopNode

      FocusLoopTransformNode newFocusLoopNode(Source source, TokenFactory tokenFactory, String focusTag, SequenceNode<ExpressionNode> tagWindow, SequenceNode<ExpressionNode> memoryList)

    • newFocusOrderedNode

      FocusOrderedTransformNode newFocusOrderedNode(Source source, TokenFactory tokenFactory, String focusTag, OperatorNode operator, RegularRangeNode range, ExpressionNode expr)

    • newFocusAssertNode

      FocusAssertTransformNode newFocusAssertNode(Source source, TokenFactory tokenFactory, List<String> focusTags)

    • newInsertTransformNode

      InsertTransformNode newInsertTransformNode(Source source, List<BlockItemNode> nodesToInsert, boolean insertAfter)