exceptions

cpp.Exceptions.typeName

def Exceptions.typeName (t : Ty Cpp.constructs) : String

A type’s name as a handler names it (and as an uncaught exception is reported).

cpp.Exceptions.typed

def Exceptions.typed (n : NodeId) (e : ExceptionStatement) : TypedStmt Cpp.constructs

A statement of exceptions without operands.

cpp.CatchLabel.of

def CatchLabel.of (catches : Option String) (label : String) : CatchLabel

A handler’s entry: what it catches and its label.

cpp.Exceptions.basesWithin

def Exceptions.basesWithin (fuel : Nat) (known : List ClassMembers) (x : String) : List String

A class’s bases, and theirs (fuel bounds the depth).

cpp.TypedExpr.memberPath

def TypedExpr.memberPath {L : Constructs} (e : TypedExpr L) : List Nat

The members’ positions an lvalue reaches from its variable (a base subobject’s path).

cpp.Exceptions.catchable

def Exceptions.catchable (types : TypeExtension Cpp.constructs) (g : Globals Cpp.constructs) (t : Ty Cpp.constructs) : List Catchable

The names an exception of a type can be caught by: its own (the object itself), then, for a class, each of its bases’ that is one subobject reached through public bases (the base subobject, [except.handle]p3), and for a pointer to a class, each pointer to such a base (the path to the subobject it points to).

cpp.Exceptions.classOf

def Exceptions.classOf (g : Globals Cpp.constructs) (t : Ty Cpp.constructs) : Option ClassMembers

The class with constructors a type is, if any.

cpp.Exceptions.throwing

def Exceptions.throwing (k : Constructing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (e : Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

throw e: the exception object initialized from e, with the names a handler catches it by. One of a class with constructors is declared and constructed from e (copied, or the temporary itself, [except.throw]p3), then handed to the exception; any other holds e’s value.

cpp.Exceptions.catches

def Exceptions.catches (k : Choosing) (g : Globals Cpp.constructs) (t : Option TypeSyntax) : Option String

The name a handler’s written type catches by (a reference catches what it refers to), none for catch (...).

cpp.Declared

def Declared : Type

Statements that declare, and the environment with what they declare.

cpp.Exceptions.declaring

def Exceptions.declaring (k : Constructing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (x : DeclId) (name : String) (byRef : Bool) (u : Ty Cpp.constructs) : CheckResult Cpp.constructs Declared

A handler’s x declared from the exception (a pointer to the subobject it is caught as): bound to it by reference, else a copy, by the copy constructor for a class with constructors (through a reference to the exception).

cpp.Exceptions.handler

def Exceptions.handler (k : Constructing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (h : Handler) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

A handler’s code: the exception adopted into its scope, x declared from it, the body, the handler finished.

cpp.Exceptions.tryStatement

def Exceptions.tryStatement (k : Constructing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (body : Stmt) (handlers : List Handler) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

try { body } catch …: a block with the body run under the handlers’ frame, then a jump past the handlers, each handler at its label (followed by the jump), and the end label.

cpp.Exceptions.statement

def Exceptions.statement (k : Constructing) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (s : Stmt) : Option (CheckResult Cpp.constructs (TypedStmt Cpp.constructs))

C++‘s statements of exceptions: throw, throw;, try, a function try block (a function’s body in a try; a constructor’s is lowered with its members’ initializations, cpp.classes).

cpp.Exceptions.with

def Exceptions.with (s : State Cpp.constructs) (e : CppState) : State Cpp.constructs

A state with C++’s part changed.

cpp.Exceptions.forget

def Exceptions.forget (b : Nat) (scopes : List Scope) : List Scope

Scopes without a block (an exception thrown again leaves the handler’s scope that adopted it).

cpp.CatchLabel.handles

def CatchLabel.handles (t : Thrown) (h : CatchLabel) : Option (List Nat)

Whether a handler catches an exception, with the path to the subobject it refers to: catch (...) (the object itself), or one of the exception’s names.

cpp.CatchLabel.first

def CatchLabel.first (t : Thrown) (handlers : List CatchLabel) : Option (CatchLabel * List Nat)

The first handler that catches an exception, and the path to the subobject it refers to.

cpp.Ahead

data Ahead

What an exception meets first on its way out: a handler that catches it, a noexcept function’s body (at a position in the frames), or nothing (it leaves main).

cpp.Exceptions.ahead

def Exceptions.ahead (t : Thrown) (i : Nat) (k : List (Frame Cpp.constructs)) : Ahead

What an exception meets first in the frames from position i.

cpp.Exceptions.pastLastCall

def Exceptions.pastLastCall (i : Nat) (best : Nat) (k : List (Frame Cpp.constructs)) : Nat

How many frames, from position i, reach past the last call in them (best so far: none is 0).

cpp.Outcome.state

def Outcome.state {L : Constructs} (o : Outcome L) : Option (State L)

The state a configuration ended in, if it has one.

cpp.Exceptions.terminate

def Exceptions.terminate (n : NodeId) (trial : List (Frame Cpp.constructs)) (actual : List (Frame Cpp.constructs)) (s : State Cpp.constructs) : Configuration Cpp.constructs

A termination after unwinding the actual frames: first a trial unwinding the frames of the other choice, and when its output differs, the divergence noted at the throw.

cpp.Exceptions.propagate

def Exceptions.propagate (n : NodeId) (t : Thrown) (k : List (Frame Cpp.constructs)) (s : State Cpp.constructs) : Configuration Cpp.constructs

An exception on its way out (in the state), thrown as libc++abi does: when a handler catches it, the stack unwinds to it; else the run terminates, having unwound only the calls the noexcept function it meets made, or nothing ([except.terminate]p2 leaves it to the implementation; whether unwinding all of it, to the noexcept function’s body or out of main, would change the output is noted).

cpp.Exceptions.run

def Exceptions.run (ev : Evaluator Cpp.constructs) (n : NodeId) (tag : ExceptionStatement) (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 exceptions.

cpp.Exceptions.uncaught

def Exceptions.uncaught (s : State Cpp.constructs) : Configuration Cpp.constructs

How a run ends with an exception main let out: reported as uncaught, by its type.

cpp.Pointer.toSubobject

def Pointer.toSubobject (p : Pointer) (path : List Nat) : Pointer

A pointer to the subobject at a path in what it points to (null stays null).

cpp.Conversion

record Conversion

What catching an exception at a path gives: the state, the block of a converted pointer (if any) and the path in the exception object the handler refers to.

cpp.Exceptions.convert

def Exceptions.convert (s : State Cpp.constructs) (b : Nat) (path : List Nat) : Conversion

An exception caught at a path: an object’s subobject (the path, for a handler’s pointer to it); a pointer caught as a pointer to a base, the pointer converted in a block of its own (and no path in it).

cpp.Exceptions.frame

def Exceptions.frame (f : CppFrame) (u : Leaving) (k : List (Frame Cpp.constructs)) (s : State Cpp.constructs) : Configuration Cpp.constructs

How leaving passes C++’s frames: at a try block’s, an exception a handler catches becomes the one being handled, and the run jumps to that handler; at a terminating one, an exception ends the run; anything else passes.

cpp.Exceptions.caught

def Exceptions.caught (s : State Cpp.constructs) : Evaluated Cpp.constructs Value

The pointer to the exception being handled.

cpp.Exceptions.body

def Exceptions.body (f : FunctionDefinition) (body : TypedStmt Cpp.constructs) : TypedStmt Cpp.constructs

A function’s body as C++ runs it: a noexcept function’s under a frame an exception leaving it ends the run at ([except.spec]p5).