rocq/theories/SlotCode.v
The checked module nanofil -O makes of rocq/programs/slot.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"fill"; TAtom"export"; TAtom"p"; TListTApp"param" TAtom"w"; TApp"tmp" TAtom"v0"; TApp"param" TAtom"l"; TApp"tmp" TAtom"v2"; TListTApp"block" TAtom"start"; TList[ ]; TListTApp"let" TApp"tmp" TAtom"v7"; TAtom"p"; TAtom"copy"; TListTApp"global" TAtom"slot_size"; TApp"let" TApp"tmp" TAtom"chk0"; TAtom"a"; TApp"check" TInt0; TInt8; TAtom"read"; TInt1; TListTApp"tmp" TAtom"v7"; TApp"let" TApp"tmp" TAtom"v8"; TAtom"l"; TApp"raw_load" TAtom"l"; TInt0; TListTApp"tmp" TAtom"chk0"; TApp"let" TApp"tmp" TAtom"v10"; TAtom"w"; TApp"cmp" TAtom"ule"; TAtom"l"; TListTApp"tmp" TAtom"v8"; TApp"tmp" TAtom"v2"; TApp"branch" TApp"tmp" TAtom"v10"; TAtom"L4"; TAtom"L6"; TApp"block" TAtom"L4"; TList[ ]; TListTApp"let" TApp"tmp" TAtom"v11"; TAtom"p"; TAtom"copy"; TListTApp"global" TAtom"slot"; TApp"let" TApp"tmp" TAtom"chk1"; TAtom"a"; TApp"check" TInt0; TInt8; TAtom"read"; TInt8; TListTApp"tmp" TAtom"v11"; TApp"let" TApp"tmp" TAtom"v12"; TAtom"p"; TApp"raw_load_pointer" TInt0; TListTAtom"aux_read"; TAtom"lower_resolve"; TAtom"address_read"; TListTApp"tmp" TAtom"chk1"; TApp"call" TAtom"void"; TApp"global" TAtom"free"; TListTApp"arg" TAtom"p"; TApp"tmp" TAtom"v12"; TApp"let" TApp"tmp" TAtom"v13"; TAtom"p"; TAtom"copy"; TListTApp"global" TAtom"slot"; TApp"let" TApp"tmp" TAtom"v15"; TAtom"l"; TAtom"add"; TListTApp"tmp" TAtom"v2"; TApp"const" TInt1; TApp"call" TApp"result" TApp"tmp" TAtom"v16"; TAtom"p"; TApp"global" TAtom"malloc"; TListTApp"arg" TAtom"l"; TApp"tmp" TAtom"v15"; TApp"let" TApp"tmp" TAtom"chk2"; TAtom"a"; TApp"check" TInt0; TInt8; TAtom"write"; TInt8; TListTApp"tmp" TAtom"v13"; TApp"raw_store_pointer" TInt0; TApp"tmp" TAtom"v16"; TApp"tmp" TAtom"chk2"; TListTAtom"aux_ensure"; TAtom"lower_barrier"; TAtom"rooted_reload"; TAtom"lower_write"; TAtom"address_write"; TApp"let" TApp"tmp" TAtom"v17"; TAtom"p"; TAtom"copy"; TListTApp"global" TAtom"slot_size"; TApp"let" TApp"tmp" TAtom"chk3"; TAtom"a"; TApp"check" TInt0; TInt8; TAtom"write"; TInt1; TListTApp"tmp" TAtom"v17"; TApp"raw_store" TAtom"l"; TInt0; TApp"tmp" TAtom"v15"; TApp"tmp" TAtom"chk3"; TApp"goto" TAtom"L6"; TApp"block" TAtom"L6"; TList[ ]; TListTApp"let" TApp"tmp" TAtom"v20"; TAtom"p"; TAtom"copy"; TListTApp"global" TAtom"slot"; TApp"let" TApp"tmp" TAtom"chk4"; TAtom"a"; TApp"check" TInt0; TInt8; TAtom"read"; TInt8; TListTApp"tmp" TAtom"v20"; TApp"let" TApp"tmp" TAtom"v21"; TAtom"p"; TApp"raw_load_pointer" TInt0; TListTAtom"aux_read"; TAtom"lower_resolve"; TAtom"address_read"; TListTApp"tmp" TAtom"chk4"; TApp"call" TApp"result" TApp"tmp" TAtom"v24"; TAtom"p"; TApp"global" TAtom"memset"; TListTApp"arg" TAtom"p"; TApp"tmp" TAtom"v21"; TApp"arg" TAtom"w"; TApp"tmp" TAtom"v0"; TApp"arg" TAtom"l"; TApp"tmp" TAtom"v2"; TApp"let" TApp"tmp" TAtom"v25"; TAtom"p"; TAtom"copy"; TListTApp"global" TAtom"slot"; TApp"let" TApp"tmp" TAtom"chk5"; TAtom"a"; TApp"check" TInt0; TInt8; TAtom"read"; TInt8; TListTApp"tmp" TAtom"v25"; TApp"let" TApp"tmp" TAtom"v26"; TAtom"p"; TApp"raw_load_pointer" TInt0; TListTAtom"aux_read"; TAtom"lower_resolve"; TAtom"address_read"; TListTApp"tmp" TAtom"chk5"; TApp"flight" TApp"tmp" TAtom"v28"; TAtom"add"; TListTApp"address" TApp"tmp" TAtom"v26"; TApp"tmp" TAtom"v2"; TApp"lower" TApp"tmp" TAtom"v26"; TApp"let" TApp"tmp" TAtom"chk6"; TAtom"a"; TApp"check" TInt0; TInt1; TAtom"write"; TInt1; TListTApp"tmp" TAtom"v28"; TApp"raw_store" TAtom"b"; TInt0; TApp"const" TInt0; TApp"tmp" TAtom"chk6"; TApp"let" TApp"tmp" TAtom"v29"; TAtom"p"; TAtom"copy"; TListTApp"global" TAtom"slot"; TApp"let" TApp"tmp" TAtom"chk7"; TAtom"a"; TApp"check" TInt0; TInt8; TAtom"read"; TInt8; TListTApp"tmp" TAtom"v29"; TApp"let" TApp"tmp" TAtom"v30"; TAtom"p"; TApp"raw_load_pointer" TInt0; TListTAtom"aux_read"; TAtom"lower_resolve"; TAtom"address_read"; TListTApp"tmp" TAtom"chk7"; TApp"ret" TApp"tmp" TAtom"v30"; TApp"func" TAtom"use"; TAtom"export"; TAtom"w"; TList[ ]; TListTApp"block" TAtom"start"; TList[ ]; TListTApp"call" TApp"result" TApp"tmp" TAtom"v1"; TAtom"p"; TApp"global" TAtom"fill"; TListTApp"arg" TAtom"w"; TApp"const" TInt97; TApp"arg" TAtom"l"; TApp"const" TInt8; TApp"flight" TApp"tmp" TAtom"v4"; TAtom"add"; TListTApp"address" TApp"tmp" TAtom"v1"; TApp"const" TInt7; TApp"lower" TApp"tmp" TAtom"v1"; TApp"let" TApp"tmp" TAtom"chk0"; TAtom"a"; TApp"check" TInt0; TInt1; TAtom"read"; TInt1; TListTApp"tmp" TAtom"v4"; TApp"let" TApp"tmp" TAtom"v5"; TAtom"w"; TApp"raw_load" TAtom"sb"; TInt0; TListTApp"tmp" TAtom"chk0"; TApp"call" TApp"result" TApp"tmp" TAtom"v7"; TAtom"p"; TApp"global" TAtom"fill"; TListTApp"arg" TAtom"w"; TApp"const" TInt98; TApp"arg" TAtom"l"; TApp"const" TInt3; TApp"let" TApp"tmp" TAtom"chk1"; TAtom"a"; TApp"check" TInt0; TInt1; TAtom"read"; TInt1; TListTApp"tmp" TAtom"v7"; TApp"let" TApp"tmp" TAtom"v11"; TAtom"w"; TApp"raw_load" TAtom"sb"; TInt0; TListTApp"tmp" TAtom"chk1"; TApp"call" TApp"result" TApp"tmp" TAtom"v13"; TAtom"p"; TApp"global" TAtom"fill"; TListTApp"arg" TAtom"w"; TApp"const" TInt99; TApp"arg" TAtom"l"; TApp"const" TInt16; TApp"let" TApp"tmp" TAtom"v16"; TAtom"w"; TAtom"add"; TListTApp"tmp" TAtom"v5"; TApp"tmp" TAtom"v11"; TApp"flight" TApp"tmp" TAtom"v18"; TAtom"add"; TListTApp"address" TApp"tmp" TAtom"v13"; TApp"const" TInt15; TApp"lower" TApp"tmp" TAtom"v13"; TApp"let" TApp"tmp" TAtom"chk2"; TAtom"a"; TApp"check" TInt0; TInt1; TAtom"read"; TInt1; TListTApp"tmp" TAtom"v18"; TApp"let" TApp"tmp" TAtom"v19"; TAtom"w"; TApp"raw_load" TAtom"sb"; TInt0; TListTApp"tmp" TAtom"chk2"; TApp"let" TApp"tmp" TAtom"v20"; TAtom"w"; TAtom"add"; TListTApp"tmp" TAtom"v16"; TApp"tmp" TAtom"v19"; TApp"ret" TApp"tmp" TAtom"v20"; TApp"data" TAtom"slot"; TAtom"local"; TInt8; TListTApp"zero" TInt8; TApp"data" TAtom"slot_size"; TAtom"local"; TInt8; TListTApp"zero" TInt8