scanning

cfamily.ScanKind

data ScanKind

What a conversion reads: d, i, u, o, x X, c, s, f e g E G, %[…] (negated with ^), or n (reads nothing: the count of characters read so far is written).

cfamily.Directive

data Directive

A directive of a format: white space (any amount, matching any), a character to match, or a conversion (suppressed with *, a maximum width).

cfamily.ScanTarget

data ScanTarget

What an argument points to: an integer of a type; a character object of a type with room for bytes (%c %s %[, or one integer of its type for %hh); a floating object.

cfamily.Scanned

data Scanned

A value a conversion assigns: bytes are followed by a null when terminated (%s %[), not for %c (C11 7.21.6.2p12).

cfamily.ScanResult

record ScanResult

The result of scanf: the count it returns, the values assigned in order, the input left, and whether the behavior was defined.

cfamily.Scan.isSpace

def Scan.isSpace (c : Nat) : Bool

Whether a code is white space (C11 7.4.1.10).

cfamily.Scan.dropSpace

def Scan.dropSpace (cs : List Nat) : List Nat

The input after leading white space.

cfamily.Scan.kind

def Scan.kind (c : Nat) : Option ScanKind

The conversion of a code.

cfamily.Scan.setBody

def Scan.setBody (cs : List Nat) (acc : List Nat) : Option (List Nat * List Nat)

The codes up to the closing ], and the codes after it.

cfamily.Scan.hasRange

def Scan.hasRange (set : List Nat) (k : Nat) : Bool

Whether a - stands between two members (a range is implementation-defined, not in the subset).

cfamily.Scan.set

def Scan.set (cs : List Nat) : Option (List Nat * List Nat)

A set after [ and any ^: a ] right after is a member.

cfamily.Scan.parse

def Scan.parse (format : String) : Option (List Directive)

The directives of a format, none if it is not valid.

cfamily.IntegerToken

record IntegerToken

An integer read from the input: whether negative, the magnitude, how many digits, and the input after it.

cfamily.IntegerToken.withSign

def IntegerToken.withSign (negative : Bool) (t : IntegerToken) : IntegerToken

The token with a sign.

cfamily.Scan.digits

def Scan.digits (base : Nat) (limit : Nat) (acc : Nat) (count : Nat) (cs : List Nat) : IntegerToken

Digits in a base, at most limit of them.

cfamily.Scan.hexPrefix

def Scan.hexPrefix (limit : Nat) (cs : List Nat) : Bool

Whether the input starts with 0x or 0X and the width leaves room for it.

cfamily.Scan.body

def Scan.body (k : ScanKind) (limit : Nat) (cs : List Nat) : IntegerToken

The digits of a conversion after any sign: %o octal, %x hexadecimal after an optional 0x, %i by its prefix (0x hexadecimal, 0 octal), the others decimal.

cfamily.Scan.integer

def Scan.integer (k : ScanKind) (limit : Nat) (cs : List Nat) : IntegerToken

An integer token: an optional sign (within the width), then the digits.

cfamily.ScanKind.isSigned

def ScanKind.isSigned (k : ScanKind) : Bool

Whether a conversion is signed (strtol) rather than unsigned (strtoul).

cfamily.Scan.twoTo64

def Scan.twoTo64 : Nat

2^64.

cfamily.Scan.integerValue

def Scan.integerValue (k : ScanKind) (negative : Bool) (m : Nat) : Option Int

strtol’s or strtoul’s result on LP64; none when it is out of range (long or unsigned long).

cfamily.LengthModifier.objectType

def LengthModifier.objectType (p : Platform) (signed : Bool) (l : LengthModifier) : IntegerType

The type of an integer conversion’s object: by the length (hh char, h short) and the conversion’s signedness.

cfamily.ScanState

record ScanState

Where a scan is: the targets left, the input, how many were assigned, whether a conversion has completed, the values so far, and how long the input was at the start (what %n counts from).

cfamily.ScanStep

data ScanStep

A directive’s outcome: scanf stops with a result, or goes on from a state.

cfamily.ScanState.stop

def ScanState.stop (s : ScanState) (rest : List Nat) (defined : Bool) : ScanStep

Stopping: a matching failure (count so far, defined), or undefined behavior.

cfamily.ScanState.inputEnded

def ScanState.inputEnded (s : ScanState) : ScanStep

The input ended: EOF before the first conversion completed, else the count (C11 7.21.6.2p16).

cfamily.ScanState.assign

def ScanState.assign (s : ScanState) (suppressed : Bool) (rest : List Nat) (v : Scanned) : ScanStep

Going on with the input consumed to rest, and (unless suppressed) one more value for the next target.

cfamily.ScanTarget.suits

def ScanTarget.suits (t : ScanTarget) (v : Scanned) (null : Nat) : Bool

Whether the next target suits a value: the same integer type with the value in range (a character object too), room for the bytes (and the null for %s), the same floating format.

cfamily.ScanState.store

def ScanState.store (s : ScanState) (suppressed : Bool) (rest : List Nat) (v : Scanned) (null : Nat) : ScanStep

Assigning a value the next target must suit (a suppressed one is not assigned).

cfamily.ScanState.integer

def ScanState.integer (p : Platform) (s : ScanState) (suppressed : Bool) (size : LengthModifier) (k : ScanKind) (limit : Nat) : ScanStep

An integer conversion of the kind k in the scan s on the platform p (assigned unless suppressed, of the length modifier size, reading at most limit characters): no digits is a matching failure; a result out of range is undefined, and so is the length modifier L.

cfamily.ScanState.characters

def ScanState.characters (s : ScanState) (suppressed : Bool) (width : Nat) : ScanStep

%c: exactly the width’s characters (white space too); fewer is the end of the input.

cfamily.ScanState.token

def ScanState.token (s : ScanState) (suppressed : Bool) (token : List Nat) : ScanStep

A token of characters (%s, %[): stored with room for the null; an empty set match is a matching failure.

cfamily.LengthModifier.floatFormat

def LengthModifier.floatFormat (l : LengthModifier) : Option FloatFormat

The format of a floating conversion’s object: none is float, l double (L is the target’s, ScanState.floating).

cfamily.ScanState.longDoubleFormat

def ScanState.longDoubleFormat (s : ScanState) (suppressed : Bool) : Option FloatFormat

The format %Lf reads in the scan s: the next target’s when it is a long double (a precision above binary64’s, x87’s extended format), none for any other target (undefined, C11 7.21.6.2p10); binary64’s when the conversion is suppressed (no target: the characters read are the same).

cfamily.ScanState.floating

def ScanState.floating (s : ScanState) (suppressed : Bool) (size : LengthModifier) (limit : Nat) : ScanStep

A floating conversion of the scan s (assigned unless suppressed, of the length modifier size, reading at most limit characters): as strtod (strtold for L) within the width; out of range is undefined.

cfamily.Scan.inSet

def Scan.inSet (negated : Bool) (set : List Nat) (limit : Nat) (cs : List Nat) : List Nat

The codes at the front while they are in the set (or not, when negated), at most limit.

cfamily.ScanState.charactersRead

def ScanState.charactersRead (p : Platform) (s : ScanState) (suppressed : Bool) (width : Option Nat) (size : LengthModifier) : ScanStep

%n in the scan state s: the characters read so far written to the next target, an integer of the type of the length size on the platform p; not counted among the assignments (C11 7.21.6.2p12). suppressed or with a width it is undefined.

cfamily.ScanState.convert

def ScanState.convert (p : Platform) (s : ScanState) (suppressed : Bool) (width : Option Nat) (size : LengthModifier) (k : ScanKind) : ScanStep

A conversion, after the white space it skips (all but %c, %[ and %n).

cfamily.ScanKind.skipsSpace

def ScanKind.skipsSpace (k : ScanKind) : Bool

Whether a conversion skips leading white space.

cfamily.ScanState.directive

def ScanState.directive (p : Platform) (s : ScanState) (d : Directive) : ScanStep

One directive.

cfamily.Directive.isConversion

def Directive.isConversion (d : Directive) : Bool

Whether a directive is a conversion (after it completes, the input ending is no longer EOF); %n is not one (it reads nothing: scanf("%n%d") on no input is EOF).

cfamily.ScanState.run

def ScanState.run (p : Platform) (s : ScanState) (ds : List Directive) : ScanResult

The directives in order.

cfamily.Scan.run

def Scan.run (p : Platform) (format : String) (targets : List ScanTarget) (input : List Nat) : ScanResult

scanf on an input with the arguments’ targets; a format that is not valid is undefined.