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

Last change on this file since 725 was 725, checked in by campbell, 9 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.