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

Last change on this file since 1513 was 1513, checked in by campbell, 8 years ago

Fix up Clight examples.

File size: 3.9 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 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))
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 Any (Tint I8 Unsigned )))
44           (Expr (Ebinop Oadd
45             (Expr (Evar (ident_of_nat 2))
46               (Tpointer Any (Tint I8 Unsigned )))
47             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
48             (Tpointer Any (Tint I8 Unsigned ))))
49         (Ssequence
50         (Sassign (Expr (Evar (ident_of_nat 2))
51                    (Tpointer Any (Tint I8 Unsigned )))
52           (Expr (Ebinop Oadd
53             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
54             (Expr (Evar (ident_of_nat 2))
55               (Tpointer Any (Tint I8 Unsigned ))))
56             (Tpointer Any (Tint I8 Unsigned ))))
57         (Ssequence
58         (Sassign (Expr (Evar (ident_of_nat 2))
59                    (Tpointer Any (Tint I8 Unsigned )))
60           (Expr (Ebinop Osub
61             (Expr (Evar (ident_of_nat 2))
62               (Tpointer Any (Tint I8 Unsigned )))
63             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
64             (Tpointer Any (Tint I8 Unsigned ))))
65         (Sreturn (Some expr (Expr (Ebinop Oeq
66                               (Expr (Evar (ident_of_nat 2))
67                                 (Tpointer Any (Tint I8 Unsigned )))
68                               (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
69                                 (Expr (Ecast (Tpointer Any Tvoid)
70                                   (Expr (Econst_int I8 (repr ? 0))
71                                     (Tint I8 Unsigned )))
72                                   (Tpointer Any Tvoid)))
73                                 (Tpointer Any (Tint I8 Unsigned ))))
74                               (Tint I32 Signed  )))))))))))
75       
76       
77       
78     )〉]
79  (ident_of_nat 0)
80 
81.
82
83(*
84example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
85normalize  (* you can examine the result here *)
86*)
Note: See TracBrowser for help on using the repository browser.