source: src/Clight/test/null-op.c.ma @ 965

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

Update some Clight examples.

File size: 3.7 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program clight_fundef type
5  [〈ident_of_nat 0 (* main *), CL_Internal (
6     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I8 Unsigned ))〉 ]
7       (Ssequence
8       (Sassign (Expr (Evar (ident_of_nat 2))
9                  (Tpointer Any (Tint I8 Unsigned )))
10         (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
11           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
12           (Tpointer Any (Tint I8 Unsigned ))))
13       (Ssequence
14       (Sassign (Expr (Evar (ident_of_nat 3))
15                  (Tpointer Any (Tint I8 Unsigned )))
16         (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
17           (Tpointer Any (Tint I8 Unsigned ))))
18       (Ssequence
19       (Sifthenelse (Expr (Ebinop Oeq
20                      (Expr (Evar (ident_of_nat 2))
21                        (Tpointer Any (Tint I8 Unsigned )))
22                      (Expr (Evar (ident_of_nat 3))
23                        (Tpointer Any (Tint I8 Unsigned ))))
24                      (Tint I32 Signed  ))
25         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
26                               (Tint I32 Signed  ))))
27         Sskip)
28       (Ssequence
29       (Sifthenelse (Expr (Ebinop Ogt
30                      (Expr (Ebinop Osub
31                        (Expr (Evar (ident_of_nat 2))
32                          (Tpointer Any (Tint I8 Unsigned )))
33                        (Expr (Evar (ident_of_nat 2))
34                          (Tpointer Any (Tint I8 Unsigned ))))
35                        (Tint I32 Signed  ))
36                      (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
37                      (Tint I32 Signed  ))
38         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
39                               (Tint I32 Signed  ))))
40         Sskip)
41       (Ssequence
42       (Sassign (Expr (Evar (ident_of_nat 2))
43                  (Tpointer Any (Tint I8 Unsigned )))
44         (Expr (Ebinop Oadd
45           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
46           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
47           (Tpointer Any (Tint I8 Unsigned ))))
48       (Ssequence
49       (Sassign (Expr (Evar (ident_of_nat 2))
50                  (Tpointer Any (Tint I8 Unsigned )))
51         (Expr (Ebinop Oadd
52           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
53           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))))
54           (Tpointer Any (Tint I8 Unsigned ))))
55       (Ssequence
56       (Sassign (Expr (Evar (ident_of_nat 2))
57                  (Tpointer Any (Tint I8 Unsigned )))
58         (Expr (Ebinop Osub
59           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
60           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
61           (Tpointer Any (Tint I8 Unsigned ))))
62       (Sreturn (Some expr (Expr (Ebinop Oeq
63                             (Expr (Evar (ident_of_nat 2))
64                               (Tpointer Any (Tint I8 Unsigned )))
65                             (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
66                               (Expr (Ecast (Tpointer Any Tvoid)
67                                 (Expr (Econst_int I8 (repr ? 0))
68                                   (Tint I8 Unsigned )))
69                                 (Tpointer Any Tvoid)))
70                               (Tpointer Any (Tint I8 Unsigned ))))
71                             (Tint I32 Signed  )))))))))))
72     
73     
74     
75   )〉]
76  (ident_of_nat 0)
77  []
78.
79
80example exec: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 50 [ ]).
81normalize  (* you can examine the result here *)
82@refl
83qed.
Note: See TracBrowser for help on using the repository browser.