source: src/Clight/test/factorial.ma @ 725

Last change on this file since 725 was 725, checked in by campbell, 10 years ago

Do some light manual disambiguation to make Clight examples go through more
easily.

File size: 2.0 KB
Line 
1include "Clight/Animation.ma".
2
3definition myprog := mk_program clight_fundef type
4  [〈succ_pos_of_nat 0 (* get_input *), CL_External (succ_pos_of_nat 0) Tnil (Tint I32 Signed  )〉;
5  〈succ_pos_of_nat 1 (* main *), CL_Internal (
6    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 3, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 4, (Tint I32 Signed  )〉 ]
7      (Ssequence
8      (Scall (Some expr (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
9        (Expr (Evar (succ_pos_of_nat 0))
10          (Tfunction Tnil (Tint I32 Signed  )))
11        [])
12      (Ssequence
13      (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
14        (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
15      (Ssequence
16      (Ssequence
17      (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
18              (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
19        (Expr (Ebinop Ole
20          (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
21          (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
22          (Tint I32 Signed  ))
23        (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
24          (Expr (Ebinop Oadd
25            (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
26            (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
27            (Tint I32 Signed  )))
28        (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
29          (Expr (Ebinop Omul
30            (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
31            (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  )))
32            (Tint I32 Signed  )))
33      )
34      Sskip)
35      (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 3))
36                            (Tint I32 Signed  )))))))
37   
38   
39   
40  )〉]
41  (succ_pos_of_nat 1)
42  []
43.
44
45example exec:
46  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 5)]; OK ? (is_final s)) = OK ? (Some ? (repr 120)).
47normalize  (* you can examine the result here *)
48@refl qed.
Note: See TracBrowser for help on using the repository browser.