objects

cpp.Access.isPublic

def Access.isPublic (a : Access) : Bool

Whether an access is public.

cpp.Objects.releaseOne

def Objects.releaseOne : String

The internal function a delete calls to release an object new made.

cpp.Objects.releaseArray

def Objects.releaseArray : String

The internal function delete[] calls to release an array new[] made.

cpp.Objects.construct

def Objects.construct (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (cls : ClassMembers) (receiver : TypedExpr Cpp.constructs) (args : List Expr) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

A class’s constructor called on an object new made (its pointer): chosen for the arguments, accessible here, each argument converted to its parameter.

cpp.Objects.store

def Objects.store (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (u : Ty Cpp.constructs) (object : TypedExpr Cpp.constructs) (args : List Expr) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

A value stored in an object new made: the argument converted to its type; without one, zero (new T(); an object of a class without constructors zero-initialized member by member, [dcl.init]p8, as a vector’s elements are).

cpp.Objects.initialized

def Objects.initialized (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (u : Ty Cpp.constructs) (cls : ClassMembers) (pointer : TypedExpr Cpp.constructs) (args : Option (List Expr)) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

An object of the class cls (of type u) initialized at pointer, as new T, new T() and new T(args) at the node n initialize theirs (args none, empty, or given; checked by k with the globals g and the scope env): default-initialized by its default constructor, if it has one, else left indeterminate ([dcl.init]p7); value-initialized, when the class declares no constructor (none is user-provided), by zeroing it and then running its implicit default constructor, if it has one (a default member initializer, a dynamic type to keep; [dcl.init]p8, p6); one object of the class (or of a class derived from it) without a copy constructor copied bit for bit (its implicit copy constructor is trivial, [class.copy.ctor]p12, as a declaration’s, Construction.trivialCopy); else constructed by the constructor chosen for the arguments.

cpp.Objects.newObject

def Objects.newObject (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (t : TypeSyntax) (args : Option (List Expr)) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

new T(args) at the node n, T written t (args none for new T; checked by k with the globals g and the scope env): the block allocated, its pointer in the temporary, the object initialized (Objects.initialized).

cpp.Objects.newPointer

def Objects.newPointer (n : NodeId) (u : Ty Cpp.constructs) : TypedExpr Cpp.constructs

The temporary holding the pointer new T (at n, of an object of type u) makes.

cpp.Objects.allocated

def Objects.allocated (g : Globals Cpp.constructs) (n : NodeId) (u : Ty Cpp.constructs) (making : CheckResult Cpp.constructs (List TypedCpp)) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

new T at n of an object of type u (in the globals g): the block allocated (byNew), its pointer in the temporary (Objects.newPointer), then the object initialized there by making; the expression is the pointer.

cpp.Objects.listedValue

def Objects.listedValue (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (t : Ty Cpp.constructs) (e : Expr) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

The value of a braced list’s element e for an object of type t (at n): e checked by k (with the globals g and the scope env) against t and converted as by assignment, not narrowed ([dcl.init.list]p7, Narrowing.of, as a declaration’s element is).

cpp.Objects.slots

def Objects.slots (g : Globals Cpp.constructs) (n : NodeId) (t : Ty Cpp.constructs) (lv : TypedExpr Cpp.constructs) : List (TypedExpr Cpp.constructs * Ty Cpp.constructs)

The subobjects a braced list initializes in order in lv, an object of the (complete) type t, each with its type (lvalues at the node n; an index’s type from the globals g): a struct’s named members (a base subobject first), an array’s elements, a union’s first member.

cpp.Objects.constructedType

def Objects.constructedType (g : Globals Cpp.constructs) (t : Ty Cpp.constructs) : Bool

Whether an object of type t is constructed or destroyed by functions (of a class of the globals g with constructors or a destructor): a braced list’s item is not simply stored into it.

cpp.Objects.oneOfClass

def Objects.oneOfClass (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (cls : ClassMembers) (args : List Expr) : Bool

Whether args are one object of the class cls or of a class derived from it (its base subobject), checked by k with the globals g and the scope env.

cpp.Objects.listInitialized

def Objects.listInitialized (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (u : Ty Cpp.constructs) (cls : ClassMembers) (pointer : TypedExpr Cpp.constructs) (xs : List Init) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

An object of the class cls (of type u) list-initialized at pointer by a braced list’s items xs at the node n ([dcl.init.list]p3; checked by k with the globals g and the scope env): an aggregate (a class that declares no constructor and has no virtual function or virtual base) from one object of its class (or of a derived one) is copied, from {} value-initialized (Objects.initialized), else zeroed, given its default member initializers (its implicit default constructor, if it has one) and its subobjects stored from the items in order (Objects.listStores; the rest keep their default member initializer’s value or zero, [dcl.init.aggr]p5); any other class is constructed by the constructor chosen for the items ({} value-initializes). An initializer-list constructor’s list, and a nested list among a constructor’s arguments, are not modeled here.

cpp.Objects.zeroed

def Objects.zeroed (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (depth : Nat) (n : NodeId) (u : Ty Cpp.constructs) (object : TypedExpr Cpp.constructs) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

The zero-initialization of the object of type u (an lvalue, at n; [dcl.init]p6): a struct as a whole (Objects.store), an array element by element (at most depth dimensions deep), a scalar zero.

cpp.Objects.listInto

def Objects.listInto (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (u : Ty Cpp.constructs) (pointer : TypedExpr Cpp.constructs) (object : TypedExpr Cpp.constructs) (xs : List Init) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

An object of type u (the lvalue object, its address pointer) list-initialized by a braced list’s items xs at the node n ([dcl.init.list]p3; checked by k with the globals g and the scope env): an object of a class by Objects.listInitialized, a scalar from its one element (not narrowed; {} zero), an array or a struct zeroed and its subobjects stored from the items (Objects.listStores).

cpp.Objects.newList

def Objects.newList (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (t : TypeSyntax) (xs : List Init) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

new T{xs} at the node n, T written t ([expr.new]p24, [dcl.init.list]p3; checked by k with the globals g and the scope env): the block allocated as new T’s, the object list-initialized there (Objects.listInto).

cpp.Objects.memberList

def Objects.memberList (k : Choosing) (statements : StatementChecker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (y : String) (xs : List Init) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

A member initialized by a braced list in a constructor (c{1, 2, 3}: direct-list-initialization, [class.base.init]p7, [dcl.init.list]p3; checked by k and statements in the context c and the scope env, at the node n): a member of a class with constructors constructed as a declaration T y{xs} is (from an initializer-list constructor’s list, Construction.fromList, else by the constructor chosen for the items, Construction.member); any other (an aggregate, an array, a scalar) list-initialized in place as new T{xs}’s object is (Objects.listInto). A member of a class with a destructor is guarded once it is made (destroyed if a later member throws, [except.ctor]p3).

cpp.Objects.listed

def Objects.listed (n : NodeId) (given : List Expr) : Init

The arguments of new T(args) as the brace list a declaration would be initialized with.

cpp.Objects.plainArray

def Objects.plainArray (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (u : Ty Cpp.constructs) (count : Expr) (zero : Bool) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

new T[count] of elements without constructors: the block allocated (zero-filled for new T[count]()), its pointer in the temporary.

cpp.Objects.classArray

def Objects.classArray (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (u : Ty Cpp.constructs) (cls : ClassMembers) (count : Expr) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

new T[count] of a class: the block allocated, then in a block of their own the elements constructed in order by the default constructor, with a guard (the pointer, and the count constructed beside it) that destroys the constructed ones when a constructor throws ([expr.new]p26: the array is not made).

cpp.Objects.newArray

def Objects.newArray (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (t : TypeSyntax) (count : Expr) (zero : Bool) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

new T[n]: the array allocated (zero-filled for new T[n]()), its pointer (to the first element) in the temporary.

cpp.Objects.copiesTrivially

def Objects.copiesTrivially (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (cls : ClassMembers) (args : List Expr) : Bool

Whether the arguments are one object of the class (or of a class derived from it: its base subobject) and the class has no copy constructor and declares no move (whose constructor then takes an rvalue, and an lvalue’s copy is deleted, [class.copy.ctor]p6): the copy is trivial ([class.copy.ctor]p12), the object stored bit for bit.

cpp.Objects.aggregate

def Objects.aggregate (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (u : Ty Cpp.constructs) (args : List Expr) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

T(args) of an aggregate (a class without constructors; T{args} from a braced list): a temporary named for the node, its members initialized from the arguments in order and the rest zero ([dcl.init.aggr]p4, p5; C++20 allows parentheses too), each argument converted at its own node.

cpp.Objects.temporary

def Objects.temporary (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (t : TypeSyntax) (args : List Expr) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

T(args) ([expr.type.conv]): an object of a class with constructors made in a temporary named for the node (the full expression’s end destroys it; passed by value or initializing an object, it is that object), reserved until its constructor has run (one that throws leaves no object to destroy), constructed with the arguments (one object of the class without a copy constructor copied bit for bit; T() of a class without constructors value-initialized, its members zero, [dcl.init]p8); for any other type with one argument, the argument converted (a cast).

cpp.Objects.expression

def Objects.expression (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (e : Expr) : Option (CheckResult Cpp.constructs (Lifted Cpp.constructs))

C++’s expressions of objects: new, new[], T(args), nullptr (a null pointer).

cpp.Objects.arrayLength

def Objects.arrayLength : String

The internal function a new T[count]’s count goes through: the count, unless it is negative (or too large for a long: negative there too), when std::bad_array_new_length is thrown ([expr.new]p8).

cpp.Objects.arrayLengthFunction

def Objects.arrayLengthFunction : Item

long #arrayLength(long n) { if (n < 0) throw std::bad_array_new_length(); return n; }.

cpp.Objects.prepare

def Objects.prepare (p : Program) : Program

A program whose own new T[count]s take their counts through #arrayLength (with it first), as it is if it has none. The library’s (lib: nodes) are not: their counts are sizes, never negative; nor a count written as a number.

cpp.Objects.nullptrType

def Objects.nullptrType : Ty Cpp.constructs

The type of nullptr, std::nullptr_t ([lex.nullptr]p1): a null pointer constant that converts to every pointer type, but not to an integer, nor to bool by copy-initialization ([conv.bool]); a condition takes it as false.

cpp.Objects.lvalue

def Objects.lvalue (k : Choosing) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (e : Expr) : Option (CheckResult Cpp.constructs (Lifted Cpp.constructs))

C++’s lvalues of objects: a temporary object of a class (materialized, [class.temporary]p2: a member function can be called on it).

cpp.Objects.deleting

def Objects.deleting (g : Globals Cpp.constructs) (n : NodeId) (array : Bool) (x : String) (p : Expr) : List Stmt

What delete does to a non-null pointer to an object of a class (or no class): the dispatch of its virtual destructor (which destroys and releases the complete object), else its destructor (if it has one) and the release; for delete[], the release of the array.

cpp.Objects.delete

def Objects.delete (k : Choosing) (statements : StatementChecker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (array : Bool) (e : Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

delete p and delete[] p: the pointer kept in a variable, and if it is not null, the object destroyed and its block released.

cpp.Objects.element

def Objects.element (k : Choosing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (f : String) (args : List Expr) : Option (CheckResult Cpp.constructs (TypedStmt Cpp.constructs))

The internal statements a container’s elements are handled by (Construction.rawArray): an object constructed at a pointer (a class’s constructor chosen for the arguments; one without constructors copied or left as it is), destroyed there (its class’s destructor, if it has one), moved there as a whole. None for any other call.

cpp.Objects.staticOnce

def Objects.staticOnce (statements : StatementChecker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (d : Stmt) : Option (CheckResult Cpp.constructs (TypedStmt Cpp.constructs))

A static declaration of a function initialized when first reached ([stmt.dcl]p4): its declaration under its global’s name (f::x), run once, its object then in the global scope (it ends after main, the latest made first, [basic.start.term]). An exception from its initialization leaves it unmade, to be tried again.

cpp.Objects.madeStatic

def Objects.madeStatic (s : State Cpp.constructs) (key : DeclId) : Bool

Whether the global scope has a function’s static object already.

cpp.Objects.promoted

def Objects.promoted (s : State Cpp.constructs) (key : DeclId) : State Cpp.constructs

A static object just made moved from the scope it was declared in to the global scope.

cpp.Objects.statement

def Objects.statement (k : Choosing) (statements : StatementChecker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (s : Stmt) : Option (CheckResult Cpp.constructs (TypedStmt Cpp.constructs))

C++’s statements of objects: delete, a static declaration initialized when first reached, and the internal releases.

cpp.Objects.run

def Objects.run (ev : Evaluator Cpp.constructs) (n : NodeId) (tag : ObjectStatement) (types : List (Ty Cpp.constructs)) (es : List (TypedExpr Cpp.constructs)) (k : List (Frame Cpp.constructs)) (s : State Cpp.constructs) : Configuration Cpp.constructs

Running a statement of objects: allocating (one object, or an array of count elements) and setting the variable to its pointer; releasing a block new (or new[]) allocated, given by its start (a null pointer does nothing); marking a guard; destroying the elements of a block new[] allocated, the last first (as many as the block has).

cpp.Objects.releasable

def Objects.releasable (m : Memory Cpp.constructs) (array : Bool) (b : Nat) (path : List Nat) (i : Int) (whole : Bool) : Bool

Whether a pointer is to the start of a block new (or new[], or the library’s raw allocation) made, so delete (or delete[]) can release it.

cpp.Objects.release

def Objects.release (ev : Evaluator Cpp.constructs) (n : NodeId) (array : Bool) (choice : Option String) (es : List (TypedExpr Cpp.constructs)) (k : List (Frame Cpp.constructs)) (s : State Cpp.constructs) : Configuration Cpp.constructs

Releasing a block delete (or delete[]) was given, by its start (a null pointer does nothing); with a choice, the library released it only because of an implementation’s choice (a later stop at it depends on the choice).

cpp.Objects.keep

def Objects.keep (ev : Evaluator Cpp.constructs) (n : NodeId) (choice : String) (es : List (TypedExpr Cpp.constructs)) (k : List (Frame Cpp.constructs)) (s : State Cpp.constructs) : Configuration Cpp.constructs

Keeping the block a pointer (an lvalue, such as a vector’s) is to under a new number because of an implementation’s choice: the object moves to the new number, the pointer is set to it, and the old number goes on to the new one (a pointer to it still reaches the object, assuming the choice). A null pointer does nothing.

cpp.Objects.runWith

def Objects.runWith (ev : Evaluator Cpp.constructs) (n : NodeId) (tag : ObjectStatement) (types : List (Ty Cpp.constructs)) (es : List (TypedExpr Cpp.constructs)) (ss : List (TypedStmt Cpp.constructs)) (k : List (Frame Cpp.constructs)) (s : State Cpp.constructs) : Configuration Cpp.constructs

Running a statement of objects with its statements: a function’s static object made once and moved into the global scope; any other as Objects.run runs it.