rocq/theories/ScanCode.v
The checked module nanofil -O makes of rocq/programs/scan.c, as a term. Generated by rocq/gallina.pl; rocq/programs.sh checks it is current. Do not edit.
From Stdlib Require Import String ZArith List Ascii
From Nanofil Require Import Term
Import ListNotations
Open Scope string_scope
Open Scope Z_scope
The one-character atom with code n.
The module term.
TApp"module" TListTApp"func" TAtom"scan"; TAtom"export"; TAtom"w"; TListTApp"param" TAtom"p"; TApp"tmp" TAtom"v0"; TListTApp"block" TAtom"start"; TList[ ]; TListTApp"call" TApp"result" TApp"tmp" TAtom"v4"; TAtom"l"; TApp"global" TAtom"strlen"; TListTApp"arg" TAtom"p"; TApp"tmp" TAtom"v0"; TApp"call" TApp"result" TApp"tmp" TAtom"v7"; TAtom"p"; TApp"global" TAtom"strchr"; TListTApp"arg" TAtom"p"; TApp"tmp" TAtom"v0"; TApp"arg" TAtom"w"; TApp"const" TInt108; TApp"let" TApp"tmp" TAtom"v12"; TAtom"l"; TAtom"ptoi"; TListTApp"tmp" TAtom"v7"; TApp"let" TApp"tmp" TAtom"v14"; TAtom"w"; TApp"cmp" TAtom"eq"; TAtom"l"; TListTApp"tmp" TAtom"v12"; TApp"const" TInt0; TApp"branch" TApp"tmp" TAtom"v14"; TAtom"L8"; TAtom"L10"; TApp"block" TAtom"L8"; TList[ ]; TList[ ]; TApp"ret" TApp"const" TInt0; TApp"block" TAtom"L10"; TList[ ]; TListTApp"call" TApp"result" TApp"tmp" TAtom"v17"; TAtom"w"; TApp"global" TAtom"puts"; TListTApp"arg" TAtom"p"; TApp"tmp" TAtom"v7"; TApp"flight" TApp"tmp" TAtom"v20"; TAtom"add"; TListTApp"address" TApp"tmp" TAtom"v7"; TApp"const" TInt1; TApp"lower" TApp"tmp" TAtom"v7"; TApp"let" TApp"tmp" TAtom"chk0"; TAtom"a"; TApp"check" TInt0; TInt1; TAtom"read"; TInt1; TListTApp"tmp" TAtom"v20"; TApp"let" TApp"tmp" TAtom"v21"; TAtom"w"; TApp"raw_load" TAtom"sb"; TInt0; TListTApp"tmp" TAtom"chk0"; TApp"let" TApp"tmp" TAtom"v22"; TAtom"w"; TAtom"add"; TListTApp"tmp" TAtom"v4"; TApp"tmp" TAtom"v21"; TApp"ret" TApp"tmp" TAtom"v22"