declarations

c.FileDeclaration

record FileDeclaration

A declaration at file scope: its node, its name, the type and whether it initializes (none for not an object), and whether it is a typedef.

c.Declarations.tags

def Declarations.tags (items : List Item) : List String

The struct and union tags a program defines.

c.Declarations.incomplete

def Declarations.incomplete (tags : List String) (t : TypeSyntax) : Bool

Whether a type is a struct or union the program does not define.

c.Declarations.atFileScope

def Declarations.atFileScope (it : Item) : List FileDeclaration

The declarations an item makes in the ordinary name space at file scope.

c.Declarations.compatible

def Declarations.compatible (earlier : FileDeclaration) (later : FileDeclaration) : Bool

Whether a later declaration at file scope can be the same entity as an earlier one: both objects of the same type, not both initializing it; two typedefs are left to the core (the same type again is allowed, Program.typeNames).

c.Declarations.clashAtFileScope

def Declarations.clashAtFileScope (seen : List FileDeclaration) (ds : List FileDeclaration) : Option (NodeId * Refusal)

The first declaration at file scope that clashes with an earlier one of the same name.

c.Declarations.inFunction

def Declarations.inFunction (tags : List String) (f : FunctionDefinition) : Option (NodeId * Refusal)

What is wrong with a function’s declarations: a parameter of an incomplete type.

c.Declarations.unnamed

def Declarations.unnamed (it : Item) : Option (NodeId * String)

A struct or union without a named member, neither its own nor through an anonymous struct or union (C11 6.7.2.1p8; the anonymous one’s definition is checked by itself).

c.Declarations.definitions

def Declarations.definitions (items : List Item) : List (String * List Field)

The structs and unions the items define, by name: their members.

c.StructDefinition.named

def StructDefinition.named (d : StructDefinition) : List (String * List Field)

The name of the struct or union d with its members.

c.Declarations.membersOf

def Declarations.membersOf (definitions : List (String * List Field)) (x : String) : Option (List Field)

The members of the struct or union named x among the definitions.

c.Declarations.memberNames

def Declarations.memberNames (definitions : List (String * List Field)) (depth : Nat) (fs : List Field) : List String

The names of the members fs, those of an anonymous struct or union among them (its members in definitions; C11 6.7.2.1p13: they are members of the one it is in), at most depth anonymous ones deep.

c.Declarations.repeated

def Declarations.repeated (names : List String) : Option String

The first of the names that comes again later.

c.Declarations.duplicateMember

def Declarations.duplicateMember (definitions : List (String * List Field)) (it : Item) : Option (NodeId * String)

The item it if it is a struct or union with two members of the same name, its own or an anonymous one’s (found in definitions; C11 6.7.2.1p13, 6.2.3p1).

c.Declarations.typedefs

def Declarations.typedefs (items : List Item) : List (String * TypeSyntax)

The typedefs of the items: names to the types they stand for.

c.Declarations.lookup

def Declarations.lookup (name : String) (typedefs : List (String * TypeSyntax)) : Option TypeSyntax

The type a typedef name stands for.

c.TypeSyntax.resolve

def TypeSyntax.resolve (typedefs : List (String * TypeSyntax)) (fuel : Nat) (t : TypeSyntax) : TypeSyntax

A type with its typedef names replaced, the outermost one at a time (fuel: at most the number of typedefs).

c.TypeSyntax.isFunctionType

def TypeSyntax.isFunctionType (typedefs : List (String * TypeSyntax)) (t : TypeSyntax) : Bool

Whether a type is a function type, through typedefs.

c.Declarations.writtenTypes

def Declarations.writtenTypes (it : Item) : List (NodeId * TypeSyntax)

The types an item writes in its declarations, with their nodes: objects, typedefs, a function’s result and parameters, a struct’s members, and the declarations in a function’s body.

c.Declarations.expressionTypes

def Declarations.expressionTypes (e : Expr) : List (NodeId * TypeSyntax)

The types written in casts and sizeof, with their nodes.

c.Declarations.qualifiedFunction

def Declarations.qualifiedFunction (items : List Item) : Option (NodeId * String)

The first place a function type is qualified (C11 6.7.3p9).

c.Declarations.firstWrong

def Declarations.firstWrong (items : List Item) : Option (NodeId * Refusal)

The first declaration C rejects: a clash at file scope, a struct or union without a named member or with two members of the same name, a function’s.