Module MutrecA
From
Coq
Require
Import
String
List
ZArith
.
From
compcert
Require
Import
Coqlib
Integers
Floats
AST
Ctypes
Cop
Clight
Clightdefs
.
Require
Import
MutrecHeader
.
Local
Open
Scope
Z_scope
.
Definition
_memoized
:
ident
:= 54%
positive
.
Definition
_t
:
ident
:= 56%
positive
.
Definition
_x
:
ident
:= 55%
positive
.
Definition
_t
'1 :
ident
:= 59%
positive
.
Definition
v_memoized
:= {|
gvar_info
:= (
tarray
tint
MAX
);
gvar_init
:= (
Init_space
(4 *
MAX
) ::
nil
);
gvar_readonly
:=
false
;
gvar_volatile
:=
false
|}.
Definition
func_f
:= {|
fn_return
:=
tint
;
fn_callconv
:=
cc_default
;
fn_params
:= ((
_x
,
tint
) ::
nil
);
fn_vars
:=
nil
;
fn_temps
:= ((
_t
,
tint
) :: (
_t
'1,
tint
) ::
nil
);
fn_body
:=
(
Ssequence
(
Sifthenelse
(
Ebinop
Oeq
(
Etempvar
_x
tint
) (
Econst_int
(
Int.repr
0)
tint
)
tint
)
(
Sreturn
(
Some
(
Econst_int
(
Int.repr
0)
tint
)))
Sskip
)
(
Ssequence
(
Sset
_t
(
Ederef
(
Ebinop
Oadd
(
Evar
_memoized
(
tarray
tint
1000)) (
Etempvar
_x
tint
)
(
tptr
tint
))
tint
))
(
Ssequence
(
Sifthenelse
(
Ebinop
Oeq
(
Etempvar
_t
tint
)
(
Econst_int
(
Int.repr
0)
tint
)
tint
)
(
Ssequence
(
Ssequence
(
Scall
(
Some
_t
'1)
(
Evar
g_id
(
Tfunction
(
Tcons
tint
Tnil
)
tint
cc_default
))
((
Ebinop
Osub
(
Etempvar
_x
tint
) (
Econst_int
(
Int.repr
1)
tint
)
tint
) ::
nil
))
(
Sset
_t
(
Ebinop
Oadd
(
Etempvar
_t
'1
tint
) (
Etempvar
_x
tint
)
tint
)))
(
Sassign
(
Ederef
(
Ebinop
Oadd
(
Evar
_memoized
(
tarray
tint
1000))
(
Etempvar
_x
tint
) (
tptr
tint
))
tint
) (
Etempvar
_t
tint
)))
Sskip
)
(
Sreturn
(
Some
(
Etempvar
_t
tint
))))))
|}.
Definition
composites
:
list
composite_definition
:=
nil
.
Definition
global_definitions
:
list
(
ident
*
globdef
fundef
type
) :=
((
g_id
,
Gfun
(
External
(
EF_external
"
g
"
(
mksignature
(
AST.Tint
::
nil
) (
Some
AST.Tint
)
cc_default
true
))
(
Tcons
tint
Tnil
)
tint
cc_default
)) :: (
_memoized
,
Gvar
v_memoized
) ::
(
f_id
,
Gfun
(
Internal
func_f
)) ::
nil
).
Definition
public_idents
:
list
ident
:=
(
f_id
::
g_id
::
nil
).
Definition
prog
:
Clight.program
:=
mkprogram
composites
global_definitions
public_idents
main_id
Logic.I
.