source: Deliverables/D3.1/C-semantics/test/factorial.ma @ 415

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

A couple of amusing examples.

File size: 1.9 KB
Line 
1include "Animation.ma".
2
3ndefinition myprog := mk_program fundef type
4 [mk_pair ?? (succ_pos_of_nat 132 (* get_input *)) (External (succ_pos_of_nat 132) Tnil (Tint I32 Signed  ));
5  mk_pair ?? (succ_pos_of_nat 133 (* main *)) (Internal (
6    mk_function (Tint I32 Signed  ) [] [mk_pair ?? (succ_pos_of_nat 134) (Tint I32 Signed  ); mk_pair ?? (succ_pos_of_nat 135) (Tint I32 Signed  ); mk_pair ?? (succ_pos_of_nat 136) (Tint I32 Signed  )]
7      (Ssequence
8      (Scall (Some ? (Expr (Evar (succ_pos_of_nat 134)) (Tint I32 Signed  )))
9        (Expr (Evar (succ_pos_of_nat 132))
10          (Tfunction Tnil (Tint I32 Signed  )))
11        [])
12      (Ssequence
13      (Sassign (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed  ))
14        (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
15      (Ssequence
16      (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
17              (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
18        (Expr (Ebinop Ole
19          (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
20          (Expr (Evar (succ_pos_of_nat 134)) (Tint I32 Signed  )))
21          (Tint I32 Signed  ))
22        (Sassign (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
23          (Expr (Ebinop Oadd
24            (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
25            (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
26            (Tint I32 Signed  )))
27        (Sassign (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed  ))
28          (Expr (Ebinop Omul
29            (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed  ))
30            (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  )))
31            (Tint I32 Signed  )))
32      )
33      (Sreturn (Some ? (Expr (Evar (succ_pos_of_nat 135))
34                         (Tint I32 Signed  )))))))
35   
36   
37   
38  ))]
39  (succ_pos_of_nat 133)
40  []
41.
42
43nremark exec: result ? (exec_up_to myprog 40 [EVint (repr 5)]).
44nnormalize;  (* you can examine the result here *)
45@; nqed.
Note: See TracBrowser for help on using the repository browser.