source: src/Clight/test/factorial.c.ma @ 1157

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

definition myprog := mk_program clight_fundef ((list init_data) × type)
  [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
  〈ident_of_nat 1 (* main *), CL_Internal (
    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ; 〈ident_of_nat 4, (Tint I32 Signed  )〉 ]
      (Ssequence
      (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
        (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
        [])
      (Ssequence
      (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
        (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
      (Ssequence
      (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
              (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
        (Expr (Ebinop Ole (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
          (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
          (Tint I32 Signed  ))
        (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
          (Expr (Ebinop Oadd
            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
            (Tint I32 Signed  )))
        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
          (Expr (Ebinop Omul
            (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
            (Tint I32 Signed  )))
      )
      (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))))))
    
    
    
  )〉]
  (ident_of_nat 1)
  []
.

example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
normalize  (* you can examine the result here *)
@refl
qed.