rocq/glibc/LenCode.v
The checked module nanofil -O makes of rocq/glibc/len.c with user glibc's string/strlen.os, linked by rocq/link.pl, as a term. Generated by rocq/gallina.pl; rocq/glibc/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"main"; TAtom"export"; TAtom"w"; TList[ ]; TListTApp"block" TAtom"start"; TList[ ]; TListTApp"let" TApp"tmp" TAtom"v0"; TAtom"p"; TAtom"copy"; TListTApp"global" TAtom"len#msg"; TApp"call" TApp"result" TApp"tmp" TAtom"v1"; TAtom"l"; TApp"global" TAtom"strlen"; TListTApp"arg" TAtom"p"; TApp"tmp" TAtom"v0"; TApp"ret" TApp"tmp" TAtom"v1"; TApp"data" TAtom"len#msg"; TApp"ro" TAtom"local"; TInt1; TListTApp"item" TAtom"b"; TApp"str" TListTAtom"h"; TAtom"e"; TAtom"l"; TAtom"l"; TAtom"o"; TAtom","; TAtom" "; TAtom"g"; TAtom"l"; TAtom"i"; TAtom"b"; TAtom"c"; TApp"zero" TInt1; TApp"func" TAtom"__strlen"; TAtom"export"; TAtom"l"; TListTApp"param" TAtom"p"; TApp"tmp" TAtom"v0"; TListTApp"block" TAtom"start"; TList[ ]; TListTApp"let" TApp"tmp" TAtom"v4"; TAtom"l"; TAtom"ptoi"; TListTApp"tmp" TAtom"v0"; TApp"let" TApp"tmp" TAtom"v9"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"v4"; TApp"const" TInt18446744073709551608; TApp"let" TApp"tmp" TAtom"lc.2"; TAtom"l"; TAtom"sub"; TListTApp"tmp" TAtom"v9"; TApp"tmp" TAtom"v4"; TApp"flight" TApp"tmp" TAtom"v10"; TAtom"add"; TListTApp"address" TApp"tmp" TAtom"v0"; TApp"tmp" TAtom"lc.2"; TApp"lower" TApp"tmp" TAtom"v0"; TApp"let" TApp"tmp" TAtom"chk0"; TAtom"a"; TApp"check" TInt0; TInt8; TAtom"read"; TInt1; TListTApp"tmp" TAtom"v10"; TApp"let" TApp"tmp" TAtom"v13"; TAtom"l"; TApp"raw_load" TAtom"l"; TInt0; TListTApp"tmp" TAtom"chk0"; TApp"let" TApp"tmp" TAtom"iw_1.v6"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"v13"; TApp"const" TInt9187201950435737471; TApp"let" TApp"tmp" TAtom"iw_1.v8"; TAtom"l"; TAtom"add"; TListTApp"tmp" TAtom"iw_1.v6"; TApp"const" TInt9187201950435737471; TApp"let" TApp"tmp" TAtom"iw_1.v10"; TAtom"l"; TAtom"or"; TListTApp"tmp" TAtom"iw_1.v8"; TApp"tmp" TAtom"v13"; TApp"let" TApp"tmp" TAtom"iw_1.v12"; TAtom"l"; TAtom"or"; TListTApp"tmp" TAtom"iw_1.v10"; TApp"const" TInt9187201950435737471; TApp"let" TApp"tmp" TAtom"iw_1.v13"; TAtom"l"; TAtom"xor"; TListTApp"tmp" TAtom"iw_1.v12"; TApp"const" TInt−1; TApp"let" TApp"tmp" TAtom"iw_2.v10"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"v4"; TApp"const" TInt7; TApp"let" TApp"tmp" TAtom"iw_2.v11"; TAtom"l"; TAtom"shl"; TListTApp"tmp" TAtom"iw_2.v10"; TApp"const" TInt3; TApp"let" TApp"tmp" TAtom"iw_2.v12"; TAtom"l"; TAtom"shr"; TListTApp"tmp" TAtom"iw_1.v13"; TApp"tmp" TAtom"iw_2.v11"; TApp"let" TApp"tmp" TAtom"v23"; TAtom"w"; TApp"cmp" TAtom"ne"; TAtom"l"; TListTApp"tmp" TAtom"iw_2.v12"; TApp"const" TInt0; TApp"branch" TApp"tmp" TAtom"v23"; TAtom"iw_3.start"; TAtom"L28"; TApp"block" TAtom"iw_3.start"; TList[ ]; TListTApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v6"; TAtom"w"; TApp"cmp" TAtom"eq"; TAtom"l"; TListTApp"tmp" TAtom"iw_2.v12"; TApp"const" TInt0; TApp"branch" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v6"; TAtom"iw_3.iw_1.iw_1.L4"; TAtom"iw_3.iw_1.iw_1.L3"; TApp"block" TAtom"iw_3.iw_1.iw_1.L3"; TList[ ]; TListTApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v8"; TAtom"l"; TAtom"neg"; TListTApp"tmp" TAtom"iw_2.v12"; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v9"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_2.v12"; TApp"tmp" TAtom"iw_3.iw_1.iw_1.v8"; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v10"; TAtom"l"; TAtom"sub"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v9"; TApp"const" TInt1; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v11"; TAtom"l"; TAtom"shr"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v10"; TApp"const" TInt1; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v12"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v11"; TApp"const" TInt6148914691236517205; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v13"; TAtom"l"; TAtom"sub"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v10"; TApp"tmp" TAtom"iw_3.iw_1.iw_1.v12"; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v14"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v13"; TApp"const" TInt3689348814741910323; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v15"; TAtom"l"; TAtom"shr"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v13"; TApp"const" TInt2; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v16"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v15"; TApp"const" TInt3689348814741910323; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v17"; TAtom"l"; TAtom"add"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v14"; TApp"tmp" TAtom"iw_3.iw_1.iw_1.v16"; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v18"; TAtom"l"; TAtom"shr"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v17"; TApp"const" TInt4; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v19"; TAtom"l"; TAtom"add"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v17"; TApp"tmp" TAtom"iw_3.iw_1.iw_1.v18"; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v20"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v19"; TApp"const" TInt1085102592571150095; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v21"; TAtom"l"; TAtom"mul"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v20"; TApp"const" TInt72340172838076673; TApp"let" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v22"; TAtom"l"; TAtom"shr"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v21"; TApp"const" TInt56; TApp"goto" TAtom"iw_3.iw_1.iw_1.L4"; TApp"block" TAtom"iw_3.iw_1.iw_1.L4"; TListTApp"phi" TApp"tmp" TAtom"iw_3.iw_1.iw_1.v23"; TAtom"w"; TListTApp"-" TAtom"iw_3.iw_1.iw_1.L3"; TApp"tmp" TAtom"iw_3.iw_1.iw_1.v22"; TApp"-" TAtom"iw_3.start"; TApp"const" TInt64; TListTApp"let" TApp"tmp" TAtom"iw_3.iw_1.v27"; TAtom"w"; TAtom"shr"; TListTApp"tmp" TAtom"iw_3.iw_1.iw_1.v23"; TApp"const" TInt3; TApp"let" TApp"tmp" TAtom"v26"; TAtom"l"; TApp"ext" TAtom"uw"; TListTApp"tmp" TAtom"iw_3.iw_1.v27"; TApp"ret" TApp"tmp" TAtom"v26"; TApp"block" TAtom"L28"; TListTApp"phi" TApp"tmp" TAtom"pr.1"; TAtom"p"; TListTApp"-" TAtom"L28"; TApp"tmp" TAtom"v32"; TApp"-" TAtom"start"; TApp"tmp" TAtom"v10"; TListTApp"flight" TApp"tmp" TAtom"v32"; TAtom"add"; TListTApp"address" TApp"tmp" TAtom"pr.1"; TApp"const" TInt8; TApp"lower" TApp"tmp" TAtom"pr.1"; TApp"let" TApp"tmp" TAtom"chk1"; TAtom"a"; TApp"check" TInt0; TInt8; TAtom"read"; TInt1; TListTApp"tmp" TAtom"v32"; TApp"let" TApp"tmp" TAtom"v33"; TAtom"l"; TApp"raw_load" TAtom"l"; TInt0; TListTApp"tmp" TAtom"chk1"; TApp"let" TApp"tmp" TAtom"iw_4.iw_1.v8"; TAtom"l"; TAtom"sub"; TListTApp"tmp" TAtom"v33"; TApp"const" TInt72340172838076673; TApp"let" TApp"tmp" TAtom"iw_4.iw_1.v10"; TAtom"l"; TAtom"xor"; TListTApp"tmp" TAtom"v33"; TApp"const" TInt−1; TApp"let" TApp"tmp" TAtom"iw_4.iw_1.v11"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_4.iw_1.v8"; TApp"tmp" TAtom"iw_4.iw_1.v10"; TApp"let" TApp"tmp" TAtom"iw_4.iw_1.v13"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_4.iw_1.v11"; TApp"const" TInt9259542123273814144; TApp"let" TApp"tmp" TAtom"v37"; TAtom"w"; TApp"cmp" TAtom"eq"; TAtom"l"; TListTApp"tmp" TAtom"iw_4.iw_1.v13"; TApp"const" TInt0; TApp"branch" TApp"tmp" TAtom"v37"; TApp"poll" TAtom"L28"; TAtom"iw_5.start"; TApp"block" TAtom"iw_5.start"; TList[ ]; TList[ ]; TApp"branch" TApp"tmp" TAtom"v37"; TAtom"iw_5.iw_3.iw_1.iw_1.L4"; TAtom"iw_5.iw_3.iw_1.iw_1.L3"; TApp"block" TAtom"iw_5.iw_3.iw_1.iw_1.L3"; TList[ ]; TListTApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v8"; TAtom"l"; TAtom"neg"; TListTApp"tmp" TAtom"iw_4.iw_1.v13"; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v9"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_4.iw_1.v13"; TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v8"; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v10"; TAtom"l"; TAtom"sub"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v9"; TApp"const" TInt1; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v11"; TAtom"l"; TAtom"shr"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v10"; TApp"const" TInt1; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v12"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v11"; TApp"const" TInt6148914691236517205; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v13"; TAtom"l"; TAtom"sub"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v10"; TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v12"; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v14"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v13"; TApp"const" TInt3689348814741910323; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v15"; TAtom"l"; TAtom"shr"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v13"; TApp"const" TInt2; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v16"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v15"; TApp"const" TInt3689348814741910323; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v17"; TAtom"l"; TAtom"add"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v14"; TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v16"; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v18"; TAtom"l"; TAtom"shr"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v17"; TApp"const" TInt4; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v19"; TAtom"l"; TAtom"add"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v17"; TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v18"; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v20"; TAtom"l"; TAtom"and"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v19"; TApp"const" TInt1085102592571150095; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v21"; TAtom"l"; TAtom"mul"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v20"; TApp"const" TInt72340172838076673; TApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v22"; TAtom"l"; TAtom"shr"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v21"; TApp"const" TInt56; TApp"goto" TAtom"iw_5.iw_3.iw_1.iw_1.L4"; TApp"block" TAtom"iw_5.iw_3.iw_1.iw_1.L4"; TListTApp"phi" TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v23"; TAtom"w"; TListTApp"-" TAtom"iw_5.iw_3.iw_1.iw_1.L3"; TApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v22"; TApp"-" TAtom"iw_5.start"; TApp"const" TInt64; TListTApp"let" TApp"tmp" TAtom"iw_5.iw_3.iw_1.v27"; TAtom"w"; TAtom"shr"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.iw_1.v23"; TApp"const" TInt3; TApp"let" TApp"tmp" TAtom"v41"; TAtom"l"; TApp"ext" TAtom"uw"; TListTApp"tmp" TAtom"iw_5.iw_3.iw_1.v27"; TApp"flight" TApp"tmp" TAtom"v42"; TAtom"add"; TListTApp"address" TApp"tmp" TAtom"v32"; TApp"tmp" TAtom"v41"; TApp"lower" TApp"tmp" TAtom"v32"; TApp"let" TApp"tmp" TAtom"v44"; TAtom"l"; TAtom"ptoi"; TListTApp"tmp" TAtom"v42"; TApp"let" TApp"tmp" TAtom"v46"; TAtom"l"; TAtom"sub"; TListTApp"tmp" TAtom"v44"; TApp"tmp" TAtom"v4"; TApp"ret" TApp"tmp" TAtom"v46"; TApp"alias" TAtom"strlen"; TAtom"weak"; TAtom"__strlen"