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

Last change on this file since 2176 was 2176, checked in by campbell, 7 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File size: 3.8 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × 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 (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer (Tint I8 Unsigned ))〉 ]
7         (Ssequence
8         (Sassign (Expr (Evar (ident_of_nat 2))
9                    (Tpointer (Tint I8 Unsigned )))
10           (Expr (Ecast (Tpointer (Tint I8 Unsigned ))
11             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
12             (Tpointer (Tint I8 Unsigned ))))
13         (Ssequence
14         (Sassign (Expr (Evar (ident_of_nat 3))
15                    (Tpointer (Tint I8 Unsigned )))
16           (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
17             (Tpointer (Tint I8 Unsigned ))))
18         (Ssequence
19         (Sifthenelse (Expr (Ebinop Oeq
20                        (Expr (Evar (ident_of_nat 2))
21                          (Tpointer (Tint I8 Unsigned )))
22                        (Expr (Evar (ident_of_nat 3))
23                          (Tpointer (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 (Tint I8 Unsigned )))
33                          (Expr (Evar (ident_of_nat 2))
34                            (Tpointer (Tint I8 Unsigned ))))
35                          (Tint I32 Signed  ))
36                        (Expr (Econst_int I32 (repr ? 0))
37                          (Tint I32 Signed  ))) (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 (Tint I8 Unsigned )))
44           (Expr (Ebinop Oadd
45             (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned )))
46             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
47             (Tpointer (Tint I8 Unsigned ))))
48         (Ssequence
49         (Sassign (Expr (Evar (ident_of_nat 2))
50                    (Tpointer (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 (Tint I8 Unsigned ))))
54             (Tpointer (Tint I8 Unsigned ))))
55         (Ssequence
56         (Sassign (Expr (Evar (ident_of_nat 2))
57                    (Tpointer (Tint I8 Unsigned )))
58           (Expr (Ebinop Osub
59             (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned )))
60             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
61             (Tpointer (Tint I8 Unsigned ))))
62         (Sreturn (Some expr (Expr (Ebinop Oeq
63                               (Expr (Evar (ident_of_nat 2))
64                                 (Tpointer (Tint I8 Unsigned )))
65                               (Expr (Ecast (Tpointer (Tint I8 Unsigned ))
66                                 (Expr (Ecast (Tpointer Tvoid)
67                                   (Expr (Econst_int I8 (repr ? 0))
68                                     (Tint I8 Unsigned ))) (Tpointer Tvoid)))
69                                 (Tpointer (Tint I8 Unsigned ))))
70                               (Tint I32 Signed  )))))))))))
71       
72       
73       
74     )〉]
75  (ident_of_nat 0)
76 
77.
78
79(*
80example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
81normalize  (* you can examine the result here *)
82*)
Note: See TracBrowser for help on using the repository browser.