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

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

Clean up Clight examples; better temporary definition of multiply.

File size: 2.0 KB
Line 
1include "Clight/Animation.ma".
2
3definition myprog := mk_program fundef type
4  [〈succ_pos_of_nat 0 (* get_input *), External (succ_pos_of_nat 0) Tnil (Tint I32 Signed  )〉;
5  〈succ_pos_of_nat 1 (* main *), 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.