Skip to content

streams

def Streams.kindOf (n : NodeId) (t : Ty Cpp.constructs) : CheckResult Cpp.constructs OutputKind

What an operand of std::cout writes, by its type; none for a type std::cout does not write (a pointer other than a char pointer prints an address, which differs from run to run).

def Streams.typed (m : NodeId) (t : StreamStatement) (operands : List (TypedExpr Cpp.constructs)) : TypedStmt Cpp.constructs

A statement of the streams, as C++’s extension statement with its operands.

def Streams.formatArgument (p : Platform) (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (m : NodeId) (a : Expr) (change : FormatChange) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

A manipulator’s operand (setw, setprecision, setfill): an integer, as long.

def Streams.item (p : Platform) (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (e : Expr) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

An operand of std::cout: std::endl, a manipulator, or a value to write.

def Streams.items (p : Platform) (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (es : List Expr) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

The operands of std::cout in order.

def Streams.statement (p : Platform) (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 statements about streams, s checked by checker and statements in the context c with the variables in scope env (p the platform): std::cout << ..., std::cin.ignore(...), and a call of ’s printf or scanf as a statement (C’s formatted output and input, Streams.cFormatted).

def Streams.cFormatted (n : NodeId) (e : Expr) : Option Stmt

printf("...", args) or scanf("...", args) (with std:: or not, from ) as a statement e of its own at the node n: the C library’s formatted output or input with that format (C11 7.21.6.3, 7.21.6.4, as C’s statement sPrintf/sScanf). None for another call, or a format that is not a string literal.

def Streams.Checked : Type

The statements a check of streams gives, or why it does not.

def Streams.ignoring (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (e : Expr) : Option Streams.Checked

std::cin.ignore(), std::cin.ignore(count), std::cin.ignore(count, delimiter) (the expression e, checked by checker with the globals g and the variables in scope env): the operands, then the input that drops characters (count 1 and delimiter EOF by default, [istream.unformatted]p25); none for another expression.

def Streams.extracted (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (e : Expr) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

Reading into an object of a class: the call std::cin >> x, its operator>> found as an operator’s (the library’s of std::string, [string.io]); the stream it returns is dropped.

def Streams.inputItem (types : TypeExtension Cpp.constructs) (p : Platform) (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (e : Expr) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

An operand of std::cin (>>): a base manipulator, else an lvalue to read into, by its type: a number (an integer, a character, a floating value), a character array (a word, through its first element), an object of a class (its operator>>, Streams.extracted).

def Streams.inputItems (types : TypeExtension Cpp.constructs) (p : Platform) (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (es : List Expr) : CheckResult Cpp.constructs (List (TypedStmt Cpp.constructs))

The operands of std::cin in order.

def Streams.expression (types : TypeExtension Cpp.constructs) (p : Platform) (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (e : Expr) : Option (CheckResult Cpp.constructs (Lifted Cpp.constructs))

C++’s expressions about streams: std::cin >> a >> b and std::getline(std::cin, s), each input before, the value whether std::cin has not failed (an int).

def Streams.endLineNode (e : Expr) : Option NodeId

The node of e where it is std::endl, else none. One match with a default: a match on the second operand nested under the default of a match on the first would be compiled once per constructor of Expr, a function of several hundred kilobytes in the WasmGC build that every expression’s check calls (Streams.manipulatorOperand).

def Streams.manipulatorOperand (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (e : Expr) : Option (CheckResult Cpp.constructs (Lifted Cpp.constructs))

std::endl as an operand of a binary operator e outside an output ("Hello!" << endl, the first << written as < in cout < "Hello!" << endl, which binds as cout < ("Hello!" << endl)): a function template with no type to deduce its arguments from ([over.over]p1), so clang’s error at it, after an error in the left operand (checked by checker with the globals g in the scope env), which clang reports first. None for any other expression.

def StreamFormat.manipulate (f : StreamFormat) (m : Manipulator) : StreamFormat

A format with a manipulator applied.

def StreamFormat.change (f : StreamFormat) (c : FormatChange) (v : Int) : StreamFormat

A format changed with an operand (a negative width is 0; the fill is a character).

def StreamFormat.pad (f : StreamFormat) (text : String) : String

Text padded to the width with the fill: on the left, or on the right when left aligned.

def StreamFormat.integerText (f : StreamFormat) (t : IntegerType) (v : Int) : String

An integer of a type as written: in decimal with its sign (+ with showpos for a signed type or bool); in octal or hexadecimal as the unsigned value of its width, with the base’s prefix for showbase except for zero.

def StreamFormat.flags (f : StreamFormat) : Flags

printf’s flags for a floating output: + with showpos.

def FloatNotation.style (n : FloatNotation) : FloatStyle

printf’s style for the notation.

def StreamFormat.floatText (f : StreamFormat) (v : Float) : String

A floating value as written: %g, %f or %e with the precision, 6 when it is negative (upper case with uppercase).

def StreamFormat.isWord (f : StreamFormat) (t : IntegerType) : Bool

Whether an output is bool written as a word: inserted as is (no padding, the width kept).

def StreamFormat.valueText (f : StreamFormat) (t : IntegerType) (v : Int) : String

An integer output’s text: a character type’s character, bool as a word with boolalpha, else the number.

def Streams.write (s : State Cpp.constructs) (text : String) (usesWidth : Bool) : State Cpp.constructs

The state after writing text to std::cout; a formatted output uses the width up.

def Streams.output (n : NodeId) (kind : OutputKind) (v : Value) (k : List (Frame Cpp.constructs)) (s : State Cpp.constructs) : Configuration Cpp.constructs

Runs an output of a value in the stream’s format.

def Streams.skipped (c : Console) : List Char

The input after the whitespace std::cin skips.

def Streams.consumed (c : Console) (rest : List Char) (failed : Bool) : Console

The console after an input that stopped before rest: at the end (eofbit) when nothing is left, failed (failbit) as the read says.

def Streams.integerRead (t : IntegerType) (negative : Bool) (magnitude : Nat) : Int * Bool

The value num_get stores for an integer of a type: in range as it is; out of range the type’s maximum (or minimum), with failbit ([facet.num.get.virtuals]p3); an unsigned type takes a negative value modulo 2^width (as strtoull).

def Streams.scanKind (base : Nat) : ScanKind

How an integer is scanned in std::cin’s base (std::dec, std::hex with an optional 0x, std::oct).

def Streams.ready (c : Console) : Bool

Whether std::cin can read: it has not failed and is not at the end (else the sentry sets failbit, [istream]p4).

def Streams.number (t : Ty Cpp.constructs) (a : Address) (k : List (Frame Cpp.constructs)) (s : State Cpp.constructs) : Configuration Cpp.constructs

A number read into the object at an address, after the whitespace: a character type’s one character; an integer as num_get reads it (no digits: 0 and failbit); a floating value as strtod (none: 0 and failbit); no input left sets failbit and eofbit and leaves the value.

def Streams.word (xs : List Char) : List Char

A word (to whitespace) after the whitespace, and the rest.

def Streams.intoArray (platform : Platform) (n : NodeId) (p : Pointer) (k : List (Frame Cpp.constructs)) (s : State Cpp.constructs) : Configuration Cpp.constructs

A word read into a character array (through its first element) with its null; one that does not fit is out of bounds.

def Streams.text (line : Bool) (c : Console) : Option (List Char * List Char)

What std::string gets: a word after the whitespace (none: failbit and eofbit), or a line (to a newline, which is read and not kept; none at the end: failbit and eofbit), and the rest.

def Streams.setString (p : Platform) (s : State Cpp.constructs) (old : Value) (dataAt : Address) (sizeAt : Address) (capacityAt : Address) (text : List Char) : State Cpp.constructs

A std::string set to text: its old block released, a block of the text and its null made (as new[]), its size and capacity the text’s length.

def Streams.isSpace (c : Char) : Bool

Whether a character code is whitespace (as std::isspace in the C locale).

def Streams.isNewline (c : Char) : Bool

Whether a character is a newline.

def Streams.ignored (count : Int) (delimiter : Int) (input : List Char) : List Char

The input left after std::cin.ignore(count, delimiter) drops characters from input: up to count of them, or through the first that is delimiter (dropped too); EOF (a negative delimiter) is none ([istream.unformatted]p25). A loop: the input may be long.

def Streams.needsInput (p : Platform) (tag : CppStatement) (es : List (TypedExpr Cpp.constructs)) (s : State Cpp.constructs) : Bool

Whether an input from std::cin may read differently with more input than given so far (the debugger then waits for it): a character needs one after the whitespace; a number or a word needs one after the whitespace that is followed by whitespace (more could extend it); a line needs a newline. A stream that has failed reads nothing.

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

Runs C++’s statements about streams.