• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
        • Soft
        • C
          • Syntax-for-tools
          • Atc
          • Language
            • Abstract-syntax
            • Integer-ranges
            • Implementation-environments
            • Dynamic-semantics
            • Static-semantics
              • Check-stmt
              • Check-cond
              • Check-binary-pure
              • Var-table-add-var
              • Check-unary
              • Check-obj-declon
              • Fun-table-add-fun
              • Check-fundef
              • Fun-sinfo
              • Check-expr-asg
              • Check-expr-call
              • Check-arrsub
              • Uaconvert-types
              • Apconvert-type-list
              • Check-initer
              • Adjust-type-list
              • Types+vartab
              • Promote-type
              • Check-tag-declon
              • Check-expr-call-or-asg
              • Check-ext-declon
              • Check-param-declon
              • Check-member
              • Check-expr-pure
              • Init-type-matchp
              • Check-obj-adeclor
              • Check-memberp
              • Check-expr-call-or-pure
              • Check-cast
              • Check-struct-declon-list
              • Check-fun-declor
              • Expr-type
              • Check-ext-declon-list
              • Check-transunit
              • Check-fun-declon
              • Var-defstatus
              • Struct-member-lookup
              • Preprocess
              • Wellformed
              • Check-tyspecseq
              • Check-param-declon-list
              • Check-iconst
              • Check-expr-pure-list
              • Var-sinfo-option
              • Fun-sinfo-option
              • Var-scope-all-definedp
              • Funtab+vartab+tagenv
              • Var-sinfo
              • Var-table-lookup
              • Apconvert-type
              • Var-table
              • Check-tyname
              • Types+vartab-result
              • Funtab+vartab+tagenv-result
              • Fun-table-lookup
              • Wellformed-result
              • Var-table-add-block
              • Var-table-scope
              • Var-table-result
              • Fun-table-result
              • Expr-type-result
              • Adjust-type
              • Check-fileset
              • Var-table-all-definedp
              • Check-const
              • Fun-table-all-definedp
              • Check-ident
              • Fun-table
              • Var-table-init
              • Fun-table-init
            • Grammar
            • Integer-formats
            • Types
            • Portable-ascii-identifiers
            • Values
            • Integer-operations
            • Computation-states
            • Object-designators
            • Operations
            • Errors
            • Tag-environments
            • Function-environments
            • Character-sets
            • Flexible-array-member-removal
            • Arithmetic-operations
            • Pointer-operations
            • Bytes
            • Keywords
            • Real-operations
            • Array-operations
            • Scalar-operations
            • Structure-operations
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Language

Static-semantics

A static semantics of C.

This static semantics consists of ACL2 functions that check whether the abstract syntactic entities satisfy the needed constraints. If the constraints are satisfied, additional information (e.g. types) may be returned, used to check constraints on enclosing abstract syntactic entities.

Subtopics

Check-stmt
Check a statement.
Check-cond
Check a ternary conditional expression [C17:6.5.15].
Check-binary-pure
Check the application of a pure binary operator to two expressions.
Var-table-add-var
Add a variable to (the innermost scope of) a variable table.
Check-unary
Check the application of a unary operator to an expression.
Check-obj-declon
Check an object declaration.
Fun-table-add-fun
Add static information about a function to a function table.
Check-fundef
Check a function definition.
Fun-sinfo
Fixtype of static information about functions.
Check-expr-asg
Check an expression that must be an assignment expression.
Check-expr-call
Check an expression that is a function call.
Check-arrsub
Check an array subscripting expression [C17:6.5.2.1].
Uaconvert-types
Apply the usual arithmetic conversions to two arithmetic types [C17:6.3.1.8].
Apconvert-type-list
Lift apconvert-type to lists.
Check-initer
Check an initializer.
Adjust-type-list
Lift adjust-type to lists.
Types+vartab
Fixtype of pairs consisting of a non-empty set of types and a variable table.
Promote-type
Apply the integer promotions to an arithmetic type [C17:6.3.1.1/2].
Check-tag-declon
Check a tag declaration.
Check-expr-call-or-asg
Check an expression that must be a function call or an assignment.
Check-ext-declon
Check an external declaration.
Check-param-declon
Check a parameter declaration.
Check-member
Check a structure member expression [C17:6.5.2.3].
Check-expr-pure
Check a pure expression.
Init-type-matchp
Check if an initializer type matches a type.
Check-obj-adeclor
Check an abstract object declarator.
Check-memberp
Check a structure pointer member expression [C17:6.5.2.3].
Check-expr-call-or-pure
Check an expression that must be a function call or a pure expression.
Check-cast
Check a cast expression [C17:6.5.4].
Check-struct-declon-list
Check a list of structure declarations.
Check-fun-declor
Check a function declarator.
Expr-type
Fixtype of expression types.
Check-ext-declon-list
Check a list of external declarations.
Check-transunit
Check a translation unit.
Check-fun-declon
Check a function declaration.
Var-defstatus
Fixtype of definition statuses of variables.
Struct-member-lookup
Look up a member in a structure type in the tag environment.
Preprocess
Preprocess a file set [C17:5.1.1.2/4].
Wellformed
Fixtype of the well-formedness indicator.
Check-tyspecseq
Check a type specifier sequence.
Check-param-declon-list
Check a list of parameter declarations.
Check-iconst
Check an integer constant.
Check-expr-pure-list
Check a list of pure expressions.
Var-sinfo-option
Fixtype of optional static information about variables.
Fun-sinfo-option
Fixtype of optional static information about functions.
Var-scope-all-definedp
CHeck if all the variables in a scope are defined.
Funtab+vartab+tagenv
Fixtype of triples consisting of a function table, a variable table, and a tag environment.
Var-sinfo
Fixtype of static information about variables.
Var-table-lookup
Look up a variable in a variable table.
Apconvert-type
Convert array type to pointer type.
Var-table
Fixtype of variable tables, i.e. symbol tables for variables.
Check-tyname
Check a type name.
Types+vartab-result
Fixtype of errors and pairs consisting of a non-empty set of types and a variable table.
Funtab+vartab+tagenv-result
Fixtype of errors and triples consisting of a function table, a variable table, and a tag environment.
Fun-table-lookup
Look up a function in a function table.
Wellformed-result
Fixtype of errors and the wellformed indicator.
Var-table-add-block
Add a block scope to a variable table.
Var-table-scope
Fixtype of scopes of variable tables.
Var-table-result
Fixtype of errors and variable tables.
Fun-table-result
Fixtype of errors and function tables.
Expr-type-result
Fixtype of errors and expression types.
Adjust-type
Adjust a parameter type.
Check-fileset
Check a file set.
Var-table-all-definedp
CHeck if all the variables in a file scope are defined.
Check-const
Check a constant.
Fun-table-all-definedp
Check if all the functions in a table are defined.
Check-ident
Check an identifier.
Fun-table
Fixtype of function tables, i.e. symbol tables for functions.
Var-table-init
Create an initial variable table.
Fun-table-init
Create an initial function table.