source: src/Clight/test/implicit.c.ma

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

Relax some Clight type checks to Cminor type checks to avoid array/pointer
confusion. Drop a dead function.

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