• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • C
          • Syntax-for-tools
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Compilation-database
            • Printer
            • Output-files
            • Abstract-syntax-operations
            • Implementation-environments
            • Abstract-syntax
            • Concrete-syntax
            • Disambiguation
            • Validation
              • Validator
              • Validation-information
                • Abstract-syntax-annop
                  • Exprs/decls/stmts-annop
                  • Filepath-transunit-map-annop
                  • Transunit-ensemble-annop
                  • Code-ensemble-annop
                  • Ident-option-annop
                  • Iconst-option-annop
                  • Extdecl-list-annop
                  • Const-option-annop
                  • Transunit-annop
                  • Ident-list-annop
                  • Attrib-name-annop
                  • Fundef-annop
                  • Extdecl-annop
                  • Iconst-annop
                  • Const-annop
                  • Ident-annop
                  • Typequal/attribspec-list-list-annop
                  • Typequal/attribspec-list-annop
                  • Typequal/attribspec-annop
                  • Struni-spec-annop
                  • Struct-declor-list-annop
                  • Struct-declor-annop
                  • Struct-declon-list-annop
                  • Struct-declon-annop
                  • Statassert-annop
                  • Spec/qual-list-annop
                  • Spec/qual-annop
                  • Param-declor-annop
                  • Param-declon-list-annop
                  • Param-declon-annop
                  • Member-designor-annop
                  • Initer-option-annop
                  • Initdeclor-list-annop
                  • Initdeclor-annop
                  • Genassoc-list-annop
                  • Expr-option-annop
                  • Enumer-list-annop
                  • Dirabsdeclor-option-annop
                  • Dirabsdeclor-annop
                  • Desiniter-list-annop
                  • Designor-list-annop
                  • Declor-option-annop
                  • Decl-spec-list-annop
                  • Const-expr-option-annop
                  • Const-expr-annop
                  • Block-item-list-annop
                  • Block-item-annop
                  • Attrib-spec-list-annop
                  • Attrib-spec-annop
                  • Attrib-list-annop
                  • Asm-output-list-annop
                  • Asm-output-annop
                  • Asm-input-list-annop
                  • Amb-expr/tyname-annop
                  • Amb-decl/stmt-annop
                  • Amb-declor/absdeclor-annop
                  • Align-spec-annop
                  • Absdeclor-option-annop
                  • Type-spec-annop
                  • Tyname-annop
                  • Stmt-annop
                  • Label-annop
                  • Initer-annop
                  • Genassoc-annop
                  • Expr-list-annop
                  • Expr-annop
                  • Enumer-annop
                  • Enum-spec-annop
                  • Dirdeclor-annop
                  • Desiniter-annop
                  • Designor-annop
                  • Declor-annop
                  • Decl-spec-annop
                  • Decl-list-annop
                  • Decl-annop
                  • Comp-stmt-annop
                  • Attrib-annop
                  • Asm-stmt-annop
                  • Asm-input-annop
                  • Absdeclor-annop
                • Types
                • Abstract-syntax-anno-additional-theroems
                • Valid-ext-info
                • Valid-table
                • Valid-ord-info
                • Uid
                • Stmts-types
                • Lifetime
                • Initdeclor-info
                • Fundef-types
                • Expr-type
                • Valid-defstatus
                • Var-info
                • Valid-ord-info-option
                • Valid-ext-info-option
                • Uid-option
                • Linkage-option
                • Linkage
                • Lifetime-option
                • Valid-table-option
                • Iconst-info
                • Param-declor-nonabstract-info
                • Fundef-info
                • Expr-null-pointer-constp
                • Valid-scope
                • Const-expr-null-pointer-constp
                • Expr-string-info
                • Expr-funcall-info
                • Expr-arrsub-info
                • Tyname-info
                • Transunit-info
                • Expr-unary-info
                • Expr-const-info
                • Expr-binary-info
                • Stmt-types
                • Block-item-list-types
                • Initer-type
                • Valid-ord-scope
                • Uid-increment
                • Uid-equal
                • Coerce-var-info
                • Valid-externals
                • Irr-var-info
                • Valid-scope-list
                • Irr-valid-table
                • Irr-lifetime
                • Irr-uid
                • Irr-linkage
                • Block-item-types
                • Comp-stmt-types
            • Gcc-builtins
            • Preprocessing
            • Parsing
          • Atc
          • Transformation-tools
          • Language
          • Representation
          • Insertion-sort
          • Pack
        • Soft
        • Bv
        • Imp-language
        • Ethereum
        • Event-macros
        • Java
        • Riscv
        • Bitcoin
        • Zcash
        • Yul
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Axe
        • Lists-light
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Validation-information

Abstract-syntax-annop

Definition of the predicates that check whether the abstract syntax is annotated with validation information.

We use fty::deffold-reduce to define these predicates concisely.

The :default value is t, meaning that there are no constraints by default.

The :combine operator is and, because we need to check all the constructs, recursively.

We override the predicate for the constructs for which the validator adds information.

Since for now the validator accepts GCC attribute and other extensions without actually checking them and their constituents, we also have the annotation predicates accept those constructs, by overriding those cases to return t.

The validator operates on unambiguous abstract syntax, which satisfies the unambiguity predicates. Ideally, the annotation predicates should use the unambiguity predicates as guards, but fty::deffold-reduce does not support that feature yet. Thus, for now we add run-time checks, in the form of raise, for the cases in which the unambiguity predicates do not hold; note that raise is logically nil, so the annotation predicates are false on ambiguous constructs.

Subtopics

Exprs/decls/stmts-annop
Filepath-transunit-map-annop
Transunit-ensemble-annop
Code-ensemble-annop
Ident-option-annop
Iconst-option-annop
Extdecl-list-annop
Const-option-annop
Transunit-annop
Ident-list-annop
Attrib-name-annop
Fundef-annop
Extdecl-annop
Iconst-annop
Const-annop
Ident-annop
Typequal/attribspec-list-list-annop
Typequal/attribspec-list-annop
Typequal/attribspec-annop
Struni-spec-annop
Struct-declor-list-annop
Struct-declor-annop
Struct-declon-list-annop
Struct-declon-annop
Statassert-annop
Spec/qual-list-annop
Spec/qual-annop
Param-declor-annop
Param-declon-list-annop
Param-declon-annop
Member-designor-annop
Initer-option-annop
Initdeclor-list-annop
Initdeclor-annop
Genassoc-list-annop
Expr-option-annop
Enumer-list-annop
Dirabsdeclor-option-annop
Dirabsdeclor-annop
Desiniter-list-annop
Designor-list-annop
Declor-option-annop
Decl-spec-list-annop
Const-expr-option-annop
Const-expr-annop
Block-item-list-annop
Block-item-annop
Attrib-spec-list-annop
Attrib-spec-annop
Attrib-list-annop
Asm-output-list-annop
Asm-output-annop
Asm-input-list-annop
Amb-expr/tyname-annop
Amb-decl/stmt-annop
Amb-declor/absdeclor-annop
Align-spec-annop
Absdeclor-option-annop
Type-spec-annop
Tyname-annop
Stmt-annop
Label-annop
Initer-annop
Genassoc-annop
Expr-list-annop
Expr-annop
Enumer-annop
Enum-spec-annop
Dirdeclor-annop
Desiniter-annop
Designor-annop
Declor-annop
Decl-spec-annop
Decl-list-annop
Decl-annop
Comp-stmt-annop
Attrib-annop
Asm-stmt-annop
Asm-input-annop
Absdeclor-annop