names

cpp.Names.ambiguousMarker

def Names.ambiguousMarker : String

The marker an ambiguous use is rewritten to (rejected when checked).

cpp.Names.possibleMarker

def Names.possibleMarker : String

The marker a use is rewritten to when the name may also come from a header (only to see whether it is used).

cpp.Names.qualified

def Names.qualified (x : String) : Bool

Whether a name is qualified (has :: in it).

cpp.Names.declared

def Names.declared (items : List Item) : List String

The names an item list declares directly (an unnamed or inline namespace’s too).

cpp.Names.table

def Names.table (pre : String) (items : List Item) : List (String * List String)

Each named namespace (its full name) with the names it declares directly.

cpp.Names.throughInline

def Names.throughInline (pre : String) (items : List Item) : List (String * String)

An inline namespace’s names as written through the namespace around it (lib::f for lib::v1::f).

cpp.Names.known

def Names.known (tbl : List (String * List String)) : List String

Every full name the namespaces declare.

cpp.Names.prefixes

def Names.prefixes (pre : String) : List String

The prefixes of a namespace prefix, innermost first: a::b::, a::, the empty one.

cpp.Names.chased

def Names.chased (vis : List (String * String)) (fuel : Nat) (y : String) : String

A name looked up again while it maps to another (an inline namespace’s member through two of them).

cpp.Names.resolved

def Names.resolved (pre : String) (known : List String) (vis : List (String * String)) (x : String) : String

A name used in the current namespace, as its full name.

cpp.Names.rewriting

def Names.rewriting (pre : String) (known : List String) (vis : List (String * String)) : SyntaxMap

Rewriting the names used, with the names visible.

cpp.Names.bases

def Names.bases (sm : SyntaxMap) (bs : List Base) : List Base

A class’s bases with their names resolved.

cpp.Names.ofClass

def Names.ofClass (pre : String) (sm : SyntaxMap) (d : ClassDefinition) : ClassDefinition

A class with its own name prefixed and the names in it resolved.

cpp.Names.ofFunction

def Names.ofFunction (pre : String) (sm : SyntaxMap) (f : FunctionDefinition) : FunctionDefinition

A function with its own name prefixed and the names in it resolved.

cpp.Names.ofStruct

def Names.ofStruct (pre : String) (sm : SyntaxMap) (d : StructDefinition) : StructDefinition

A struct or union with its own name prefixed and the names in it resolved.

cpp.Names.item

def Names.item (pre : String) (sm : SyntaxMap) (it : Item) : Item

An item in a namespace: its own name prefixed, the names in it resolved.

cpp.Names.namespaceNamed

def Names.namespaceNamed (pre : String) (x : String) (tbl : List (String * List String)) : String

The full name of a namespace a using-directive or an alias names: the current namespace’s first, else the outermost one.

cpp.Names.members

def Names.members (tbl : List (String * List String)) (ns : String) : List String

The names a namespace declares in all its definitions (a namespace may be opened more than once).

cpp.Names.usingNames

def Names.usingNames (ns : String) (tbl : List (String * List String)) : List (String * String)

The names a using-directive makes visible: each name the namespace declares, to its full name.

cpp.Names.declarationNames

def Names.declarationNames (pre : String) (qualified : String) (tbl : List (String * List String)) : List (String * String)

The name a using-declaration makes visible (using a::b::x;: x, to the full name of a::b’s x), when the namespace declares it; nothing otherwise.

cpp.Names.aliasNames

def Names.aliasNames (alias : String) (target : String) (names : List String) : List (String * String)

The names an alias makes visible: each full name under the target written with the alias instead.

cpp.Names.flattenedIn

def Names.flattenedIn (fuel : Nat) (pre : String) (vis : List (String * String)) (tbl : List (String * List String)) (items : List Item) : List Item

The items of a namespace flattened: its declarations visible to all of them, then each item in turn.

cpp.Names.flattenedItems

def Names.flattenedItems (fuel : Nat) (pre : String) (vis : List (String * String)) (tbl : List (String * List String)) (items : List Item) : List Item

Items flattened in order (a using-directive or alias affects the items after it).

cpp.Names.fuel

def Names.fuel (items : List Item) : Nat

How deep namespaces may nest (and how many items there may be) for flattening.

cpp.Names.protectedMarker

def Names.protectedMarker : String

Marked names of nested classes used where their access does not let them be ([class.access]p1): the class’s name and its enclosing class’s, after the marker.

cpp.Names.privateMarker

def Names.privateMarker : String

See Names.protectedMarker.

cpp.Names.nestedIn

def Names.nestedIn (ms : List Member) : List (String * Access)

The types a class defines (its classes, unions and named enumerations), each with its access.

cpp.Names.ownMembers

def Names.ownMembers (ms : List Member) : List Member

A class’s members other than the classes it defines.

cpp.Names.inScopeOf

def Names.inScopeOf (x : String) (names : List String) (types : List String) : SyntaxMap

Writing a nested class’s name y (of class x) as x::y, and a member type’s (typedef): they are found in x’s scope ([class.nest]p1, [class.mem]p1); a member type is the program’s typedef x::y (cpp.classes).

cpp.Names.memberTypes

def Names.memberTypes (ms : List Member) : List String

The names of a class’s member types (typedefs).

cpp.Names.liftedClass

def Names.liftedClass (fuel : Nat) (d : ClassDefinition) : List Item

A class with the classes it defines before it, each its own class named Outer::Inner, outermost last; in all of them a nested class’s name is written in full.

cpp.HiddenClass

record HiddenClass

A non-public nested class: its full name, its access, and the class that defines it.

cpp.Names.hiddenType

def Names.hiddenType (x : String) (y : String) (acc : Access) : List HiddenClass

A union or an enumeration class x defines, if it is not public.

cpp.Names.hiddenIn

def Names.hiddenIn (fuel : Nat) (items : List Item) : List HiddenClass

The non-public nested classes, unions and enumerations of the items’ classes (full name, access, enclosing class), deepest included.

cpp.Names.liftedItems

def Names.liftedItems (fuel : Nat) (items : List Item) : List Item

The items, each class with its nested classes unnested (in namespaces too).

cpp.Names.derives

def Names.derives (fuel : Nat) (items : List Item) (c : String) (b : String) : Bool

Whether class c derives from class b, among the items’ classes.

cpp.Names.mayUse

def Names.mayUse (fuel : Nat) (items : List Item) (o : String) (acc : Access) (it : Item) : Bool

Whether an item may use a nested class of class o with an access: o’s own class and the classes nested in it, a class o befriends or a function it befriends by name; for a protected one also o’s derived classes.

cpp.Names.named

def Names.named (z : String) (h : HiddenClass) : Bool

Whether a hidden class is the one named z.

cpp.Names.markedHidden

def Names.markedHidden (fuel : Nat) (hidden : List HiddenClass) (items : List Item) (it : Item) : Item

An item with the hidden nested classes it may not use marked.

cpp.Names.lifted

def Names.lifted (fuel : Nat) (items : List Item) : List Item

The items with their nested classes unnested (Names.liftedClass), and a non-public one’s name marked where it is used outside the class that defines it (and that class’s nested classes, friends, and for a protected one its derived classes).

cpp.Names.flattened

def Names.flattened (written : List Item) : List Item

A program’s items flattened (the functions the branch provides under std are std’s members too, for a using namespace std;).

cpp.OutermostName

data OutermostName

What a name the program declares at the outermost level is: a function, a type, or an object (by its declaration).

cpp.Names.outermost

def Names.outermost (items : List Item) : List (String * OutermostName)

The names the program declares at the outermost level, with what they are.

cpp.Names.includes

def Names.includes (items : List Item) : List String

The headers the program includes.

cpp.Names.usesStd

def Names.usesStd (items : List Item) : Bool

Whether the program has using namespace std at the outermost level.

cpp.Names.indexOf

def Names.indexOf (h : String) (hs : List String) (k : Nat) : Option Nat

Where a header is in the list, from k.

cpp.Names.level

def Names.level (code : String) (headers : List String) : Nat

How strongly the headers declare a name in std, from its code (a kind, then one digit per header): 1 required, 2 possibly through other headers, 0 not.

cpp.Names.collisions

def Names.collisions (marker : String) (want : Nat) (items : List Item) : List (String * String)

The collisions of a level: the names (an object’s as its declaration) with the marker they are rewritten to.

cpp.Names.marked

def Names.marked (marks : List (String * String)) (items : List Item) : List Item

The items with the uses of colliding names rewritten to markers (the declarations stay).

cpp.Names.usesPossible

def Names.usesPossible (e : Expr) : Bool

Whether an expression uses a name marked possible.

cpp.Names.markedType

def Names.markedType (marker : String) (t : TypeSyntax) : Bool

Whether a type names a marked type.

cpp.Names.noteName

def Names.noteName : String

The name a call to note a possible collision has (put first in the run’s entry).

cpp.Names.noted

def Names.noted (entry : String) (n : NodeId) (items : List Item) : List Item

The run’s entry (its name) with a possible collision noted first.

cpp.Names.standardFunction

def Names.standardFunction (name : String) : Bool

Whether a name is a function of the standard library: std declares it (on either implementation) as a function.

cpp.Names.cFunction

def Names.cFunction (name : String) : Bool

Whether a header of the C library declares a function (required, as both implementations do): it is in the global namespace too, without using namespace std.

cpp.Names.requiredAt

def Names.requiredAt (code : String) (positions : List Nat) : Bool

Whether a code has a 1 (required) at one of the positions.

cpp.Names.distinct

def Names.distinct (seen : List String) (names : List String) : List String

The names in order, each once.

cpp.Names.qualifiedStandardCalls

def Names.qualifiedStandardCalls (items : List Item) (flat : List Item) : List Item

Under using namespace std, the calls of std’s functions that neither the program nor a library defines, named std::f ([namespace.udir]p2: the directive makes them visible), so that the branch tells them apart from undeclared names. A function of the C library stays as written (it is in the global namespace, and the core models some by name).

cpp.Names.standardType

def Names.standardType (x : String) : Option TypeSyntax

The written type of the class the model makes for the standard library’s type std::x, if it makes one: a standard exception’s (tStdExc, cpp.standardexceptions), std::ostream’s (tOstream) and std::istream’s (cpp.operators). A library header’s classes are not these: the flattening finds them (Names.flattened).

cpp.Names.standardTypeName

def Names.standardTypeName (name : String) : Bool

Whether name is a type of the standard library: std declares it (on either implementation) as a type.

cpp.Names.classNames

def Names.classNames (items : List Item) : List String

The class names written in the types of the items.

cpp.Names.qualifiedStandardTypes

def Names.qualifiedStandardTypes (items : List Item) (flat : List Item) : List Item

The standard library’s types whose classes the model makes (Names.standardType) written as the model’s: with std:: (std::length_error as a class’s name), and under using namespace std without it when std declares the name as a type (the standard names’ table, cpp.standardnames) and neither the program nor a library declares it ([namespace.udir]p2). Other names stay as written (a library class’s member type iterator is not std::iterator). flat is the program’s items flattened (Names.flattened), items as written (where the directive is).

cpp.Names.prepare

def Names.prepare (entry : String) (p : Program) : Program

A program with its namespaces flattened and its colliding names marked (a possible collision the program uses noted at the start of the run’s entry, of the name given).

cpp.Names.ambiguous

def Names.ambiguous (x : String) : String

clang’s words for an ambiguous use.

cpp.Names.expression

def Names.expression (e : Expr) : Option (CheckResult Cpp.constructs (Lifted Cpp.constructs))

A use of an ambiguous name, rejected; the note of a possible collision.

cpp.Names.ofDeclaration

def Names.ofDeclaration (x : DeclId) : String

The name a declaration’s id is written with: the part before its @ (HIGH@6:11 is HIGH).

cpp.Names.enumeratorName

def Names.enumeratorName (names : TypeNames) (x : DeclId) : String

The name the enumeration constant x is written with outside its enumeration: its own, or through its enumeration where that is scoped (Color::Red, C++ [dcl.enum]p11), by the type names names.

cpp.Names.constant

def Names.constant (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (asLvalue : Bool) (e : Expr) : Option (CheckResult Cpp.constructs (Lifted Cpp.constructs))

eConst n name: a constant or an object the program’s environment declares (an Arduino board’s HIGH, A0; the library’s Serial), the global declared with that name; the outermost one (the environment’s items come before the program’s). Where an lvalue is wanted (an object a member function is called on) it is the global itself. Without such a global, an enumeration constant of that name (a header’s WL_CONNECTED); else none, for the core’s macro constants.

cpp.Names.markedIn

def Names.markedIn (t : TypeSyntax) : Option String

The marked name a type uses, if any.

cpp.Names.inaccessible

def Names.inaccessible (marked : String) : Option String

clang’s words for a nested class used where its access does not let it be, from its marked name.

cpp.Names.inaccessibleIn

def Names.inaccessibleIn (t : TypeSyntax) : Option String

The words for the first nested class a type uses where its access does not let it be, if any.

cpp.Names.statement

def Names.statement (s : Stmt) : Option (CheckResult Cpp.constructs (TypedStmt Cpp.constructs))

A declaration of an ambiguous type, or of a nested class it may not use, rejected; the note of a possible collision, as the divergence it is.