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

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

Fix up some minor null pointer issues in Clight.
Add corresponding Cminor example and fix up pretty printer a little.

File size: 3.6 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 (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 (repr 0)) (Tint I32 Signed  ))))
26         Sskip)
27       (Ssequence
28       (Sifthenelse (Expr (Ebinop Ogt
29                      (Expr (Ebinop Osub
30                        (Expr (Evar (ident_of_nat 2))
31                          (Tpointer Any (Tint I8 Unsigned )))
32                        (Expr (Evar (ident_of_nat 2))
33                          (Tpointer Any (Tint I8 Unsigned ))))
34                        (Tint I32 Signed  ))
35                      (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
36                      (Tint I32 Signed  ))
37         (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed  ))))
38         Sskip)
39       (Ssequence
40       (Sassign (Expr (Evar (ident_of_nat 2))
41                  (Tpointer Any (Tint I8 Unsigned )))
42         (Expr (Ebinop Oadd
43           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
44           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
45           (Tpointer Any (Tint I8 Unsigned ))))
46       (Ssequence
47       (Sassign (Expr (Evar (ident_of_nat 2))
48                  (Tpointer Any (Tint I8 Unsigned )))
49         (Expr (Ebinop Oadd (Expr (Econst_int (repr 0)) (Tint I32 Signed  ))
50           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))))
51           (Tpointer Any (Tint I8 Unsigned ))))
52       (Ssequence
53       (Sassign (Expr (Evar (ident_of_nat 2))
54                  (Tpointer Any (Tint I8 Unsigned )))
55         (Expr (Ebinop Osub
56           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
57           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
58           (Tpointer Any (Tint I8 Unsigned ))))
59       (Sreturn (Some expr (Expr (Ebinop Oeq
60                             (Expr (Evar (ident_of_nat 2))
61                               (Tpointer Any (Tint I8 Unsigned )))
62                             (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
63                               (Expr (Ecast (Tpointer Any Tvoid)
64                                 (Expr (Econst_int (repr 0))
65                                   (Tint I32 Unsigned)))
66                                 (Tpointer Any Tvoid)))
67                               (Tpointer Any (Tint I8 Unsigned ))))
68                             (Tint I32 Signed  )))))))))))
69     
70     
71     
72   )〉]
73  (ident_of_nat 0)
74  []
75.
76
77example exec: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 50 [ ]).
78normalize  (* you can examine the result here *)
79@refl
80qed.
Note: See TracBrowser for help on using the repository browser.