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

Last change on this file since 2177 was 1513, checked in by campbell, 9 years ago

Fix up Clight examples.

File size: 2.0 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
5  [][〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
6    〈ident_of_nat 1 (* main *), CL_Internal (
7      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  )〉 ]
8        (Ssequence
9        (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
10          (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
11          [])
12        (Ssequence
13        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
14          (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
15        (Ssequence
16        (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
17                (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
18          (Expr (Ebinop Ole
19            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
20            (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
21            (Tint I32 Signed  ))
22          (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
23            (Expr (Ebinop Oadd
24              (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
25              (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
26              (Tint I32 Signed  )))
27          (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
28            (Expr (Ebinop Omul
29              (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
30              (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
31              (Tint I32 Signed  )))
32        )
33        (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
34                              (Tint I32 Signed  )))))))
35     
36     
37     
38    )〉]
39  (ident_of_nat 1)
40 
41.
42
43(*
44example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
45normalize  (* you can examine the result here *)
46*)
Note: See TracBrowser for help on using the repository browser.