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

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

Common definition for animation semantics, and factor out IO definitions.

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))
11          (Tfunction Tnil (Tint I32 Signed  )))
12        [])
13      (Ssequence
14      (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
15        (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
16      (Ssequence
17      (Ssequence
18      (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
19              (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
20        (Expr (Ebinop Ole
21          (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
22          (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
23          (Tint I32 Signed  ))
24        (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
25          (Expr (Ebinop Oadd
26            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
27            (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
28            (Tint I32 Signed  )))
29        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
30          (Expr (Ebinop Omul
31            (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
32            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
33            (Tint I32 Signed  )))
34      )
35      Sskip)
36      (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
37                            (Tint I32 Signed  )))))))
38   
39   
40   
41  )〉]
42  (ident_of_nat 1)
43  []
44.
45
46example exec: finishes_with (repr 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 5)]).
47normalize  (* you can examine the result here *)
48@refl qed.
Note: See TracBrowser for help on using the repository browser.