• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • C
        • Syntax-for-tools
          • Formalized-subset
          • Mapping-to-language-definition
          • Input-files
          • Compilation-database
          • Printer
          • Output-files
          • Abstract-syntax-operations
            • Expr-priority
            • Expr-priority-<=
            • Combine-dirabsdeclor-into-dirabsdeclor
            • Declor/dirdeclor-rename
            • Check-decl-spec-list-all-typespec/stoclass
            • Binop-expected-priorities
            • Expr->priority
            • Transunit-at-path
            • Declor/dirdeclor->ident
            • Declor/dirdeclor-has-params-p
            • Check-expr-binary
            • Apply-post-inc/dec-ops
            • Check-spec/qual-list-all-typespec
            • Apply-pre-inc/dec-ops
            • Check-decl-spec-list-all-typespec
            • Expr-to-asg-expr-list
            • Check-expr-mul
            • Expr-unary/postfix/primary-p
            • Transunit-ensemble-paths
            • Check-struni-spec-no-members
            • Expr-postfix/primary-p
            • Dirabsdeclor-declor?-nil-p
            • Check-enum-spec-no-list
            • Expr-zerop
            • Expr-priority->=
            • Decl-spec-list-to-stor-spec-list
            • Spec/qual-list-to-type-spec-list
            • Expr-priority->
            • Expr-priority-<
            • Declor-spec-list-filter-out-linkage-specs
            • Decl-spec-list-to-type-spec-list
            • Ident-list-map-expr-ident
            • Binop->priority
            • Stringlit-list->prefix?-list
            • Declor-spec-list-make-static
            • Binop-strictp
            • Check-expr-iconst
            • Init-declor->ident
            • Check-expr-ident
            • Dirabsdeclor-to-dirdeclor
            • Dirabsdeclor-option-to-dirdeclor
            • Dirdeclor-has-params-p
            • Absdeclor-to-declor
            • Dirdeclor-rename
            • Declor-rename
            • Declor-has-params-p
            • Dirdeclor->ident
            • Declor->ident
          • Implementation-environments
          • Abstract-syntax
          • Concrete-syntax
          • Disambiguation
          • Validation
          • Gcc-builtins
          • Preprocessing
          • Parsing
        • Atc
        • Transformation-tools
        • Language
        • Representation
        • Insertion-sort
        • Pack
      • Proof-checker-array
      • Soft
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Ethereum
      • Leftist-trees
      • Java
      • Riscv
      • Taspi
      • Bitcoin
      • Zcash
      • Des
      • X86isa
      • Sha-2
      • Yul
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Axe
      • Poseidon
      • Where-do-i-place-my-book
      • Aleo
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Syntax-for-tools

Abstract-syntax-operations

Operations on the abstract syntax.

Subtopics

Expr-priority
Fixtype of expression priorities.
Expr-priority-<=
Total order on expression priorities: less than or equal to.
Combine-dirabsdeclor-into-dirabsdeclor
Combine a direct abstract declarator into another.
Declor/dirdeclor-rename
Change the identifier of a declarator or direct declarator.
Check-decl-spec-list-all-typespec/stoclass
Check if all the declaration specifiers in a list are type specifiers or storage class specifiers.
Binop-expected-priorities
Expected expression priorities of the operands of the binary operators.
Expr->priority
Priorities of expressions.
Transunit-at-path
Translation unit at a certain path in a translation unit ensemble.
Declor/dirdeclor->ident
Identifier of a declarator or direct declarator.
Declor/dirdeclor-has-params-p
Check if a declarator or direct declarator contains function parameters or names.
Check-expr-binary
Check if an expression is a binary expression.
Apply-post-inc/dec-ops
Apply a sequence of post-increment and post-decrement operators to an expression.
Check-spec/qual-list-all-typespec
Check if all the specifiers and qualifiers in a list are type specifiers.
Apply-pre-inc/dec-ops
Apply a sequence of pre-increment and pre-decrement operators to an expression.
Check-decl-spec-list-all-typespec
Check if all the declaration specifiers in a list are type specifiers.
Expr-to-asg-expr-list
Turn an expression into a list of assignment expressions.
Check-expr-mul
Check if an expression is a multiplication.
Expr-unary/postfix/primary-p
Check if an expression is unary or postfix or primary.
Transunit-ensemble-paths
Set of file paths in a translation unit ensemble.
Check-struni-spec-no-members
Check if a structure or union specifier has no members, returning the name if the check passes.
Expr-postfix/primary-p
Check if an expression is postfix or primary.
Dirabsdeclor-declor?-nil-p
Check if a direct abstract declarator has a declor? component that is nil.
Check-enum-spec-no-list
Check if an enumeration union specifier has no enumerators, returning the name if the check passes.
Expr-zerop
Check if an expression is zero.
Expr-priority->=
Total order on expression priorities: greater than or equal to.
Decl-spec-list-to-stor-spec-list
Extract the list of storage class specifiers from a list of declaration specifiers, preserving the order.
Spec/qual-list-to-type-spec-list
Extract the list of type specifiers from a list of type specifiers and qualifiers, preserving the order.
Expr-priority->
Total order on expression priorities: greater than.
Expr-priority-<
Total order on expression priorities: less than.
Declor-spec-list-filter-out-linkage-specs
Drop declaration specifiers related to linkage.
Decl-spec-list-to-type-spec-list
Extract the list of type specifiers from a list of declaration specifiers, preserving the order.
Ident-list-map-expr-ident
Map expr-ident over a list of identifiers.
Binop->priority
Priority of (binary expressions with) operators.
Stringlit-list->prefix?-list
Lift stringlit->prefix? to lists.
Declor-spec-list-make-static
Add the static declaration specifier and remove all existing specifiers related to linkage.
Binop-strictp
Check if a binary operator is strict.
Check-expr-iconst
Check if an expression is an integer constant, returning the integer constant if the check passes.
Init-declor->ident
Identifier of an initializer declarator.
Check-expr-ident
Check if an expression is an identifier, returning the identifier if the check passes.
Dirabsdeclor-to-dirdeclor
Turn an abstract direct declarator into a regular direct declarator using the provided identifier.
Dirabsdeclor-option-to-dirdeclor
Turn an optional abstract direct declarator into a regular direct declarator using the provided identifier.
Dirdeclor-has-params-p
Check if a direct declarator contains function parameters/names.
Absdeclor-to-declor
Turn an abstract declarator into a regular declarator using the provided identifier.
Dirdeclor-rename
Change the identifier of the direct declarator.
Declor-rename
Change the identifier of the declarator.
Declor-has-params-p
Check if a declarator contains function parameters/names.
Dirdeclor->ident
Identifier of a direct declarator.
Declor->ident
Identifier of a declarator.