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

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

Update remaining Clight examples.

File size: 1.9 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program clight_fundef 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 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
19          (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
20          (Tint I32 Signed  ))
21        (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
22          (Expr (Ebinop Oadd
23            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
24            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
25            (Tint I32 Signed  )))
26        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
27          (Expr (Ebinop Omul
28            (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
29            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
30            (Tint I32 Signed  )))
31      )
32      (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))))))
33   
34   
35   
36  )〉]
37  (ident_of_nat 1)
38  []
39.
40
41example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
42normalize  (* you can examine the result here *)
43@refl qed.
Note: See TracBrowser for help on using the repository browser.