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

Last change on this file since 779 was 776, checked in by campbell, 9 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.