source: src/Clight/test/endptr2.c.ma @ 2771

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

Proper handling of comparison of pointers off-the-end of an object.
We might need to drop this if the proofs/back-end work is too involved.

File size: 2.7 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 I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ; 〈ident_of_nat 4, (Tpointer (Tint I32 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer (Tint I32 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer (Tint I32 Signed  ))〉 ]
7         (Ssequence
8         (Sassign (Expr (Evar (ident_of_nat 4))
9                    (Tpointer (Tint I32 Signed  )))
10           (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
11             (Tpointer (Tint I32 Signed  ))))
12         (Ssequence
13         (Sassign (Expr (Evar (ident_of_nat 5))
14                    (Tpointer (Tint I32 Signed  )))
15           (Expr (Ebinop Oadd
16             (Expr (Eaddrof
17               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
18               (Tpointer (Tint I32 Signed  )))
19             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
20             (Tpointer (Tint I32 Signed  ))))
21         (Ssequence
22         (Sassign (Expr (Evar (ident_of_nat 6))
23                    (Tpointer (Tint I32 Signed  )))
24           (Expr (Ebinop Oadd
25             (Expr (Eaddrof
26               (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
27               (Tpointer (Tint I32 Signed  )))
28             (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
29             (Tpointer (Tint I32 Signed  ))))
30         (Ssequence
31         (Sifthenelse (Expr (Ebinop Olt
32                        (Expr (Evar (ident_of_nat 4))
33                          (Tpointer (Tint I32 Signed  )))
34                        (Expr (Evar (ident_of_nat 5))
35                          (Tpointer (Tint I32 Signed  ))))
36                        (Tint I32 Signed  ))
37           (Sifthenelse (Expr (Ebinop Olt
38                          (Expr (Evar (ident_of_nat 5))
39                            (Tpointer (Tint I32 Signed  )))
40                          (Expr (Evar (ident_of_nat 6))
41                            (Tpointer (Tint I32 Signed  ))))
42                          (Tint I32 Signed  ))
43             (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 1))
44                                   (Tint I32 Signed  ))))
45             Sskip)
46           Sskip)
47         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 1))
48                               (Tint I32 Signed  ))))))))
49       
50       
51       
52     )〉]
53  (ident_of_nat 0)
54 
55.
56
57(*
58example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
59normalize  (* you can examine the result here *)
60*)
Note: See TracBrowser for help on using the repository browser.