classes

cpp.Member.entry

def Member.entry (m : Member) : Option ClassMember

A member’s name and access, if it is a data member, a member function or a name a using-declaration brings in (lookup of the name then stops at the class, [namespace.udecl]p1; the access is the declaration’s, p19).

cpp.Classes.importsOf

def Classes.importsOf (ms : List Member) : List (String * String)

The names a class brings in with using-declarations, each with the base it names.

cpp.Classes.all

def Classes.all {A : Type} (rs : List (CheckResult Cpp.constructs A)) : CheckResult Cpp.constructs (List A)

Every result in order, or the first error.

cpp.Classes.numbered

def Classes.numbered {A : Type} (k : Nat) (xs : List A) : List (Nat * A)

Each element with its position.

cpp.Classes.constructorName

def Classes.constructorName (x : String) (k : Nat) : String

The name of a class’s k-th constructor’s function.

cpp.Classes.constructorTemplateName

def Classes.constructorTemplateName (x : String) (k : Nat) : String

The name of the function template the k-th constructor template of the class x is lowered to (C::C#c0; an instance is C::C#c0<int *>).

cpp.MemberInit.field

def MemberInit.field (mi : MemberInit) : String

The member the constructor’s initializer mi initializes (a data member, a base class, or the class itself when it delegates).

cpp.MemberInit.node

def MemberInit.node (mi : MemberInit) : NodeId

The node of the constructor’s initializer mi.

cpp.MemberInit.statement

def MemberInit.statement (mi : MemberInit) : Stmt

The constructor’s initializer mi as the statement initializing its member: sMInit with the arguments, sMInitList with a braced list’s items.

cpp.Classes.destructorName

def Classes.destructorName (x : String) : String

The name of a class’s destructor’s function.

cpp.Classes.named

def Classes.named (known : List ClassMembers) (t : TypeSyntax) : Option ClassMembers

The class a written type names, among the known ones; a const class is still that class ([basic.type.qualifier]p1), so a const object is constructed and destroyed as any other.

cpp.TypeSyntax.dimensions

def TypeSyntax.dimensions (t : TypeSyntax) : List Nat * TypeSyntax

The lengths of a written array type’s dimensions, outermost first, and its element type (no lengths for a type that is not an array).

cpp.Classes.elementCount

def Classes.elementCount (lengths : List Nat) : Nat

How many elements an array of the lengths has.

cpp.Classes.fieldClass

def Classes.fieldClass (known : List ClassMembers) (t : TypeSyntax) : Option ClassMembers

The class a written type is, or the class of its elements when it is an array (of arrays) of one.

cpp.TypeSyntax.isArray

def TypeSyntax.isArray (t : TypeSyntax) : Bool

Whether a written type is an array.

cpp.Classes.leafAt

def Classes.leafAt (n : NodeId) (array : Expr) (lengths : List Nat) (j : Expr) : Expr

The j-th element (row by row; j a surface expression) of an array of the given lengths: a[j / d1][j % d1].

cpp.Classes.leafLoop

def Classes.leafLoop (n : NodeId) (key : String) (count : Nat) (backward : Bool) (body : Expr -> Stmt) : Stmt

A loop over the indices of count elements (the first first, or the last first), with a statement for each.

cpp.DataMember

record DataMember

A data member: its name, written type and default member initializer.

cpp.Member.fields

def Member.fields (ms : List Member) : List DataMember

The data members of a class’s members, in order.

cpp.Classes.dynamicType

def Classes.dynamicType : String

The hidden member that keeps a polymorphic object’s dynamic type (cpp.polymorphism).

cpp.Member.isVirtual

def Member.isVirtual (m : Member) : Bool

Whether a member function is virtual as declared (virtual, override or pure).

cpp.Member.functionName

def Member.functionName (m : Member) : Option String

The name a member function declares, if the member is one.

cpp.Member.isHidden

def Member.isHidden (f : DataMember) : Bool

Whether a data member is one of a class’s hidden parts that a copy keeps its own of: the dynamic type, the pointers to its virtual bases, and their storage (a copy’s virtual bases are made by the complete object).

cpp.Member.copiedFields

def Member.copiedFields (ms : List Member) : List DataMember

The data members that are copied and assigned: all but the hidden ones (a copy keeps its own).

cpp.Classes.polymorphic

def Classes.polymorphic (known : List ClassMembers) (ms : List Member) : Bool

Whether a class (its members, with its bases as subobjects) is polymorphic: it declares a virtual function, or a base is polymorphic ([class.virtual]p1).

cpp.Classes.needsDefault

def Classes.needsDefault (known : List ClassMembers) (ms : List Member) : Bool

Whether a class needs a constructor it does not declare: a default member initializer, a member of a class with constructors ([class.default.ctor]p4), or a dynamic type to keep (a polymorphic class).

cpp.Classes.destroysMembers

def Classes.destroysMembers (known : List ClassMembers) (ms : List Member) : Bool

Whether a class has members to destroy: a member (or an array of them) of a class with a destructor.

cpp.DeclaredConstructor

record DeclaredConstructor

A constructor to lower: its access, node, parameters, member initializers and body.

cpp.Classes.names

def Classes.names (x : String) (t : TypeSyntax) : Bool

Whether a written type names a class (as a class or a struct).

cpp.Classes.isReferenceTo

def Classes.isReferenceTo (x : String) (t : TypeSyntax) : Bool

Whether a written type is a reference to a class, const or not.

cpp.Classes.allDefaulted

def Classes.allDefaulted (ps : List Param) : Bool

Whether the parameters ps all have defaults (the ones after a constructor’s first: it is then called with one argument, [dcl.fct.default]p1).

cpp.Classes.isCopyParameters

def Classes.isCopyParameters (x : String) (ps : List Param) : Bool

Whether a constructor’s parameters ps make it a copy constructor of the class x: a reference to the class, const or not, and any others with defaults ([class.copy.ctor]p1).

cpp.Classes.isRvalueReferenceTo

def Classes.isRvalueReferenceTo (x : String) (t : TypeSyntax) : Bool

Whether a written type is an rvalue reference to a class, const or not.

cpp.Classes.isMoveParameters

def Classes.isMoveParameters (x : String) (ps : List Param) : Bool

Whether a constructor’s parameters ps make it a move constructor of the class x: an rvalue reference to the class, and any others with defaults ([class.copy.ctor]p3).

cpp.Member.moveAssigns

def Member.moveAssigns (x : String) (m : Member) : Bool

Whether a member is a move assignment operator of class x: operator= taking an rvalue reference to a (const) x ([class.copy.assign]p3).

cpp.Classes.made

def Classes.made (n : NodeId) : NodeId

The node of the code the branch makes for a written node n (an implicit member’s body, the dynamic type set in a constructor): not one the program wrote, so the debugger does not stop at it, and a problem found in it is placed at n (Program.placedNode).

cpp.Member.isImplicit

def Member.isImplicit (n : NodeId) (m : Member) : Bool

Whether a member is one the class has implicitly: a member function carrying the class’s own node (the implicit assignment operators).

cpp.Classes.declaresMove

def Classes.declaresMove (x : String) (n : NodeId) (ms : List Member) : Bool

Whether class x (of node n) declares a move constructor or a move assignment operator.

cpp.Classes.declaresCopying

def Classes.declaresCopying (x : String) (n : NodeId) (ms : List Member) : Bool

Whether class x (of node n) declares a copy or move constructor, a copy or move assignment operator, or a destructor (with none of them it has an implicit move, [class.copy.ctor]p8, [class.copy.assign]p4).

cpp.Classes.movedFrom

def Classes.movedFrom (n : NodeId) (t : TypeSyntax) (e : Expr) : Expr

The value of a member (of a written type) to move from: an xvalue of it (static_cast<T &&>; an array’s elements are then xvalues too, [expr.sub]p2).

cpp.Classes.copiesMembers

def Classes.copiesMembers (known : List ClassMembers) (ms : List Member) : Bool

Whether copying a class’s members needs a constructor: a member (or an array of them) of a class with a copy constructor.

cpp.Classes.nothrowMembers

def Classes.nothrowMembers (known : List ClassMembers) (ms : List Member) : Bool

Whether moving (or copying) each member of a class (its base subobjects too) cannot throw: of a class that moves so, or not of a class (an implicit move or copy constructor is noexcept so, [except.spec]p8).

cpp.Classes.implicitCopy

def Classes.implicitCopy (known : List ClassMembers) (x : String) (n : NodeId) (ms : List Member) : List DeclaredConstructor

The implicit copy constructor, when the class declares none (nor a move, which deletes it) and copying its members needs one: each member initialized from the other object’s ([class.copy.ctor]p14).

cpp.Classes.implicitMove

def Classes.implicitMove (known : List ClassMembers) (x : String) (n : NodeId) (ms : List Member) : List DeclaredConstructor

The implicit move constructor, when the class declares no copy or move operation nor destructor and moving its members differs from copying them (a member, or a base subobject, of a class with a move constructor): each member initialized from the other object’s as an xvalue ([class.copy.ctor]p14).

cpp.Classes.lacksDefault

def Classes.lacksDefault (known : List ClassMembers) (ms : List Member) : Bool

Whether a data member (a base subobject too) without a default member initializer is of a class an object of which cannot be default-initialized: the implicit default constructor is then deleted ([class.default.ctor]p2.4).

cpp.Classes.declaredConstructors

def Classes.declaredConstructors (ms : List Member) : List DeclaredConstructor

The constructors a class declares, in order.

cpp.Classes.constructorTemplates

def Classes.constructorTemplates (ms : List Member) : List (List TemplateParam * DeclaredConstructor)

The constructor templates among a class’s members ms, in order, each with its template parameters ([temp.mem]p1).

cpp.Classes.declaresConstructor

def Classes.declaresConstructor (ms : List Member) : Bool

Whether a class with the members ms declares a constructor (a constructor template is one: with it, the class has no implicit default constructor, [class.default.ctor]p1).

cpp.Classes.defaultConstructibleOf

def Classes.defaultConstructibleOf (known : List ClassMembers) (ms : List Member) : Bool

Whether an object of a class with the members ms (given the classes known before it) can be default-initialized: without declared constructors, unless its implicit default constructor is deleted; else by a constructor callable without arguments (each parameter has a default; a constructor template is not, its parameters deduced from arguments).

cpp.Classes.constructorsIn

def Classes.constructorsIn (known : List ClassMembers) (x : String) (n : NodeId) (ms : List Member) : List DeclaredConstructor

The constructors of the class x (of node n, with the members ms, given the classes known before it) in order: the declared ones (else the implicit default one, if it needs one and is not deleted, [class.default.ctor]p1: a declared constructor or constructor template suppresses it), then the implicit copy constructor, if it has one.

cpp.Classes.requiredOf

def Classes.requiredOf (ps : List Param) : Nat

How many of the parameters ps have no default argument: the fewest arguments a call passes.

cpp.Classes.constructorEntry

def Classes.constructorEntry (x : String) (declared : Nat) (p : Nat * DeclaredConstructor) : Constructor

The k-th constructor’s entry in its class’s table (implicit past the declared ones).

cpp.Classes.constructorTemplateEntry

def Classes.constructorTemplateEntry (x : String) (p : Nat * (List TemplateParam * DeclaredConstructor)) : Constructor

The entry of a constructor template p (numbered k: its position, its template parameters and the constructor) in the table of its class x: the function template it is lowered to.

cpp.Classes.constructorsOf

def Classes.constructorsOf (known : List ClassMembers) (x : String) (n : NodeId) (ms : List Member) : List Constructor

A class’s constructors for its table: the function each is lowered to, its arity and access; then its constructor templates.

cpp.Classes.copyConstructorOf

def Classes.copyConstructorOf (known : List ClassMembers) (x : String) (n : NodeId) (ms : List Member) : Option String

A class’s copy constructor’s function, if it has one.

cpp.Classes.nothrowMoveOf

def Classes.nothrowMoveOf (known : List ClassMembers) (x : String) (n : NodeId) (ms : List Member) : Bool

Whether moving an object of a class cannot throw (std::is_nothrow_move_constructible, what libc++’s move_if_noexcept asks): its move constructor is noexcept; without one, its copy constructor is, or it has none (copied bit for bit).

cpp.Classes.moveConstructorOf

def Classes.moveConstructorOf (known : List ClassMembers) (x : String) (n : NodeId) (ms : List Member) : Option String

A class’s move constructor’s function, if it has one.

cpp.Classes.destroyedOf

def Classes.destroyedOf (known : List ClassMembers) (ms : List Member) : Bool

Whether a class has a destructor to run: declared, or for its members.

cpp.ClassMembers.assigns

def ClassMembers.assigns (c : ClassMembers) : Bool

Whether a class has a copy assignment operator (declared or implicit).

cpp.Classes.assignmentDeleted

def Classes.assignmentDeleted (known : List ClassMembers) (ms : List Member) : Bool

Whether a class’s implicit copy and move assignment operators are deleted ([class.copy.assign]p7): a data member (or an array’s elements) is const or a reference, or is of a class (a base subobject included) whose are.

cpp.Member.copyAssigns

def Member.copyAssigns (x : String) (m : Member) : Bool

Whether a member is a copy assignment operator of class x: operator= taking an x or a reference to a (const) x ([class.copy.assign]p1).

cpp.Classes.implicitAssignment

def Classes.implicitAssignment (known : List ClassMembers) (x : String) (n : NodeId) (ms : List Member) : List Member

The implicit copy assignment operator, when the class declares no copy assignment (nor a move, which deletes it) and assigning its members needs one, or it declares another operator= (both are then chosen between, [class.copy.assign]p2): each member assigned from the other object’s (an array element by element), then *this returned ([class.copy.assign]p12).

cpp.Classes.implicitMoveAssignment

def Classes.implicitMoveAssignment (known : List ClassMembers) (x : String) (n : NodeId) (ms : List Member) : List Member

The implicit move assignment operator, when the class declares no copy or move operation nor destructor and a member (or a base subobject) is of a class with a move assignment operator: each member assigned from the other object’s as an xvalue (an array element by element), then *this returned ([class.copy.assign]p12).

cpp.Classes.baseField

def Classes.baseField (k : Nat) : String

The name of a class’s k-th base class subobject, a member of its struct.

cpp.Classes.constructionField

def Classes.constructionField : String

The member of a class that keeps virtual bases holding, while a base subobject of it is constructed or destroyed, the number of its first construction context in the complete object (Polymorphism.block).

cpp.Classes.virtualPointer

def Classes.virtualPointer (y : String) : String

The name of the member pointing to a direct virtual base’s subobject (the complete object’s).

cpp.Classes.virtualStorage

def Classes.virtualStorage (y : String) : String

The name of the member a complete object keeps a virtual base’s subobject in.

cpp.Classes.distinct

def Classes.distinct (xs : List String) : List String

The names in order, each once (its first).

cpp.Classes.virtualBasesOf

def Classes.virtualBasesOf (known : List ClassMembers) (bs : List Base) : List String

The virtual bases of a hierarchy with direct bases, in the order a complete object constructs them: depth first, left to right, a base’s own virtual bases before it, each once ([class.base.init]p13).

cpp.Classes.baseMembers

def Classes.baseMembers (bs : List Base) : List Member

A class’s direct bases as its first data members, in declaration order (the Itanium C++ ABI’s layout): a non-virtual one as its subobject (constructed first and destroyed last, copied and assigned like a member), a virtual one as a pointer to the complete object’s subobject of it.

cpp.Classes.baseNamed

def Classes.baseNamed (bs : List Base) (vs : List String) (y : String) : Option String

The base subobject a name in a member initializer list names, if it is a direct base class’s or a virtual base’s of the hierarchy (vs; a virtual base’s is the complete object’s storage of it, [class.base.init]p2).

cpp.Classes.baseInits

def Classes.baseInits (bs : List Base) (vs : List String) (inits : List MemberInit) : List MemberInit

A constructor’s member initializers inits with a base class’s name replaced by its subobject’s (Classes.baseNamed, with the direct bases bs and the hierarchy’s virtual bases vs).

cpp.Member.withBaseInits

def Member.withBaseInits (bs : List Base) (vs : List String) (m : Member) : Member

A constructor’s member initializers with a base class’s name replaced by its subobject’s.

cpp.ClassDefinition.completed

def ClassDefinition.completed (known : List ClassMembers) (d : ClassDefinition) : ClassDefinition

A class’s definition with its bases as subobjects and the members it has implicitly (the copy and move assignment operators).

cpp.Classes.listOf

def Classes.listOf {A : Type} (o : Option A) : List A

The element of an option as a list (empty or one).

cpp.Base.table

def Base.table (known : List ClassMembers) (b : Base) : Option ClassMembers

The table entry of a direct base, if its class is known.

cpp.Classes.aliases

def Classes.aliases (items : List Item) : List (String * TypeSyntax)

The program’s typedefs, by name (a typedef name is a synonym of its type, [dcl.typedef]p1).

cpp.Classes.aliased

def Classes.aliased (aliases : List (String * TypeSyntax)) (x : String) : Option TypeSyntax

The type a typedef name stands for, if it is one.

cpp.Classes.typeKey

def Classes.typeKey (aliases : List (String * TypeSyntax)) (fuel : Nat) (t : TypeSyntax) : String

A written type as a string, the same for the same type: typedef names expanded (fuel bounds their chains).

cpp.Classes.functionKey

def Classes.functionKey (aliases : List (String * TypeSyntax)) (name : String) (isConst : Bool) (ps : List Param) : String

A member function’s identity for overriding ([class.virtual]p2: the name, the parameter-type-list and the cv-qualification), as f#(i,PKc)K: its name, its parameters’ types after this (typedefs expanded) and K when it is const. A class in a namespace is written with ., so the identity has no :: and reads as a member’s name.

cpp.Member.key

def Member.key (aliases : List (String * TypeSyntax)) (m : Member) : Option String

A member function’s identity for overriding (a destructor’s is ~), if the member is a function.

cpp.Classes.overloadNames

def Classes.overloadNames (ms : List Member) : List Member

A class’s member functions with those declared more than once named f#k (the k-th of the name), or a member function template’s name too ([temp.over]: the template’s instance is chosen among them, as for free functions), the others as they are.

cpp.Classes.among

def Classes.among (names : List String) (f : String) : Bool

Whether a name is among names.

cpp.Classes.functionsWhere

def Classes.functionsWhere (test : Member -> Bool) (ms : List Member) : List String

The names of the member functions among members that satisfy a test.

cpp.Member.isPure

def Member.isPure (m : Member) : Bool

Whether a member function is pure virtual.

cpp.Classes.keysWhere

def Classes.keysWhere (aliases : List (String * TypeSyntax)) (test : Member -> Bool) (ms : List Member) : List String

The identities (Classes.functionKey) of the member functions among members that satisfy a test.

cpp.Classes.virtualsOf

def Classes.virtualsOf (known : List ClassMembers) (aliases : List (String * TypeSyntax)) (bs : List Base) (ms : List Member) : List String

A class’s virtual functions, by identity: the ones it declares virtual and the ones its bases have (a function of the same name and parameters in it overrides, and is virtual too, [class.virtual]p2).

cpp.Classes.pureOf

def Classes.pureOf (known : List ClassMembers) (aliases : List (String * TypeSyntax)) (bs : List Base) (ms : List Member) : List String

A class’s pure virtual functions it does not override, by identity: its own pure ones and its bases’ it declares no overrider for (a class with any is abstract, [class.abstract]p2).

cpp.Base.entry

def Base.entry (b : Base) : ClassBase

A direct base’s entry in its class’s table.

cpp.Classes.functionKeysOf

def Classes.functionKeysOf (aliases : List (String * TypeSyntax)) (ms : List Member) : List (String * String)

A class’s member functions by the name each is lowered to (after C::, Classes.overloadNames) and identity.

cpp.ClassMembers.entry

def ClassMembers.entry (known : List ClassMembers) (aliases : List (String * TypeSyntax)) (d : ClassDefinition) : ClassMembers

A class’s entry, given the classes before it and the program’s typedefs.

cpp.Classes.staticsOf

def Classes.staticsOf (x : String) (ms : List Member) : List StaticMember

A class’s static members: a data member as its global’s declaration, a member function as x::f.

cpp.Classes.isLibrary

def Classes.isLibrary (known : List ClassMembers) (x : String) : Bool

Whether a class is the library’s (ClassMembers.library).

cpp.ClassMembers.of

def ClassMembers.of (items : List Item) : List ClassMembers

The classes of the items, each given the ones before it.

cpp.Classes.thisParameter

def Classes.thisParameter (x : String) (isConst : Bool) : Param

A member function’s this: a pointer to the class, to const for a const member function.

cpp.Classes.selfMember

def Classes.selfMember (n : NodeId) (x : String) : Expr

A member used alone in a member function: this->x.

cpp.Classes.method

def Classes.method (x : String) (isConst : Bool) (f : FunctionDefinition) : FunctionDefinition

A member function as a function: named C::f, with this first.

cpp.Classes.pureCall

def Classes.pureCall : String

The internal function a pure virtual function’s body calls: calling it is undefined behavior.

cpp.Member.lowered

def Member.lowered (x : String) (isConst : Bool) (virt : Virtuality) (f : FunctionDefinition) : FunctionDefinition

A member function lowered: a pure virtual one’s body is a call of the pure call (it is called only through the dynamic type during construction or destruction, [class.abstract]p6). The body is the branch’s, on a node of its own, so the problem is reported at the call the program made.

cpp.Member.asTemplate

def Member.asTemplate (x : String) (m : Member) : List Item

A member function template of class x as the function template it is lowered to: x::f with this first ([temp.mem]p1); nothing for any other member.

cpp.Classes.memberTemplates

def Classes.memberTemplates (items : List Item) : List Item

The member function templates of the items’ classes, as the function templates they are lowered to (where a call’s instance is made from).

cpp.Classes.fieldInit

def Classes.fieldInit (known : List ClassMembers) (n : NodeId) (inits : List MemberInit) (f : DataMember) : CheckResult Cpp.constructs (List Stmt)

A data member’s initialization in a constructor ([class.base.init]): by the initializer the constructor gives, else by its default member initializer ([class.base.init]p9), else a member of a class with constructors is constructed without arguments (sMInit) and any other left uninitialized (sMInit without arguments when its class has a destructor, so it is guarded). An initialization is no assignment: a const member can be.

cpp.Classes.fieldInits

def Classes.fieldInits (known : List ClassMembers) (sets : List Stmt) (prelude : List Stmt) (complete : Bool) (n : NodeId) (ms : List Member) (inits : List MemberInit) : CheckResult Cpp.constructs (List Stmt)

The members’ initializations in a constructor, in declaration order ([class.base.init]p13); an initializer for something that is not a data member is an error.

cpp.Handler.rethrowing

def Handler.rethrowing (h : Handler) : Handler

A handler of a constructor’s function try block: at its end the exception is thrown again ([except.handle]p15).

cpp.Classes.constructorBody

def Classes.constructorBody (n : NodeId) (initializing : List Stmt) (body : Stmt) : Stmt

A constructor’s body after its members’ initializations: with a function try block, the initializations are in its try (its handlers catch what they throw, after the constructed members are destroyed, and throw it again).

cpp.Classes.baseVariant

def Classes.baseVariant (name : String) : String

The name of the variant of a constructor or destructor for a base subobject (the Itanium C++ ABI’s base object constructor and destructor): it leaves the virtual bases to the complete object.

cpp.Member.keepsVirtualBases

def Member.keepsVirtualBases (ms : List Member) : Bool

Whether a class’s members (completed) keep virtual bases.

cpp.Variant

record Variant

What a variant of a constructor or destructor sets first: the dynamic type, and the prelude (for a complete object the pointers to its virtual bases and the construction contexts of its bases; for a base subobject those of its bases).

cpp.Classes.delegatedBody

def Classes.delegatedBody (known : List ClassMembers) (x : String) (ms : List Member) (n : NodeId) (m : NodeId) (args : List Expr) (body : Stmt) : CheckResult Cpp.constructs Stmt

A delegating constructor’s body ([class.base.init]p6): the object made by the constructor the arguments choose (#construct(this, args), the internal function placement new lowers to, Construction.constructAt), then the body; the object is complete before the body, so an exception from it destroys the object and goes on ([except.ctor]p4, as catch (...) destroying it and throwing again).

cpp.Classes.constructorNamed

def Classes.constructorNamed (known : List ClassMembers) (v : Variant) (x : String) (ms : List Member) (complete : String) (n : NodeId) (ps : List Param) (inits : List MemberInit) (body : Stmt) : CheckResult Cpp.constructs Item

Classes.constructor (the classes known before the class x, the variant v, the members ms; the constructor’s node n, parameters ps, initializers inits and body) as the function named complete (for a complete object; its variant for a base subobject is complete:base).

cpp.Classes.constructor

def Classes.constructor (known : List ClassMembers) (v : Variant) (x : String) (ms : List Member) (k : Nat) (n : NodeId) (ps : List Param) (inits : List MemberInit) (body : Stmt) : CheckResult Cpp.constructs Item

A constructor as a function C::C#k with this first: for a complete object, the prelude and the virtual bases constructed; the bases constructed, the dynamic type set (sets), the members initialized, then the body ([class.base.init]p13, [class.cdtor]p4). The variant for a base subobject is C::C#k:base. A delegating one (its only initializer names its own class) is Classes.delegatedBody.

cpp.Classes.constructors

def Classes.constructors (known : List ClassMembers) (whole : Variant) (part : Variant) (x : String) (n : NodeId) (ms : List Member) : CheckResult Cpp.constructs (List Item)

A class’s constructors as functions, numbered as in its table; with virtual bases, each also for a base subobject.

cpp.Classes.constructorTemplateItems

def Classes.constructorTemplateItems (known : List ClassMembers) (whole : Variant) (x : String) (ms : List Member) : CheckResult Cpp.constructs (List Item)

The constructor templates among the members ms of the class x (given the classes known before it) as function templates C::C#ck (Classes.constructorTemplateName), each lowered as a constructor is (Classes.constructorNamed, the variant whole for a complete object), with its template parameters ([temp.mem]p1). A class with virtual bases would need each instance’s variant for a base subobject too: not done.

cpp.Classes.writableMember

def Classes.writableMember (n : NodeId) (written : TypeSyntax) (object : Expr) : Expr

A member (or an element of a member array) of a written type as an object under construction or destruction: a const one through const_cast, since const does not apply then ([class.ctor]p5, [class.dtor]p2).

cpp.Classes.memberDestructions

def Classes.memberDestructions (known : List ClassMembers) (n : NodeId) (fs : List DataMember) : List Stmt

The destructions of a class’s members of classes with destructors, in reverse declaration order (an array’s elements the last first, [class.dtor]p13); a base subobject or a virtual base by its class’s variant for one.

cpp.Classes.destructor

def Classes.destructor (known : List ClassMembers) (sets : List Stmt) (partSets : List Stmt) (x : String) (n : NodeId) (ms : List Member) : List Item

A class’s destructor as functions: the declared body as C::~C#body (a return in it leaves only the body), then C::~C runs it and destroys the members, then the virtual bases (a complete object’s, the last); an implicit one only destroys them. With virtual bases, C::~C:base too, for a base subobject: without the virtual bases. All are noexcept (a destructor is, unless declared otherwise, [except.spec]p8): an exception leaving them terminates the run.

cpp.Classes.dynamicTypeSets

def Classes.dynamicTypeSets (known : List ClassMembers) (self : ClassMembers) (n : NodeId) : List Stmt

The dynamic type set in a constructor or destructor of a class (given the classes before it, and its own entry): each of its chains’ #vt the number of its context ([class.cdtor]p4: during construction and destruction the object is of this class).

cpp.Classes.partTypeSets

def Classes.partTypeSets (known : List ClassMembers) (self : ClassMembers) (n : NodeId) : List Stmt

The dynamic type set in a constructor or destructor of a class for a base subobject: its chains in its virtual bases hold its construction contexts (this->#vtt and on), the others as in a complete object’s.

cpp.Classes.rootContexts

def Classes.rootContexts (known : List ClassMembers) (self : ClassMembers) (n : NodeId) : List Stmt

What a complete object’s constructor sets before its bases are constructed: each construction root’s #vtt, the number of its block’s first context.

cpp.Classes.baseContexts

def Classes.baseContexts (all : List ClassMembers) (self : ClassMembers) (n : NodeId) : List Stmt

What a base subobject’s constructor sets before its bases are constructed: each non-virtual base’s that keeps virtual bases #vtt, where its block is in this one’s.

cpp.Classes.staticItems

def Classes.staticItems (x : String) (ms : List Member) : List Item

A class’s static members as the program’s: a data member a global (its uses are already of its declaration), a member function the function x::f without this ([class.static.mfct]).

cpp.ClassDefinition.lowered

def ClassDefinition.lowered (known : List ClassMembers) (aliases : List (String * TypeSyntax)) (d : ClassDefinition) : CheckResult Cpp.constructs (List Item)

A class lowered, given the classes before it: its member types as typedefs C::name, the class kept (for the table), its data members as a struct, its member functions, constructors and destructor as functions.

cpp.Classes.parts

def Classes.parts (all : List ClassMembers) (self : ClassMembers) (n : NodeId) : List (ClassMembers * Expr)

A complete object’s subobjects (*this, given the classes so far and its class): its own and its non-virtual bases’, then each virtual base’s (in the complete object’s storage) and its non-virtual bases’; a virtual base is one subobject however many paths reach it.

cpp.Classes.pointing

def Classes.pointing (all : List ClassMembers) (self : ClassMembers) (n : NodeId) : List Stmt

What a complete object’s constructor does first: point every subobject’s pointer to a direct virtual base at the complete object’s storage of it.

cpp.Classes.lowerAll

def Classes.lowerAll (known : List ClassMembers) (aliases : List (String * TypeSyntax)) (items : List Item) : CheckResult Cpp.constructs (List Item)

The items with their classes lowered (each given the ones before it and the program’s typedefs), or where one is not lowered by this step.

cpp.Item.asClass

def Item.asClass (it : Item) : Item

A struct item as the class it is in C++ ([class]p4: a struct is a class whose members are public by default), so that its members are constructed and destroyed like a class’s.

cpp.Classes.loweredFunction

def Classes.loweredFunction (items : List Item) (name : String) : Option FunctionDefinition

A lowered function by name, among the items.

cpp.Classes.keyed

def Classes.keyed (all : List ClassMembers) (y : String) (key : String) : Option String

The name of a class’s member function with an identity (after C::), if the class declares one.

cpp.Classes.keyName

def Classes.keyName (key : String) : String

The name in a member function’s identity (what comes before #().

cpp.Classes.declaresOverrider

def Classes.declaresOverrider (all : List ClassMembers) (y : String) (key : String) : Bool

Whether a class declares a function overriding one: a member function with its identity.

cpp.Classes.overrider

def Classes.overrider (all : List ClassMembers) (x : String) (path : List Nat) (f : String) : Option (String * Nat)

The class that overrides a virtual function for a subobject of a class at a path: going down the path from the complete object’s class, the first that declares the function, and how many levels up from the subobject it is (in a hierarchy without virtual bases the final overrider is on that path, [class.virtual]p2).

cpp.Classes.baseOverrider

def Classes.baseOverrider (all : List ClassMembers) (c : String) (path : List Nat) (f : String) : Option (String * List Nat)

The class that overrides a virtual function in a class’s bases when no class from the complete object down to it does: along the path to the base whose function the call finds, the first that declares it, and the path to it.

cpp.Classes.containingCall

def Classes.containingCall (x : String) : String

The name of the internal call #containing:X(p, k): the complete object of class X containing what p points to, k levels up (how a dispatcher reaches the complete object from a subobject in a virtual base, which no cast may).

cpp.Classes.finalOverrider

def Classes.finalOverrider (all : List ClassMembers) (x : String) (owner : List Nat) (f : String) : Option (String * List Nat)

The overrider of a virtual function for a subobject of a complete object with virtual bases ([class.virtual]p2): along every path from the complete object’s class to the subobject the call finds the function in, the first class that declares it, then the one of those that dominates (derives from) the others; and the path to it.

cpp.Classes.keepsVirtualBases

def Classes.keepsVirtualBases (all : List ClassMembers) (x : String) : Bool

Whether a class keeps virtual bases.

cpp.Classes.dispatcherName

def Classes.dispatcherName (c : String) (f : String) : String

The name of the function that dispatches a class’s virtual function.

cpp.Dispatch

record Dispatch

What a dispatcher’s cases are written with: the class and the function’s identity (Classes.functionKey), the path to the base whose function the call finds, the path to the root of the chain, the arguments after this, the result type, and the node.

cpp.Classes.dispatchCase

def Classes.dispatchCase (all : List ClassMembers) (dp : Dispatch) (ctx : Nat * (String * List Nat)) : List Clause

A dispatcher’s case for a context (its number, its complete object’s class and the path to its chain): when the class is on the chain at that context, the call of the overrider, with this converted up to it (or to its subobject, when it is one of the class’s bases).

cpp.Classes.dispatchConstruction

def Classes.dispatchConstruction (all : List ClassMembers) (dp : Dispatch) (ctx : ConstructionContext) : List Clause

A dispatcher’s case for a construction context (its number, the complete object’s class, the path to the base subobject being constructed or destroyed and the path to its chain): when the class is on the chain, the call of the final overrider in the hierarchy of that base subobject’s class (its dynamic type then, [class.cdtor]p4), on the subobject the complete object has of it.

cpp.Classes.dispatcher

def Classes.dispatcher (all : List ClassMembers) (contexts : Contexts) (items : List Item) (c : String) (key : String) : Option Item

The dispatch of a polymorphic class’s virtual function (by its identity, Classes.functionKey): C::f#(...)#virtual(this, args) reads the dynamic type of the chain this is on and calls the overrider for that context. The class whose function a call finds by the name ([class.member.lookup]) must declare one with that identity, or bring one in with a using-declaration (Classes.declaring); when it only hides it, there is no call to dispatch.

cpp.Classes.deleter

def Classes.deleter (all : List ClassMembers) (contexts : Contexts) (c : String) : Option Item

The dispatch of a class’s virtual destructor for delete: C::~#virtual(this) destroys the complete object (its class’s destructor, on this converted up to it) and releases its block, for the context the dynamic type names.

cpp.Classes.dispatchers

def Classes.dispatchers (all : List ClassMembers) (items : List Item) : List Item

The dispatch functions of every polymorphic class’s virtual functions (a virtual destructor’s for delete).

cpp.Classes.prepare

def Classes.prepare (p : Program) : CheckResult Cpp.constructs (List Item)

The program’s items with the classes (and structs) lowered, and the virtual functions’ dispatch functions.

cpp.Classes.current

def Classes.current (g : Globals Cpp.constructs) : String

The class the function being checked is a member function of (empty outside one): the longest class name the function’s name starts with (a generated class’s name has :: in it, std::vector<int>), else what comes before its last ::.

cpp.ClassMembers.member

def ClassMembers.member (cs : List ClassMembers) (x : String) (f : String) : Option ClassMember

A class’s member by name.

cpp.ClassMembers.named

def ClassMembers.named (known : List ClassMembers) (x : String) : Option ClassMembers

The class with a name, among the known ones.

cpp.Lookup

data Lookup

Where name lookup finds a member of a class ([class.member.lookup]): in the class itself or a base, by the path of base subobjects (their positions), with the class that declares it and the inheritance links on the way; or in two bases (ambiguous); or nowhere.

cpp.Lookup.through

def Lookup.through (k : Nat) (from : String) (acc : Access) (r : Lookup) : Lookup

A found member reached through one more base: the base’s position and the link from the class to it.

cpp.Classes.lookupWithin

def Classes.lookupWithin (fuel : Nat) (known : List ClassMembers) (x : String) (f : String) : Lookup

The member of a class named f: its own (which hides the bases’), else the one the bases have, ambiguous when more than one base does; fuel bounds the depth (the classes before it, as the hierarchy has no cycle).

cpp.Classes.lookup

def Classes.lookup (known : List ClassMembers) (x : String) (f : String) : Lookup

The member of a class named f, by name lookup.

cpp.Classes.usingsChecked

def Classes.usingsChecked (all : List ClassMembers) (x : String) (n : NodeId) (ms : List Member) : CheckResult Cpp.constructs Unit

A class’s using-declarations checked ([namespace.udecl]): each names a base of the class and member functions of it the class may use (a private one may not be named, p19); one naming a data member is not provided.

cpp.Classes.importOf

def Classes.importOf (all : List ClassMembers) (x : String) (f : String) : Option String

The base a class brings a name in from with a using-declaration, if it does.

cpp.Classes.pathTo

def Classes.pathTo (all : List ClassMembers) (x : String) (y : String) : List Nat

The path of base positions from a class to one of its bases (the first, when there are more).

cpp.Classes.ofLowered

def Classes.ofLowered (all : List ClassMembers) (lowered : String) : Option (String * String)

The class a lowered member function (C::f#k) is of, and its identity there.

cpp.Classes.declaringWithin

def Classes.declaringWithin (fuel : Nat) (all : List ClassMembers) (c : String) (key : String) : Option (List Nat * String)

The class declaring the member function with an identity that a call on a class finds by its name, and the path to it: the class the name’s lookup finds, or, when that class brings the name in with a using-declaration, the one the base’s lookup finds (fuel bounds the chain).

cpp.Classes.declaring

def Classes.declaring (all : List ClassMembers) (c : String) (key : String) : Option (List Nat * String)

The class declaring the member function with an identity that a call on a class finds, and the path to it.

cpp.Classes.importedWithin

def Classes.importedWithin (fuel : Nat) (g : Globals Cpp.constructs) (x : String) (f : String) (own : List String) : List String

The functions a using-declaration in a class brings in for a name: the base’s (as a call on it finds them, through its own using-declarations too), without those the class declares with the same identity (they override or hide them, [namespace.udecl]p14).

cpp.Classes.functionsNamed

def Classes.functionsNamed (g : Globals Cpp.constructs) (name : String) : List String

The functions a member function’s name is lowered to: C::f alone, or its overloads C::f#k.

cpp.Classes.derivesFrom

def Classes.derivesFrom (known : List ClassMembers) (x : String) (y : String) : Bool

Whether a class is derived from another, directly or not (or is it).

cpp.Classes.reachesWithin

def Classes.reachesWithin (fuel : Nat) (known : List ClassMembers) (x : String) (y : String) : Bool

Whether a class reaches another through its bases, within fuel steps.

cpp.Access.word

def Access.word (acc : Access) : String

The word for an access in the error.

cpp.Classes.befriends

def Classes.befriends (g : Globals Cpp.constructs) (owner : String) : Bool

Whether the function being checked is a friend of a class ([class.friend]p2): a function it names, or a member function of a class it names.

cpp.Classes.allows

def Classes.allows (g : Globals Cpp.constructs) (owner : String) (acc : Access) : Bool

Whether a member with an access in its class may be used in the function being checked ([class.access]p1): a public one anywhere, a protected one in the class and the classes derived from it, a private one in the class; a private or protected one also in the class’s friends.

cpp.Classes.denied

def Classes.denied (g : Globals Cpp.constructs) (x : String) (f : String) : Option String

Why a member of a class cannot be used here: it is private or protected and this function may not use it, or it is reached through a base inherited privately or protectedly, outside the class that inherits it ([class.access.base]).

cpp.Classes.member

def Classes.member (g : Globals Cpp.constructs) (n : NodeId) (f : String) (l : Lifted Cpp.constructs) : Option (CheckResult Cpp.constructs (Lifted Cpp.constructs))

A member’s access checked: none leaves the member to the core, else the error.

cpp.Classes.subobject

def Classes.subobject (all : List ClassMembers) (x : String) (n : NodeId) (object : Expr) (arrow : Bool) (path : List Nat) : Expr

An object’s base subobject along a path of base positions from its class: obj.#base0.#base1… for non-virtual bases, *obj.#vbp:V through a virtual one (through p-> first when the object is reached through a pointer).

cpp.Classes.objectClass

def Classes.objectClass (arrow : Bool) (l : Lifted Cpp.constructs) : Ty Cpp.constructs

The class an object designates, from its checked form: through the pointer for p->.

cpp.Picking

def Picking : Type

How a call chooses among overloaded functions (cpp.overloading): given the call’s node, the name as written, the candidates, whether the object is const, and the arguments, the chosen function.

cpp.Classes.isNumbered

def Classes.isNumbered (name : String) (lowered : String) : Bool

Whether a lowered name is one of a name’s overloads, f#k (not a function made for it, f#(i)#virtual).

cpp.Classes.overloadOf

def Classes.overloadOf (lowered : String) : Option String

The name an overload is of (f for f#k, C::f for C::f#k), if it is one.

cpp.Classes.overloadTable

def Classes.overloadTable (names : List String) : List (String * List String)

The program’s overloaded functions, each name with its overloads in order (f with f#0, f#1…): looked up by the name, so a call does not compare its name with every function’s.

cpp.Classes.overloadsOf

def Classes.overloadsOf (g : Globals Cpp.constructs) (name : String) : List String

The functions a name is lowered to when it is overloaded: f#k, C::f#k (none when it is not).

cpp.Classes.virtualKeyOf

def Classes.virtualKeyOf (all : List ClassMembers) (x : String) (chosen : String) : Option String

The identity of the member function a call chose (C::f#k), when it is virtual in the object’s class: the call then goes through the class’s dispatcher.

cpp.Classes.receiverNode

def Classes.receiverNode (n : NodeId) : NodeId

The node of the object’s address a member function’s call passes (n:this): a node of its own, so the call’s node n has only the call’s type (problems at it are placed at n, Program.placedNode).

cpp.Classes.isConstMember

def Classes.isConstMember (sg : Signature Cpp.constructs) : Bool

Whether the member function of the signature sg is const: its this points to a const object.

cpp.Classes.memberCall

def Classes.memberCall (pick : Picking) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (object : Expr) (arrow : Bool) (f : String) (args : List Expr) (l : Lifted Cpp.constructs) : CheckResult Cpp.constructs Expr

obj.f(args) or p->f(args) as the call C::f(&obj, args) or C::f(p, args), once the object’s class is known (from its checked form): the member function must exist (chosen among its overloads, with those a using-declaration brings in) and be accessible, and a const object needs a const member function. The object is passed as the subobject of the class the chosen function is of.

cpp.Classes.templateCall

def Classes.templateCall (g : Globals Cpp.constructs) (n : NodeId) (object : Expr) (arrow : Bool) (f : String) (targs : List TypeSyntax) (args : List Expr) (l : Lifted Cpp.constructs) : CheckResult Cpp.constructs Expr

obj.f<T...>(args) or p->f<T...>(args) ([temp.arg.explicit]): only a member function template of the name is called, as C::f<T...>(&obj, args) once the object’s class is known (the object passed as the subobject of the class declaring it, its access checked first); the explicit arguments are the template’s first ones, the rest deduced.

cpp.Classes.templateCallOf

def Classes.templateCallOf (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (object : Expr) (arrow : Bool) (f : String) (targs : List TypeSyntax) (args : List Expr) : CheckResult Cpp.constructs Expr

A member function template’s call with explicit arguments as the call it is (its object checked first).

cpp.Classes.arrowOperand

def Classes.arrowOperand (g : Globals Cpp.constructs) (n : NodeId) (object : Expr) (l : Lifted Cpp.constructs) : Option Expr

What a-> applies to when a (checked) is an object of a class, not a pointer: a.operator->(), the result of which -> applies to in turn ([over.ref]p1: an iterator’s it->first); none when a is a pointer or its class (and its bases) declare no operator->.

cpp.Classes.standardStream

def Classes.standardStream (object : Expr) : Option String

The standard stream a member function’s call’s object is (std::cout, std::cerr, std::cin), if it is one: the console’s stream (eStdout, as the C family and a front end that resolves its names write it) or its name (eConst "cout", with or without std::).

cpp.Classes.streamMember

def Classes.streamMember {A : Type} (n : NodeId) (stream : String) (f : String) : CheckResult Cpp.constructs A

A member f of the standard stream stream called at the node n: the model has its operators (cout << x, cin >> x), not yet its member functions, so the program is unknown, not wrong.

cpp.Kept

record Kept

An operand evaluated before what comes after it, kept so that nothing after it changes it: its statements and accesses, the scope that names what keeps it, and the expression standing for it (written where the operand was).

cpp.Kept.Checked

def Kept.Checked : Type

What checking an expression gives: its lifted form, or why it is not checked.

cpp.Kept.none

def Kept.none (env : Env Cpp.constructs) (e : Expr) : Kept

The expression e as written, nothing kept, in the scope env.

cpp.Kept.with

def Kept.with (k : Kept) (e : Expr) : Kept

The kept operand k with the expression e standing in its scope (the call it is an operand of).

cpp.Kept.lifted

def Kept.lifted (k : Kept) (r : Lifted Cpp.constructs) : Lifted Cpp.constructs

What the expression of k, checked as r, needs: the kept operand’s statements first, then its own; both accesses.

cpp.Kept.checkWith

def Kept.checkWith (check : Env Cpp.constructs -> Expr -> Kept.Checked) (k : Kept) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

The expression of k checked by check (as a value or an lvalue) in the scope of k, the kept operand’s statements first.

cpp.Kept.statement

def Kept.statement (n : NodeId) (k : Kept) (s : TypedStmt Cpp.constructs) : TypedStmt Cpp.constructs

The statement of the expression of k, checked as s at the node n: the kept operand’s statements first.

cpp.Classes.kept

def Classes.kept (p : Platform) (env : Env Cpp.constructs) (n : NodeId) (arrow : Bool) (l : Lifted Cpp.constructs) : Option Kept

The operand checked as l (on the platform p, in the scope env) kept at the node n ([expr.call]p8, [over.match.oper]p2: what comes after it is sequenced after it): a temporary it already is (a call’s result), named in the scope; else, as the pointer a member function is called through (arrow) or a value not of a class, its value in a temporary of its own; else, as an lvalue, its address in one (the operand is that lvalue again, *p, an lvalue of the same type). None for a value of a class that is not in a temporary (an xvalue): it is not kept.

cpp.Classes.isOperatorName

def Classes.isOperatorName (f : String) : Bool

Whether a member function’s name f is an operator’s (operator+, operator[], operator int), not a name that only begins so (operatorCount).

cpp.Classes.objectFirst

def Classes.objectFirst (f : String) : Bool

Whether a call of the member function f evaluates its object before its arguments: a call is so ([expr.call]p8), and an operator written as one whose built-in left operand goes first is too (<<, >> [expr.shift]p4; [] [expr.sub]p1; ->* [expr.mptr.oper]p4; &&, ||, ,; a call (); [over.match.oper]p2). Any other operator is not taken to: its built-in operands are unsequenced (+, ==), or the right goes first (=, +=, which cpp.copies keeps first); an explicit call of one (a.operator+(b)) is then taken as unsequenced.

cpp.Classes.callOf

def Classes.callOf (pick : Picking) (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (object : Expr) (arrow : Bool) (f : String) (args : List Expr) : CheckResult Cpp.constructs Kept

The call at the node n of the member function f on the object (through it when arrow) with the args, as the call it is (the object checked by checker with the globals g in the scope env to know the class; overloads chosen by pick); a->f(args) with a an object of a class is a.operator->()->f(args). Where the object goes first (Classes.objectFirst) and it has statements of its own, it is kept (Classes.kept) before the arguments: the call is then in the kept object’s scope. A member of a standard stream (cout.put(c)) is not provided yet.

cpp.Classes.checkedCall

def Classes.checkedCall (pick : Picking) (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (object : Expr) (arrow : Bool) (f : String) (args : List Expr) (check : Env Cpp.constructs -> Expr -> Kept.Checked) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

The call at the node n of the member function f on the object (through it when arrow) with the args (Classes.callOf with pick, checker, the globals g and the scope env), checked by check (as a value or an lvalue), the kept object’s statements first.

cpp.Classes.inherited

def Classes.inherited (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (object : Expr) (arrow : Bool) (f : String) (asLvalue : Bool) : Option (CheckResult Cpp.constructs (Lifted Cpp.constructs))

A data member found in a base, obj.f or p->f, as the access through the base subobjects (its access checked); none for a member of the class itself (the core’s), an error when two bases have it. a->f with a an object of a class is a.operator->()->f.

cpp.Classes.expression

def Classes.expression (pick : Picking) (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (e : Expr) : Option (CheckResult Cpp.constructs (Lifted Cpp.constructs))

C++’s class expressions: this, a member used alone, a member function’s call, a member found in a base.

cpp.Classes.statement

def Classes.statement (pick : Picking) (checker : Checker Cpp.constructs) (statements : StatementChecker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (s : Stmt) : Option (CheckResult Cpp.constructs (TypedStmt Cpp.constructs))

C++’s class statements: a member function’s call whose result is dropped is that call’s statement; the pure call (a pure virtual function’s body) stops the run.

cpp.Classes.lvalue

def Classes.lvalue (pick : Picking) (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (e : Expr) : Option (CheckResult Cpp.constructs (Lifted Cpp.constructs))

C++’s class lvalues: a member used alone, a member function’s call (one returning a reference is an lvalue), a member found in a base.

cpp.Classes.resolve

def Classes.resolve (t : TypeSyntax) : Option (Ty Cpp.constructs)

A class name as a type: its struct.

cpp.Cpp.nameParts

def Cpp.nameParts (f : String) : Option String * String

A lowered name’s parts: what comes before the last :: (none without one), and the name after it without a # suffix (A::f#1 is A and f).

cpp.Cpp.libraryOwner

def Cpp.libraryOwner (g : Globals Cpp.constructs) (f : String) : Option String

The library’s class whose member function f is (lowered as C::f), if it is one among the classes of g: the library models the standard library’s classes without every overload, so a call that matches none of the modeled ones may be right.

cpp.Cpp.mismatchOf

def Cpp.mismatchOf (g : Globals Cpp.constructs) (f : String) : Mismatch

What a call of f (in the program whose globals are g) whose arguments match no function means. For a library class’s member function: not provided (the model’s overloads are not all of the standard’s). Else rejected as clang says it: no matching member function for a class’s member function (lowered as C::f), no matching function for any other; by the name without its qualifier, as declared.