source: src/Clight/test/oneoff.c.ma @ 2180

include "Clight/Cexec.ma".
include "common/Animation.ma".

definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
  [][〈ident_of_nat 0 (* main *), CL_Internal (
       mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tarray (Tint I8 Unsigned ) 4)〉 ]
         (Ssequence
         (Sassign (Expr (Ederef
                    (Expr (Ebinop Oadd
                      (Expr (Evar (ident_of_nat 1))
                        (Tarray (Tint I8 Unsigned ) 4))
                      (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
                      (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
           (Expr (Ecast (Tint I8 Unsigned )
             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
             (Tint I8 Unsigned )))
         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
                               (Tint I32 Signed  )))))
       
       
       
     )〉]
  (ident_of_nat 0)
  
.

(*
example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
normalize  (* you can examine the result here *)
*)