rocq/spikes/ListSumCode.v
The checked module nanofil -O makes of rocq/spikes/listsum.c, as a term. Generated by rocq/gallina.pl; rocq/spikes/code.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"sum"; TAtom"export"; TAtom"l"; TListTApp"param" TAtom"p"; TApp"tmp" TAtom"v0"; TListTApp"block" TAtom"start"; TList[ ]; TList[ ]; TApp"goto" TAtom"L3"; TApp"block" TAtom"L3"; TListTApp"phi" TApp"tmp" TAtom"pr.2"; TAtom"l"; TListTApp"-" TAtom"L4"; TApp"tmp" TAtom"v13"; TApp"-" TAtom"start"; TApp"const" TInt0; TApp"phi" TApp"tmp" TAtom"pr.1"; TAtom"p"; TListTApp"-" TAtom"L4"; TApp"tmp" TAtom"v15"; TApp"-" TAtom"start"; TApp"tmp" TAtom"v0"; TListTApp"let" TApp"tmp" TAtom"v7"; TAtom"l"; TAtom"ptoi"; TListTApp"tmp" TAtom"pr.1"; TApp"let" TApp"tmp" TAtom"v8"; TAtom"w"; TApp"cmp" TAtom"ne"; TAtom"l"; TListTApp"tmp" TAtom"v7"; TApp"const" TInt0; TApp"branch" TApp"tmp" TAtom"v8"; TAtom"L4"; TAtom"L5"; TApp"block" TAtom"L4"; TList[ ]; TListTApp"flight" TApp"tmp" TAtom"v11"; TAtom"add"; TListTApp"address" TApp"tmp" TAtom"pr.1"; TApp"const" TInt8; TApp"lower" TApp"tmp" TAtom"pr.1"; TApp"let" TApp"tmp" TAtom"chk0"; TAtom"a"; TApp"check" TInt0; TInt8; TAtom"read"; TInt1; TListTApp"tmp" TAtom"v11"; TApp"let" TApp"tmp" TAtom"v12"; TAtom"l"; TApp"raw_load" TAtom"l"; TInt0; TListTApp"tmp" TAtom"chk0"; TApp"let" TApp"tmp" TAtom"v13"; TAtom"l"; TAtom"add"; TListTApp"tmp" TAtom"pr.2"; TApp"tmp" TAtom"v12"; TApp"let" TApp"tmp" TAtom"chk1"; TAtom"a"; TApp"half_check" TAtom"lower"; TInt0; TInt8; TAtom"read"; TInt8; TListTApp"tmp" TAtom"chk0"; TApp"tmp" TAtom"pr.1"; TApp"let" TApp"tmp" TAtom"v15"; TAtom"p"; TApp"raw_load_pointer" TInt0; TListTAtom"aux_read"; TAtom"lower_resolve"; TAtom"address_read"; TListTApp"tmp" TAtom"chk1"; TApp"goto" TApp"poll" TAtom"L3"; TApp"block" TAtom"L5"; TList[ ]; TList[ ]; TApp"ret" TApp"tmp" TAtom"pr.2"; TApp"func" TAtom"listsum"; TAtom"export"; TAtom"l"; TListTApp"param" TAtom"w"; TApp"tmp" TAtom"v0"; TListTApp"block" TAtom"start"; TList[ ]; TList[ ]; TApp"goto" TAtom"L4"; TApp"block" TAtom"L4"; TListTApp"phi" TApp"tmp" TAtom"pr.2"; TAtom"w"; TListTApp"-" TAtom"L5"; TApp"tmp" TAtom"v21"; TApp"-" TAtom"start"; TApp"const" TInt0; TApp"phi" TApp"tmp" TAtom"pr.1"; TAtom"p"; TListTApp"-" TAtom"L5"; TApp"tmp" TAtom"v12"; TApp"-" TAtom"start"; TApp"const" TInt0; TListTApp"let" TApp"tmp" TAtom"v10"; TAtom"w"; TApp"cmp" TAtom"slt"; TAtom"w"; TListTApp"tmp" TAtom"pr.2"; TApp"tmp" TAtom"v0"; TApp"branch" TApp"tmp" TAtom"v10"; TAtom"L5"; TAtom"L7"; TApp"block" TAtom"L5"; TList[ ]; TListTApp"let" TApp"tmp" TAtom"v12"; TAtom"p"; TApp"alloc" TInt16; TListTApp"const" TInt16; TApp"let" TApp"tmp" TAtom"chk0"; TAtom"a"; TApp"check" TInt0; TInt8; TAtom"write"; TInt8; TListTApp"tmp" TAtom"v12"; TApp"raw_store_pointer" TInt0; TApp"tmp" TAtom"pr.1"; TApp"tmp" TAtom"chk0"; TListTAtom"aux_ensure"; TAtom"lower_barrier"; TAtom"rooted_reload"; TAtom"lower_write"; TAtom"address_write"; TApp"flight" TApp"tmp" TAtom"v16"; TAtom"add"; TListTApp"address" TApp"tmp" TAtom"v12"; TApp"const" TInt8; TApp"lower" TApp"tmp" TAtom"v12"; TApp"let" TApp"tmp" TAtom"v18"; TAtom"l"; TApp"ext" TAtom"sw"; TListTApp"tmp" TAtom"pr.2"; TApp"let" TApp"tmp" TAtom"chk1"; TAtom"a"; TApp"half_check" TAtom"upper"; TInt0; TInt8; TAtom"write"; TInt1; TListTApp"tmp" TAtom"chk0"; TApp"tmp" TAtom"v16"; TApp"raw_store" TAtom"l"; TInt0; TApp"tmp" TAtom"v18"; TApp"tmp" TAtom"chk1"; TApp"let" TApp"tmp" TAtom"v21"; TAtom"w"; TAtom"add"; TListTApp"tmp" TAtom"pr.2"; TApp"const" TInt1; TApp"goto" TApp"poll" TAtom"L4"; TApp"block" TAtom"L7"; TList[ ]; TListTApp"call" TApp"result" TApp"tmp" TAtom"v23"; TAtom"l"; TApp"global" TAtom"sum"; TListTApp"arg" TAtom"p"; TApp"tmp" TAtom"pr.1"; TApp"ret" TApp"tmp" TAtom"v23"