source: src/Clight/test/addptrcharboth.c.ma @ 2569

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

Fix Clight semantics for ptr + char. (Compiler works anyway.)

File size: 8.5 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 (* arr *), XData〉, 〈[(Init_space 280) ],
6     (Tarray (Tint I8 Unsigned ) 280)〉〉][〈ident_of_nat 1 (* diffu *), CL_Internal (
7                                               mk_function (Tint I32 Signed  ) [〈ident_of_nat 2, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 4, (Tint I8 Unsigned )〉 ] []
8                                                 (Ssequence
9                                                 (Sassign (Expr (Evar (ident_of_nat 2))
10                                                            (Tpointer (Tint I8 Unsigned )))
11                                                   (Expr (Ebinop Oadd
12                                                     (Expr (Evar (ident_of_nat 2))
13                                                       (Tpointer (Tint I8 Unsigned )))
14                                                     (Expr (Evar (ident_of_nat 4))
15                                                       (Tint I8 Unsigned )))
16                                                     (Tpointer (Tint I8 Unsigned ))))
17                                                 (Sreturn (Some expr
18                                                 (Expr (Ebinop Osub
19                                                   (Expr (Evar (ident_of_nat 2))
20                                                     (Tpointer (Tint I8 Unsigned )))
21                                                   (Expr (Evar (ident_of_nat 3))
22                                                     (Tpointer (Tint I8 Unsigned ))))
23                                                   (Tint I32 Signed  )))))
24                                               
25                                               
26                                               
27                                             )〉;
28                                            〈ident_of_nat 5 (* diffs *), CL_Internal (
29                                              mk_function (Tint I32 Signed  ) [〈ident_of_nat 2, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 4, (Tint I8 Signed   )〉 ] []
30                                                (Ssequence
31                                                (Sassign (Expr (Evar (ident_of_nat 2))
32                                                           (Tpointer (Tint I8 Unsigned )))
33                                                  (Expr (Ebinop Oadd
34                                                    (Expr (Evar (ident_of_nat 2))
35                                                      (Tpointer (Tint I8 Unsigned )))
36                                                    (Expr (Evar (ident_of_nat 4))
37                                                      (Tint I8 Signed   )))
38                                                    (Tpointer (Tint I8 Unsigned ))))
39                                                (Sreturn (Some expr (Expr (Ebinop
40                                                                    Osub
41                                                                    (Expr (Evar (ident_of_nat 2))
42                                                                    (Tpointer (Tint I8 Unsigned )))
43                                                                    (Expr (Evar (ident_of_nat 3))
44                                                                    (Tpointer (Tint I8 Unsigned ))))
45                                                                    (Tint I32 Signed  )))))
46                                             
47                                             
48                                             
49                                            )〉;
50                                            〈ident_of_nat 6 (* main *), CL_Internal (
51                                              mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 7, (Tint I32 Signed  )〉 ; 〈ident_of_nat 8, (Tint I32 Signed  )〉 ]
52                                                (Ssequence
53                                                (Sassign (Expr (Evar (ident_of_nat 2))
54                                                           (Tpointer (Tint I8 Unsigned )))
55                                                  (Expr (Evar (ident_of_nat 0))
56                                                    (Tarray (Tint I8 Unsigned ) 280)))
57                                                (Ssequence
58                                                (Scall (Some expr (Expr (Evar (ident_of_nat 7))
59                                                                    (Tint I32 Signed  )))
60                                                  (Expr (Evar (ident_of_nat 1))
61                                                    (Tfunction (Tcons (Tpointer (Tint I8 Unsigned )) (Tcons (Tpointer (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I32 Signed  )))
62                                                  [(Expr (Ebinop Oadd
63                                                     (Expr (Evar (ident_of_nat 2))
64                                                       (Tpointer (Tint I8 Unsigned )))
65                                                     (Expr (Econst_int I32 (repr ? 20))
66                                                       (Tint I32 Signed  )))
67                                                     (Tpointer (Tint I8 Unsigned )));
68                                                  (Expr (Evar (ident_of_nat 2))
69                                                    (Tpointer (Tint I8 Unsigned )));
70                                                  (Expr (Ecast (Tint I8 Unsigned )
71                                                    (Expr (Econst_int I32 (repr ? 241))
72                                                      (Tint I32 Signed  )))
73                                                    (Tint I8 Unsigned ))])
74                                                (Ssequence
75                                                (Scall (Some expr (Expr (Evar (ident_of_nat 8))
76                                                                    (Tint I32 Signed  )))
77                                                  (Expr (Evar (ident_of_nat 5))
78                                                    (Tfunction (Tcons (Tpointer (Tint I8 Unsigned )) (Tcons (Tpointer (Tint I8 Unsigned )) (Tcons (Tint I8 Signed   ) Tnil))) (Tint I32 Signed  )))
79                                                  [(Expr (Ebinop Oadd
80                                                     (Expr (Evar (ident_of_nat 2))
81                                                       (Tpointer (Tint I8 Unsigned )))
82                                                     (Expr (Econst_int I32 (repr ? 20))
83                                                       (Tint I32 Signed  )))
84                                                     (Tpointer (Tint I8 Unsigned )));
85                                                  (Expr (Evar (ident_of_nat 2))
86                                                    (Tpointer (Tint I8 Unsigned )));
87                                                  (Expr (Ecast (Tint I8 Signed   )
88                                                    (Expr (Eunop Oneg
89                                                      (Expr (Econst_int I32 (repr ? 15))
90                                                        (Tint I32 Signed  )))
91                                                      (Tint I32 Signed  )))
92                                                    (Tint I8 Signed   ))])
93                                                (Sreturn (Some expr (Expr (Ebinop
94                                                                    Oadd
95                                                                    (Expr (Evar (ident_of_nat 7))
96                                                                    (Tint I32 Signed  ))
97                                                                    (Expr (Evar (ident_of_nat 8))
98                                                                    (Tint I32 Signed  )))
99                                                                    (Tint I32 Signed  )))))))
100                                             
101                                             
102                                             
103                                            )〉]
104  (ident_of_nat 6)
105 
106.
107
108(*
109example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
110normalize  (* you can examine the result here *)
111*)
Note: See TracBrowser for help on using the repository browser.