Changeset 1513 for src/Clight/test
- Timestamp:
- Nov 17, 2011, 4:50:46 PM (9 years ago)
- Location:
- src/Clight/test
- Files:
-
- 6 added
- 6 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/castremoval.c.ma
r1198 r1513 2 2 include "common/Animation.ma". 3 3 4 definition myprog := mk_program 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, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 4, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ] 7 (Ssequence 8 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )) 9 (Expr (Ecast (Tint I8 Unsigned ) 10 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 11 (Tint I8 Unsigned ))) 12 (Ssequence 13 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 14 (Expr (Ecast (Tint I8 Unsigned ) 15 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 16 (Tint I8 Unsigned ))) 17 (Ssequence 18 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )) 19 (Expr (Ecast (Tint I8 Unsigned ) 20 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))) 21 (Tint I8 Unsigned ))) 22 (Ssequence 23 (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I8 Unsigned )) 24 (Expr (Ecast (Tint I8 Unsigned ) 25 (Expr (Ebinop Oadd 26 (Expr (Ecast (Tint I32 Signed ) 27 (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))) 28 (Tint I32 Signed )) 29 (Expr (Ecast (Tint I32 Signed ) 30 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 31 (Tint I32 Signed ))) (Tint I32 Signed ))) 32 (Tint I8 Unsigned ))) 33 (Ssequence 34 (Sassign (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )) 35 (Expr (Ecast (Tint I8 Unsigned ) 36 (Expr (Ebinop Oadd 4 definition 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, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 4, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ] 7 (Ssequence 8 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )) 9 (Expr (Ecast (Tint I8 Unsigned ) 10 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 11 (Tint I8 Unsigned ))) 12 (Ssequence 13 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 14 (Expr (Ecast (Tint I8 Unsigned ) 15 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 16 (Tint I8 Unsigned ))) 17 (Ssequence 18 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )) 19 (Expr (Ecast (Tint I8 Unsigned ) 20 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))) 21 (Tint I8 Unsigned ))) 22 (Ssequence 23 (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I8 Unsigned )) 24 (Expr (Ecast (Tint I8 Unsigned ) 37 25 (Expr (Ebinop Oadd 38 26 (Expr (Ecast (Tint I32 Signed ) … … 41 29 (Expr (Ecast (Tint I32 Signed ) 42 30 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 43 (Tint I32 Signed ))) (Tint I32 Signed )) 44 (Expr (Ecast (Tint I32 Signed ) 45 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) 46 (Tint I32 Signed ))) (Tint I32 Signed ))) 47 (Tint I8 Unsigned ))) 48 (Sreturn (Some expr (Expr (Ebinop Oeq 49 (Expr (Ecast (Tint I32 Signed ) 50 (Expr (Evar (ident_of_nat 5)) 51 (Tint I8 Unsigned ))) (Tint I32 Signed )) 52 (Expr (Ebinop Oadd 31 (Tint I32 Signed ))) (Tint I32 Signed ))) 32 (Tint I8 Unsigned ))) 33 (Ssequence 34 (Sassign (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )) 35 (Expr (Ecast (Tint I8 Unsigned ) 36 (Expr (Ebinop Oadd 37 (Expr (Ebinop Oadd 38 (Expr (Ecast (Tint I32 Signed ) 39 (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))) 40 (Tint I32 Signed )) 41 (Expr (Ecast (Tint I32 Signed ) 42 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 43 (Tint I32 Signed ))) (Tint I32 Signed )) 44 (Expr (Ecast (Tint I32 Signed ) 45 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) 46 (Tint I32 Signed ))) (Tint I32 Signed ))) 47 (Tint I8 Unsigned ))) 48 (Sreturn (Some expr (Expr (Ebinop Oeq 53 49 (Expr (Ecast (Tint I32 Signed ) 54 (Expr (Evar (ident_of_nat 4))50 (Expr (Evar (ident_of_nat 5)) 55 51 (Tint I8 Unsigned ))) (Tint I32 Signed )) 56 (Expr (Ecast (Tint I32 Signed ) 57 (Expr (Evar (ident_of_nat 3)) 58 (Tint I8 Unsigned ))) (Tint I32 Signed ))) 59 (Tint I32 Signed ))) (Tint I32 Signed ))))))))) 60 61 62 63 )〉] 52 (Expr (Ebinop Oadd 53 (Expr (Ecast (Tint I32 Signed ) 54 (Expr (Evar (ident_of_nat 4)) 55 (Tint I8 Unsigned ))) 56 (Tint I32 Signed )) 57 (Expr (Ecast (Tint I32 Signed ) 58 (Expr (Evar (ident_of_nat 3)) 59 (Tint I8 Unsigned ))) 60 (Tint I32 Signed ))) (Tint I32 Signed ))) 61 (Tint I32 Signed ))))))))) 62 63 64 65 )〉] 64 66 (ident_of_nat 0) 65 []67 66 68 . 67 69 68 example exec: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]). 70 (* 71 example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]). 69 72 normalize (* you can examine the result here *) 70 @refl 71 qed. 72 73 include "Clight/SimplifyCasts.ma". 74 75 example simplified: result ? (simplify_program myprog). 76 normalize 77 % 78 qed. 79 80 example exec_s: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [EVint I32 (repr I32 0)]). 81 normalize (* you can examine the result here *) 82 @refl 83 qed. 84 73 *) -
src/Clight/test/duff.c.ma
r1157 r1513 2 2 include "common/Animation.ma". 3 3 4 definition myprog := mk_program clight_fundef ((list init_data) × type) 5 [〈ident_of_nat 0 (* copy *), CL_Internal ( 6 mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed )〉 ] [〈ident_of_nat 1, (Tint I32 Signed )〉 ; 〈ident_of_nat 2, (Tint I32 Signed )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 18, (Tpointer Any (Tint I16 Signed ))〉 ] 7 (Ssequence 8 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed )) 9 (Expr (Ebinop Odiv 10 (Expr (Ebinop Oadd 11 (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed )) 12 (Expr (Econst_int I32 (repr ? 7)) (Tint I32 Signed ))) 13 (Tint I32 Signed )) 14 (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed ))) 15 (Tint I32 Signed ))) 16 (Sswitch (Expr (Ebinop Omod 17 (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed )) 18 (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed ))) 19 (Tint I32 Signed )) ( 20 (LScase I32 (repr ? 0) 21 (Slabel (ident_of_nat 22) 22 (Ssequence 23 (Ssequence 24 (Sassign (Expr (Evar (ident_of_nat 17)) 25 (Tpointer Any (Tint I16 Signed ))) 26 (Expr (Evar (ident_of_nat 19)) 27 (Tpointer Any (Tint I16 Signed )))) 28 (Sassign (Expr (Evar (ident_of_nat 19)) 29 (Tpointer Any (Tint I16 Signed ))) 4 definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type) 5 [][〈ident_of_nat 0 (* copy *), CL_Internal ( 6 mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed )〉 ] [〈ident_of_nat 1, (Tint I32 Signed )〉 ; 〈ident_of_nat 2, (Tint I32 Signed )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 18, (Tpointer Any (Tint I16 Signed ))〉 ] 7 (Ssequence 8 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed )) 9 (Expr (Ebinop Odiv 30 10 (Expr (Ebinop Oadd 31 (Expr (Evar (ident_of_nat 17)) 32 (Tpointer Any (Tint I16 Signed ))) 33 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 34 (Tpointer Any (Tint I16 Signed ))))) 35 (Ssequence 36 (Ssequence 37 (Sassign (Expr (Evar (ident_of_nat 18)) 38 (Tpointer Any (Tint I16 Signed ))) 39 (Expr (Evar (ident_of_nat 20)) 40 (Tpointer Any (Tint I16 Signed )))) 41 (Sassign (Expr (Evar (ident_of_nat 20)) 42 (Tpointer Any (Tint I16 Signed ))) 43 (Expr (Ebinop Oadd 44 (Expr (Evar (ident_of_nat 18)) 45 (Tpointer Any (Tint I16 Signed ))) 46 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 47 (Tpointer Any (Tint I16 Signed ))))) 48 (Sassign (Expr (Ederef 49 (Expr (Evar (ident_of_nat 17)) 50 (Tpointer Any (Tint I16 Signed )))) 51 (Tint I16 Signed )) 52 (Expr (Ederef 53 (Expr (Evar (ident_of_nat 18)) 54 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed )))))) 55 (LScase I32 (repr ? 7) 11 (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed )) 12 (Expr (Econst_int I32 (repr ? 7)) (Tint I32 Signed ))) 13 (Tint I32 Signed )) 14 (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed ))) 15 (Tint I32 Signed ))) 16 (Sswitch (Expr (Ebinop Omod 17 (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed )) 18 (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed ))) 19 (Tint I32 Signed )) ( 20 (LScase I32 (repr ? 0) 21 (Slabel (ident_of_nat 22) 56 22 (Ssequence 57 (Sassign (Expr (Evar (ident_of_nat 15)) 23 (Ssequence 24 (Sassign (Expr (Evar (ident_of_nat 17)) 58 25 (Tpointer Any (Tint I16 Signed ))) 59 26 (Expr (Evar (ident_of_nat 19)) 60 27 (Tpointer Any (Tint I16 Signed )))) 61 (Ssequence62 28 (Sassign (Expr (Evar (ident_of_nat 19)) 63 29 (Tpointer Any (Tint I16 Signed ))) 64 30 (Expr (Ebinop Oadd 65 (Expr (Evar (ident_of_nat 1 5))31 (Expr (Evar (ident_of_nat 17)) 66 32 (Tpointer Any (Tint I16 Signed ))) 67 33 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 68 (Tpointer Any (Tint I16 Signed )))) 34 (Tpointer Any (Tint I16 Signed ))))) 69 35 (Ssequence 70 (Sassign (Expr (Evar (ident_of_nat 16)) 36 (Ssequence 37 (Sassign (Expr (Evar (ident_of_nat 18)) 71 38 (Tpointer Any (Tint I16 Signed ))) 72 39 (Expr (Evar (ident_of_nat 20)) 73 40 (Tpointer Any (Tint I16 Signed )))) 74 (Ssequence75 41 (Sassign (Expr (Evar (ident_of_nat 20)) 76 42 (Tpointer Any (Tint I16 Signed ))) 77 43 (Expr (Ebinop Oadd 78 (Expr (Evar (ident_of_nat 1 6))44 (Expr (Evar (ident_of_nat 18)) 79 45 (Tpointer Any (Tint I16 Signed ))) 80 46 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 81 (Tpointer Any (Tint I16 Signed )))) 47 (Tpointer Any (Tint I16 Signed ))))) 82 48 (Sassign (Expr (Ederef 83 (Expr (Evar (ident_of_nat 1 5))49 (Expr (Evar (ident_of_nat 17)) 84 50 (Tpointer Any (Tint I16 Signed )))) 85 51 (Tint I16 Signed )) 86 52 (Expr (Ederef 87 (Expr (Evar (ident_of_nat 1 6))88 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed )))))) )89 (LScase I32 (repr ? 6)53 (Expr (Evar (ident_of_nat 18)) 54 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed )))))) 55 (LScase I32 (repr ? 7) 90 56 (Ssequence 91 (Sassign (Expr (Evar (ident_of_nat 1 3))57 (Sassign (Expr (Evar (ident_of_nat 15)) 92 58 (Tpointer Any (Tint I16 Signed ))) 93 59 (Expr (Evar (ident_of_nat 19)) … … 97 63 (Tpointer Any (Tint I16 Signed ))) 98 64 (Expr (Ebinop Oadd 99 (Expr (Evar (ident_of_nat 1 3))65 (Expr (Evar (ident_of_nat 15)) 100 66 (Tpointer Any (Tint I16 Signed ))) 101 67 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 102 68 (Tpointer Any (Tint I16 Signed )))) 103 69 (Ssequence 104 (Sassign (Expr (Evar (ident_of_nat 1 4))70 (Sassign (Expr (Evar (ident_of_nat 16)) 105 71 (Tpointer Any (Tint I16 Signed ))) 106 72 (Expr (Evar (ident_of_nat 20)) … … 110 76 (Tpointer Any (Tint I16 Signed ))) 111 77 (Expr (Ebinop Oadd 112 (Expr (Evar (ident_of_nat 1 4))78 (Expr (Evar (ident_of_nat 16)) 113 79 (Tpointer Any (Tint I16 Signed ))) 114 80 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 115 81 (Tpointer Any (Tint I16 Signed )))) 116 82 (Sassign (Expr (Ederef 117 (Expr (Evar (ident_of_nat 1 3))83 (Expr (Evar (ident_of_nat 15)) 118 84 (Tpointer Any (Tint I16 Signed )))) 119 85 (Tint I16 Signed )) 120 86 (Expr (Ederef 121 (Expr (Evar (ident_of_nat 1 4))87 (Expr (Evar (ident_of_nat 16)) 122 88 (Tpointer Any (Tint I16 Signed )))) 123 89 (Tint I16 Signed ))))))) 124 (LScase I32 (repr ? 5)90 (LScase I32 (repr ? 6) 125 91 (Ssequence 126 (Sassign (Expr (Evar (ident_of_nat 1 1))92 (Sassign (Expr (Evar (ident_of_nat 13)) 127 93 (Tpointer Any (Tint I16 Signed ))) 128 94 (Expr (Evar (ident_of_nat 19)) … … 132 98 (Tpointer Any (Tint I16 Signed ))) 133 99 (Expr (Ebinop Oadd 134 (Expr (Evar (ident_of_nat 1 1))100 (Expr (Evar (ident_of_nat 13)) 135 101 (Tpointer Any (Tint I16 Signed ))) 136 102 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 137 103 (Tpointer Any (Tint I16 Signed )))) 138 104 (Ssequence 139 (Sassign (Expr (Evar (ident_of_nat 1 2))105 (Sassign (Expr (Evar (ident_of_nat 14)) 140 106 (Tpointer Any (Tint I16 Signed ))) 141 107 (Expr (Evar (ident_of_nat 20)) … … 145 111 (Tpointer Any (Tint I16 Signed ))) 146 112 (Expr (Ebinop Oadd 147 (Expr (Evar (ident_of_nat 1 2))113 (Expr (Evar (ident_of_nat 14)) 148 114 (Tpointer Any (Tint I16 Signed ))) 149 115 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 150 116 (Tpointer Any (Tint I16 Signed )))) 151 117 (Sassign (Expr (Ederef 152 (Expr (Evar (ident_of_nat 1 1))118 (Expr (Evar (ident_of_nat 13)) 153 119 (Tpointer Any (Tint I16 Signed )))) 154 120 (Tint I16 Signed )) 155 121 (Expr (Ederef 156 (Expr (Evar (ident_of_nat 1 2))122 (Expr (Evar (ident_of_nat 14)) 157 123 (Tpointer Any (Tint I16 Signed )))) 158 124 (Tint I16 Signed ))))))) 159 (LScase I32 (repr ? 4)125 (LScase I32 (repr ? 5) 160 126 (Ssequence 161 (Sassign (Expr (Evar (ident_of_nat 9))127 (Sassign (Expr (Evar (ident_of_nat 11)) 162 128 (Tpointer Any (Tint I16 Signed ))) 163 129 (Expr (Evar (ident_of_nat 19)) … … 167 133 (Tpointer Any (Tint I16 Signed ))) 168 134 (Expr (Ebinop Oadd 169 (Expr (Evar (ident_of_nat 9))135 (Expr (Evar (ident_of_nat 11)) 170 136 (Tpointer Any (Tint I16 Signed ))) 171 137 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 172 138 (Tpointer Any (Tint I16 Signed )))) 173 139 (Ssequence 174 (Sassign (Expr (Evar (ident_of_nat 1 0))140 (Sassign (Expr (Evar (ident_of_nat 12)) 175 141 (Tpointer Any (Tint I16 Signed ))) 176 142 (Expr (Evar (ident_of_nat 20)) … … 180 146 (Tpointer Any (Tint I16 Signed ))) 181 147 (Expr (Ebinop Oadd 182 (Expr (Evar (ident_of_nat 1 0))148 (Expr (Evar (ident_of_nat 12)) 183 149 (Tpointer Any (Tint I16 Signed ))) 184 150 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 185 151 (Tpointer Any (Tint I16 Signed )))) 186 152 (Sassign (Expr (Ederef 187 (Expr (Evar (ident_of_nat 9))153 (Expr (Evar (ident_of_nat 11)) 188 154 (Tpointer Any (Tint I16 Signed )))) 189 155 (Tint I16 Signed )) 190 156 (Expr (Ederef 191 (Expr (Evar (ident_of_nat 1 0))157 (Expr (Evar (ident_of_nat 12)) 192 158 (Tpointer Any (Tint I16 Signed )))) 193 159 (Tint I16 Signed ))))))) 194 (LScase I32 (repr ? 3)160 (LScase I32 (repr ? 4) 195 161 (Ssequence 196 (Sassign (Expr (Evar (ident_of_nat 7))162 (Sassign (Expr (Evar (ident_of_nat 9)) 197 163 (Tpointer Any (Tint I16 Signed ))) 198 164 (Expr (Evar (ident_of_nat 19)) … … 202 168 (Tpointer Any (Tint I16 Signed ))) 203 169 (Expr (Ebinop Oadd 204 (Expr (Evar (ident_of_nat 7))170 (Expr (Evar (ident_of_nat 9)) 205 171 (Tpointer Any (Tint I16 Signed ))) 206 172 (Expr (Econst_int I32 (repr ? 1)) … … 208 174 (Tpointer Any (Tint I16 Signed )))) 209 175 (Ssequence 210 (Sassign (Expr (Evar (ident_of_nat 8))176 (Sassign (Expr (Evar (ident_of_nat 10)) 211 177 (Tpointer Any (Tint I16 Signed ))) 212 178 (Expr (Evar (ident_of_nat 20)) … … 216 182 (Tpointer Any (Tint I16 Signed ))) 217 183 (Expr (Ebinop Oadd 218 (Expr (Evar (ident_of_nat 8))184 (Expr (Evar (ident_of_nat 10)) 219 185 (Tpointer Any (Tint I16 Signed ))) 220 186 (Expr (Econst_int I32 (repr ? 1)) … … 222 188 (Tpointer Any (Tint I16 Signed )))) 223 189 (Sassign (Expr (Ederef 224 (Expr (Evar (ident_of_nat 7))190 (Expr (Evar (ident_of_nat 9)) 225 191 (Tpointer Any (Tint I16 Signed )))) 226 192 (Tint I16 Signed )) 227 193 (Expr (Ederef 228 (Expr (Evar (ident_of_nat 8))194 (Expr (Evar (ident_of_nat 10)) 229 195 (Tpointer Any (Tint I16 Signed )))) 230 196 (Tint I16 Signed ))))))) 231 (LScase I32 (repr ? 2)197 (LScase I32 (repr ? 3) 232 198 (Ssequence 233 (Sassign (Expr (Evar (ident_of_nat 5))199 (Sassign (Expr (Evar (ident_of_nat 7)) 234 200 (Tpointer Any (Tint I16 Signed ))) 235 201 (Expr (Evar (ident_of_nat 19)) … … 239 205 (Tpointer Any (Tint I16 Signed ))) 240 206 (Expr (Ebinop Oadd 241 (Expr (Evar (ident_of_nat 5))207 (Expr (Evar (ident_of_nat 7)) 242 208 (Tpointer Any (Tint I16 Signed ))) 243 209 (Expr (Econst_int I32 (repr ? 1)) … … 245 211 (Tpointer Any (Tint I16 Signed )))) 246 212 (Ssequence 247 (Sassign (Expr (Evar (ident_of_nat 6))213 (Sassign (Expr (Evar (ident_of_nat 8)) 248 214 (Tpointer Any (Tint I16 Signed ))) 249 215 (Expr (Evar (ident_of_nat 20)) … … 253 219 (Tpointer Any (Tint I16 Signed ))) 254 220 (Expr (Ebinop Oadd 255 (Expr (Evar (ident_of_nat 6))221 (Expr (Evar (ident_of_nat 8)) 256 222 (Tpointer Any (Tint I16 Signed ))) 257 223 (Expr (Econst_int I32 (repr ? 1)) … … 259 225 (Tpointer Any (Tint I16 Signed )))) 260 226 (Sassign (Expr (Ederef 261 (Expr (Evar (ident_of_nat 5))227 (Expr (Evar (ident_of_nat 7)) 262 228 (Tpointer Any (Tint I16 Signed )))) 263 229 (Tint I16 Signed )) 264 230 (Expr (Ederef 265 (Expr (Evar (ident_of_nat 6))231 (Expr (Evar (ident_of_nat 8)) 266 232 (Tpointer Any (Tint I16 Signed )))) 267 233 (Tint I16 Signed ))))))) 268 (LScase I32 (repr ? 1)234 (LScase I32 (repr ? 2) 269 235 (Ssequence 270 (Sassign (Expr (Evar (ident_of_nat 3))236 (Sassign (Expr (Evar (ident_of_nat 5)) 271 237 (Tpointer Any (Tint I16 Signed ))) 272 238 (Expr (Evar (ident_of_nat 19)) … … 276 242 (Tpointer Any (Tint I16 Signed ))) 277 243 (Expr (Ebinop Oadd 278 (Expr (Evar (ident_of_nat 3))244 (Expr (Evar (ident_of_nat 5)) 279 245 (Tpointer Any (Tint I16 Signed ))) 280 246 (Expr (Econst_int I32 (repr ? 1)) … … 282 248 (Tpointer Any (Tint I16 Signed )))) 283 249 (Ssequence 284 (Sassign (Expr (Evar (ident_of_nat 4))250 (Sassign (Expr (Evar (ident_of_nat 6)) 285 251 (Tpointer Any (Tint I16 Signed ))) 286 252 (Expr (Evar (ident_of_nat 20)) … … 290 256 (Tpointer Any (Tint I16 Signed ))) 291 257 (Expr (Ebinop Oadd 292 (Expr (Evar (ident_of_nat 4))258 (Expr (Evar (ident_of_nat 6)) 293 259 (Tpointer Any (Tint I16 Signed ))) 294 260 (Expr (Econst_int I32 (repr ? 1)) 295 261 (Tint I32 Signed ))) 296 262 (Tpointer Any (Tint I16 Signed )))) 297 (Ssequence298 263 (Sassign (Expr (Ederef 299 (Expr (Evar (ident_of_nat 3))264 (Expr (Evar (ident_of_nat 5)) 300 265 (Tpointer Any (Tint I16 Signed )))) 301 266 (Tint I16 Signed )) 302 267 (Expr (Ederef 303 (Expr (Evar (ident_of_nat 4))268 (Expr (Evar (ident_of_nat 6)) 304 269 (Tpointer Any (Tint I16 Signed )))) 305 (Tint I16 Signed ))) 306 (Ssequence 307 (Sassign (Expr (Evar (ident_of_nat 2)) 308 (Tint I32 Signed )) 309 (Expr (Ebinop Osub 310 (Expr (Evar (ident_of_nat 1)) 311 (Tint I32 Signed )) 312 (Expr (Econst_int I32 (repr ? 1)) 313 (Tint I32 Signed ))) (Tint I32 Signed ))) 314 (Ssequence 315 (Sassign (Expr (Evar (ident_of_nat 1)) 316 (Tint I32 Signed )) 317 (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 318 (Sifthenelse (Expr (Ebinop Ogt 319 (Expr (Evar (ident_of_nat 2)) 270 (Tint I16 Signed ))))))) 271 (LScase I32 (repr ? 1) 272 (Ssequence 273 (Sassign (Expr (Evar (ident_of_nat 3)) 274 (Tpointer Any (Tint I16 Signed ))) 275 (Expr (Evar (ident_of_nat 19)) 276 (Tpointer Any (Tint I16 Signed )))) 277 (Ssequence 278 (Sassign (Expr (Evar (ident_of_nat 19)) 279 (Tpointer Any (Tint I16 Signed ))) 280 (Expr (Ebinop Oadd 281 (Expr (Evar (ident_of_nat 3)) 282 (Tpointer Any (Tint I16 Signed ))) 283 (Expr (Econst_int I32 (repr ? 1)) 284 (Tint I32 Signed ))) 285 (Tpointer Any (Tint I16 Signed )))) 286 (Ssequence 287 (Sassign (Expr (Evar (ident_of_nat 4)) 288 (Tpointer Any (Tint I16 Signed ))) 289 (Expr (Evar (ident_of_nat 20)) 290 (Tpointer Any (Tint I16 Signed )))) 291 (Ssequence 292 (Sassign (Expr (Evar (ident_of_nat 20)) 293 (Tpointer Any (Tint I16 Signed ))) 294 (Expr (Ebinop Oadd 295 (Expr (Evar (ident_of_nat 4)) 296 (Tpointer Any (Tint I16 Signed ))) 297 (Expr (Econst_int I32 (repr ? 1)) 298 (Tint I32 Signed ))) 299 (Tpointer Any (Tint I16 Signed )))) 300 (Ssequence 301 (Sassign (Expr (Ederef 302 (Expr (Evar (ident_of_nat 3)) 303 (Tpointer Any (Tint I16 Signed )))) 304 (Tint I16 Signed )) 305 (Expr (Ederef 306 (Expr (Evar (ident_of_nat 4)) 307 (Tpointer Any (Tint I16 Signed )))) 308 (Tint I16 Signed ))) 309 (Ssequence 310 (Sassign (Expr (Evar (ident_of_nat 2)) 311 (Tint I32 Signed )) 312 (Expr (Ebinop Osub 313 (Expr (Evar (ident_of_nat 1)) 314 (Tint I32 Signed )) 315 (Expr (Econst_int I32 (repr ? 1)) 316 (Tint I32 Signed ))) (Tint I32 Signed ))) 317 (Ssequence 318 (Sassign (Expr (Evar (ident_of_nat 1)) 319 (Tint I32 Signed )) 320 (Expr (Evar (ident_of_nat 2)) 321 (Tint I32 Signed ))) 322 (Sifthenelse (Expr (Ebinop Ogt 323 (Expr (Evar (ident_of_nat 2)) 324 (Tint I32 Signed )) 325 (Expr (Econst_int I32 (repr ? 0)) 326 (Tint I32 Signed ))) 320 327 (Tint I32 Signed )) 321 (Expr (Econst_int I32 (repr ? 0)) 322 (Tint I32 Signed ))) 323 (Tint I32 Signed )) 324 (Sgoto (ident_of_nat 22)) 325 Sskip)))))))) 326 (LSdefault 327 Sskip))))))))) 328 ))) 329 330 331 332 )〉; 333 〈ident_of_nat 23 (* main *), CL_Internal ( 334 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 24, (Tarray Any (Tint I16 Signed ) 3)〉 ; 〈ident_of_nat 25, (Tarray Any (Tint I16 Signed ) 3)〉 ] 335 (Ssequence 336 (Sassign (Expr (Ederef 337 (Expr (Ebinop Oadd 338 (Expr (Evar (ident_of_nat 24)) 339 (Tarray Any (Tint I16 Signed ) 3)) 340 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 341 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed )) 342 (Expr (Ecast (Tint I16 Signed ) 343 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 344 (Tint I16 Signed ))) 345 (Ssequence 346 (Sassign (Expr (Ederef 347 (Expr (Ebinop Oadd 348 (Expr (Evar (ident_of_nat 24)) 349 (Tarray Any (Tint I16 Signed ) 3)) 350 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 351 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed )) 352 (Expr (Ecast (Tint I16 Signed ) 353 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 354 (Tint I16 Signed ))) 355 (Ssequence 356 (Sassign (Expr (Ederef 357 (Expr (Ebinop Oadd 358 (Expr (Evar (ident_of_nat 24)) 359 (Tarray Any (Tint I16 Signed ) 3)) 360 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 361 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed )) 362 (Expr (Ecast (Tint I16 Signed ) 363 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))) 364 (Tint I16 Signed ))) 365 (Ssequence 366 (Scall (None expr) (Expr (Evar (ident_of_nat 0)) 367 (Tfunction (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tint I32 Signed ) Tnil))) Tvoid)) 368 [(Expr (Evar (ident_of_nat 25)) (Tarray Any (Tint I16 Signed ) 3)); 369 (Expr (Evar (ident_of_nat 24)) (Tarray Any (Tint I16 Signed ) 3)); 370 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))]) 371 (Sreturn (Some expr (Expr (Ebinop Oadd 372 (Expr (Ebinop Oadd 328 (Sgoto (ident_of_nat 22)) 329 Sskip)))))))) 330 (LSdefault 331 Sskip))))))))) 332 ))) 333 334 335 336 )〉; 337 〈ident_of_nat 23 (* main *), CL_Internal ( 338 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 24, (Tarray Any (Tint I16 Signed ) 3)〉 ; 〈ident_of_nat 25, (Tarray Any (Tint I16 Signed ) 3)〉 ] 339 (Ssequence 340 (Sassign (Expr (Ederef 341 (Expr (Ebinop Oadd 342 (Expr (Evar (ident_of_nat 24)) 343 (Tarray Any (Tint I16 Signed ) 3)) 344 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 345 (Tpointer Any (Tint I16 Signed )))) 346 (Tint I16 Signed )) 347 (Expr (Ecast (Tint I16 Signed ) 348 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 349 (Tint I16 Signed ))) 350 (Ssequence 351 (Sassign (Expr (Ederef 352 (Expr (Ebinop Oadd 353 (Expr (Evar (ident_of_nat 24)) 354 (Tarray Any (Tint I16 Signed ) 3)) 355 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 356 (Tpointer Any (Tint I16 Signed )))) 357 (Tint I16 Signed )) 358 (Expr (Ecast (Tint I16 Signed ) 359 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 360 (Tint I16 Signed ))) 361 (Ssequence 362 (Sassign (Expr (Ederef 363 (Expr (Ebinop Oadd 364 (Expr (Evar (ident_of_nat 24)) 365 (Tarray Any (Tint I16 Signed ) 3)) 366 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 367 (Tpointer Any (Tint I16 Signed )))) 368 (Tint I16 Signed )) 369 (Expr (Ecast (Tint I16 Signed ) 370 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))) 371 (Tint I16 Signed ))) 372 (Ssequence 373 (Scall (None expr) (Expr (Evar (ident_of_nat 0)) 374 (Tfunction (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tint I32 Signed ) Tnil))) Tvoid)) 375 [(Expr (Evar (ident_of_nat 25)) (Tarray Any (Tint I16 Signed ) 3)); 376 (Expr (Evar (ident_of_nat 24)) (Tarray Any (Tint I16 Signed ) 3)); 377 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))]) 378 (Sreturn (Some expr (Expr (Ebinop Oadd 379 (Expr (Ebinop Oadd 380 (Expr (Ecast (Tint I32 Signed ) 381 (Expr (Ederef 382 (Expr (Ebinop Oadd 383 (Expr (Evar (ident_of_nat 25)) 384 (Tarray Any (Tint I16 Signed ) 3)) 385 (Expr (Econst_int I32 (repr ? 0)) 386 (Tint I32 Signed ))) 387 (Tpointer Any (Tint I16 Signed )))) 388 (Tint I16 Signed ))) 389 (Tint I32 Signed )) 390 (Expr (Ecast (Tint I32 Signed ) 391 (Expr (Ederef 392 (Expr (Ebinop Oadd 393 (Expr (Evar (ident_of_nat 25)) 394 (Tarray Any (Tint I16 Signed ) 3)) 395 (Expr (Econst_int I32 (repr ? 1)) 396 (Tint I32 Signed ))) 397 (Tpointer Any (Tint I16 Signed )))) 398 (Tint I16 Signed ))) 399 (Tint I32 Signed ))) (Tint I32 Signed )) 373 400 (Expr (Ecast (Tint I32 Signed ) 374 401 (Expr (Ederef … … 376 403 (Expr (Evar (ident_of_nat 25)) 377 404 (Tarray Any (Tint I16 Signed ) 3)) 378 (Expr (Econst_int I32 (repr ? 0)) 379 (Tint I32 Signed ))) 380 (Tpointer Any (Tint I16 Signed )))) 381 (Tint I16 Signed ))) (Tint I32 Signed )) 382 (Expr (Ecast (Tint I32 Signed ) 383 (Expr (Ederef 384 (Expr (Ebinop Oadd 385 (Expr (Evar (ident_of_nat 25)) 386 (Tarray Any (Tint I16 Signed ) 3)) 387 (Expr (Econst_int I32 (repr ? 1)) 405 (Expr (Econst_int I32 (repr ? 2)) 388 406 (Tint I32 Signed ))) 389 407 (Tpointer Any (Tint I16 Signed )))) 390 408 (Tint I16 Signed ))) (Tint I32 Signed ))) 391 (Tint I32 Signed )) 392 (Expr (Ecast (Tint I32 Signed ) 393 (Expr (Ederef 394 (Expr (Ebinop Oadd 395 (Expr (Evar (ident_of_nat 25)) 396 (Tarray Any (Tint I16 Signed ) 3)) 397 (Expr (Econst_int I32 (repr ? 2)) 398 (Tint I32 Signed ))) 399 (Tpointer Any (Tint I16 Signed )))) 400 (Tint I16 Signed ))) (Tint I32 Signed ))) 401 (Tint I32 Signed )))))))) 402 403 404 405 )〉] 409 (Tint I32 Signed )))))))) 410 411 412 413 )〉] 406 414 (ident_of_nat 23) 407 []415 408 416 . 409 417 410 example exec: finishes_with (repr I32 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]). 418 (* 419 example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]). 411 420 normalize (* you can examine the result here *) 412 @refl 413 qed. 421 *) -
src/Clight/test/factorial.c.ma
r1157 r1513 2 2 include "common/Animation.ma". 3 3 4 definition myprog := mk_program clight_fundef ((list init_data) × type) 5 [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed )〉; 6 〈ident_of_nat 1 (* main *), CL_Internal ( 7 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 2, (Tint I32 Signed )〉 ; 〈ident_of_nat 3, (Tint I32 Signed )〉 ; 〈ident_of_nat 4, (Tint I32 Signed )〉 ] 8 (Ssequence 9 (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 10 (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed ))) 11 []) 12 (Ssequence 13 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) 14 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 15 (Ssequence 16 (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 17 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 18 (Expr (Ebinop Ole (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 19 (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 20 (Tint I32 Signed )) 21 (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 22 (Expr (Ebinop Oadd 4 definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type) 5 [][〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed )〉; 6 〈ident_of_nat 1 (* main *), CL_Internal ( 7 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 2, (Tint I32 Signed )〉 ; 〈ident_of_nat 3, (Tint I32 Signed )〉 ; 〈ident_of_nat 4, (Tint I32 Signed )〉 ] 8 (Ssequence 9 (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 10 (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed ))) 11 []) 12 (Ssequence 13 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) 14 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 15 (Ssequence 16 (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 17 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 18 (Expr (Ebinop Ole 23 19 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 24 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 25 (Tint I32 Signed ))) 26 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) 27 (Expr (Ebinop Omul 28 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) 29 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed ))) 30 (Tint I32 Signed ))) 31 ) 32 (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed ))))))) 33 34 35 36 )〉] 20 (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 21 (Tint I32 Signed )) 22 (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 23 (Expr (Ebinop Oadd 24 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 25 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 26 (Tint I32 Signed ))) 27 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) 28 (Expr (Ebinop Omul 29 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) 30 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed ))) 31 (Tint I32 Signed ))) 32 ) 33 (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) 34 (Tint I32 Signed ))))))) 35 36 37 38 )〉] 37 39 (ident_of_nat 1) 38 []40 39 41 . 40 42 41 example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]). 43 (* 44 example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]). 42 45 normalize (* you can examine the result here *) 43 @refl 44 qed. 46 *) -
src/Clight/test/insertsort.c.ma
r1139 r1513 5 5 generate Init_null at the moment. *) 6 6 7 definition myprog := mk_program clight_fundef ((list init_data) × type) 8 [〈ident_of_nat 0 (* insert *), CL_Internal ( 9 mk_function Tvoid [〈ident_of_nat 2, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 1, (Tint I32 Signed )〉 ] 7 definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type) 8 [〈〈ident_of_nat 3 (* l6 *), Any〉, 9 〈[(Init_int8 (repr I8 69)) ; (Init_space 3) ; 10 (Init_null Any) ], 11 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉; 12 〈〈ident_of_nat 4 (* l5 *), Any〉, 13 〈[(Init_int8 (repr I8 36)) ; (Init_space 3) ; 14 (Init_addrof Any (ident_of_nat 3) 0)], 15 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉; 16 〈〈ident_of_nat 5 (* l4 *), Any〉, 17 〈[(Init_int8 (repr I8 136)) ; (Init_space 3) ; 18 (Init_addrof Any (ident_of_nat 4) 0)], 19 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉; 20 〈〈ident_of_nat 6 (* l3 *), Any〉, 21 〈[(Init_int8 (repr I8 105)) ; (Init_space 3) ; 22 (Init_addrof Any (ident_of_nat 5) 0)], 23 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉; 24 〈〈ident_of_nat 7 (* l2 *), Any〉, 25 〈[(Init_int8 (repr I8 234)) ; (Init_space 3) ; 26 (Init_addrof Any (ident_of_nat 6) 0)], 27 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉; 28 〈〈ident_of_nat 8 (* l1 *), Any〉, 29 〈[(Init_int8 (repr I8 240)) ; (Init_space 3) ; 30 (Init_addrof Any (ident_of_nat 7) 0)], 31 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉; 32 〈〈ident_of_nat 9 (* l0 *), Any〉, 33 〈[(Init_int8 (repr I8 102)) ; (Init_space 3) ; 34 (Init_addrof Any (ident_of_nat 8) 0)], 35 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉] 36 [〈ident_of_nat 10 (* insert *), CL_Internal ( 37 mk_function Tvoid [〈ident_of_nat 12, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 11, (Tint I32 Signed )〉 ] 10 38 (Ssequence 11 39 (Sifthenelse (Expr (Ebinop Oeq 12 40 (Expr (Ederef 13 (Expr (Evar (ident_of_nat 6))14 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))15 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))16 (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))41 (Expr (Evar (ident_of_nat 13)) 42 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))) 43 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 44 (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) 17 45 (Expr (Ecast (Tpointer Any Tvoid) 18 46 (Expr (Econst_int I8 (repr ? 0)) 19 47 (Tint I8 Unsigned ))) (Tpointer Any Tvoid))) 20 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))48 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 21 49 (Tint I32 Signed )) 22 (Sassign (Expr (Evar (ident_of_nat 1 )) (Tint I32 Signed ))50 (Sassign (Expr (Evar (ident_of_nat 11)) (Tint I32 Signed )) 23 51 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 24 (Sassign (Expr (Evar (ident_of_nat 1 )) (Tint I32 Signed ))52 (Sassign (Expr (Evar (ident_of_nat 11)) (Tint I32 Signed )) 25 53 (Expr (Ebinop One 26 54 (Expr (Ebinop Oge … … 28 56 (Expr (Efield (Expr (Ederef 29 57 (Expr (Ederef 30 (Expr (Evar (ident_of_nat 6))31 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))32 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))33 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))58 (Expr (Evar (ident_of_nat 13)) 59 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))) 60 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 61 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1)) 34 62 (Tint I8 Unsigned ))) (Tint I32 Signed )) 35 63 (Expr (Ecast (Tint I32 Signed ) 36 64 (Expr (Efield (Expr (Ederef 37 (Expr (Evar (ident_of_nat 2))38 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))39 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))65 (Expr (Evar (ident_of_nat 12)) 66 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 67 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1)) 40 68 (Tint I8 Unsigned ))) (Tint I32 Signed ))) 41 69 (Tint I32 Signed )) 42 70 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 43 71 (Tint I32 Signed )))) 44 (Sifthenelse (Expr (Evar (ident_of_nat 1 )) (Tint I32 Signed ))72 (Sifthenelse (Expr (Evar (ident_of_nat 11)) (Tint I32 Signed )) 45 73 (Ssequence 46 74 (Sassign (Expr (Efield (Expr (Ederef 47 (Expr (Evar (ident_of_nat 2))48 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))49 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))50 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))75 (Expr (Evar (ident_of_nat 12)) 76 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 77 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2)) 78 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 51 79 (Expr (Ederef 52 (Expr (Evar (ident_of_nat 6))53 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))54 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))80 (Expr (Evar (ident_of_nat 13)) 81 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))) 82 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 55 83 (Sassign (Expr (Ederef 56 (Expr (Evar (ident_of_nat 6))57 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))58 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))59 (Expr (Evar (ident_of_nat 2))60 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))61 (Scall (None expr) (Expr (Evar (ident_of_nat 0))62 (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid))63 [(Expr (Evar (ident_of_nat 2))64 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))));84 (Expr (Evar (ident_of_nat 13)) 85 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))) 86 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 87 (Expr (Evar (ident_of_nat 12)) 88 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))) 89 (Scall (None expr) (Expr (Evar (ident_of_nat 10)) 90 (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid)) 91 [(Expr (Evar (ident_of_nat 12)) 92 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))); 65 93 (Expr (Eaddrof 66 94 (Expr (Efield (Expr (Ederef 67 95 (Expr (Ederef 68 (Expr (Evar (ident_of_nat 6))69 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))70 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))71 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))72 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))73 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))])))96 (Expr (Evar (ident_of_nat 13)) 97 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))) 98 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 99 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2)) 100 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 101 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))]))) 74 102 75 103 76 104 77 105 )〉; 78 〈ident_of_nat 7(* sort *), CL_Internal (79 mk_function Tvoid [〈ident_of_nat 1 0, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 8, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ]80 (Ssequence 81 (Sassign (Expr (Evar (ident_of_nat 5))82 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))106 〈ident_of_nat 14 (* sort *), CL_Internal ( 107 mk_function Tvoid [〈ident_of_nat 17, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 15, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 2, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ] 108 (Ssequence 109 (Sassign (Expr (Evar (ident_of_nat 2)) 110 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 83 111 (Expr (Ederef 84 (Expr (Evar (ident_of_nat 1 0))85 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))86 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))87 (Ssequence 88 (Sassign (Expr (Evar (ident_of_nat 9))89 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))90 (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))112 (Expr (Evar (ident_of_nat 17)) 113 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))) 114 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 115 (Ssequence 116 (Sassign (Expr (Evar (ident_of_nat 16)) 117 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 118 (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) 91 119 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 92 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))93 (Ssequence 94 (Swhile (Expr (Evar (ident_of_nat 5))95 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))120 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 121 (Ssequence 122 (Swhile (Expr (Evar (ident_of_nat 2)) 123 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 96 124 (Ssequence 97 (Sassign (Expr (Evar (ident_of_nat 8))98 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))99 (Expr (Evar (ident_of_nat 5))100 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))125 (Sassign (Expr (Evar (ident_of_nat 15)) 126 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 127 (Expr (Evar (ident_of_nat 2)) 128 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 101 129 (Ssequence 102 (Sassign (Expr (Evar (ident_of_nat 5))103 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))130 (Sassign (Expr (Evar (ident_of_nat 2)) 131 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 104 132 (Expr (Efield (Expr (Ederef 105 (Expr (Evar (ident_of_nat 5))106 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))107 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))108 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))109 (Scall (None expr) (Expr (Evar (ident_of_nat 0))110 (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid))111 [(Expr (Evar (ident_of_nat 8))112 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))));133 (Expr (Evar (ident_of_nat 2)) 134 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 135 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2)) 136 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 137 (Scall (None expr) (Expr (Evar (ident_of_nat 10)) 138 (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid)) 139 [(Expr (Evar (ident_of_nat 15)) 140 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))); 113 141 (Expr (Eaddrof 114 (Expr (Evar (ident_of_nat 9))115 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))116 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))]))))142 (Expr (Evar (ident_of_nat 16)) 143 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 144 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))])))) 117 145 (Sassign (Expr (Ederef 118 (Expr (Evar (ident_of_nat 1 0))119 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))120 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))121 (Expr (Evar (ident_of_nat 9))122 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))))146 (Expr (Evar (ident_of_nat 17)) 147 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))) 148 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 149 (Expr (Evar (ident_of_nat 16)) 150 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))))) 123 151 124 152 125 153 126 154 )〉; 127 〈ident_of_nat 1 1 (* out *), CL_External (ident_of_nat 11) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;128 〈ident_of_nat 1 2(* main *), CL_Internal (129 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 13, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ]130 (Ssequence 131 (Sassign (Expr (Evar (ident_of_nat 13))132 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))155 〈ident_of_nat 18 (* out *), CL_External (ident_of_nat 18) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉; 156 〈ident_of_nat 19 (* main *), CL_Internal ( 157 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 20, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ] 158 (Ssequence 159 (Sassign (Expr (Evar (ident_of_nat 20)) 160 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 133 161 (Expr (Eaddrof 134 (Expr (Evar (ident_of_nat 14))135 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))136 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))137 (Ssequence 138 (Scall (None expr) (Expr (Evar (ident_of_nat 7))139 (Tfunction (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))) Tnil) Tvoid))162 (Expr (Evar (ident_of_nat 9)) 163 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 164 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 165 (Ssequence 166 (Scall (None expr) (Expr (Evar (ident_of_nat 14)) 167 (Tfunction (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil) Tvoid)) 140 168 [(Expr (Eaddrof 141 (Expr (Evar (ident_of_nat 13))142 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))143 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))])144 (Ssequence 145 (Swhile (Expr (Evar (ident_of_nat 13))146 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))169 (Expr (Evar (ident_of_nat 20)) 170 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 171 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))]) 172 (Ssequence 173 (Swhile (Expr (Evar (ident_of_nat 20)) 174 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 147 175 (Ssequence 148 (Scall (None expr) (Expr (Evar (ident_of_nat 1 1))176 (Scall (None expr) (Expr (Evar (ident_of_nat 18)) 149 177 (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) Tvoid)) 150 178 [(Expr (Efield (Expr (Ederef 151 (Expr (Evar (ident_of_nat 13))152 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))153 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))179 (Expr (Evar (ident_of_nat 20)) 180 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 181 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1)) 154 182 (Tint I8 Unsigned ))]) 155 (Sassign (Expr (Evar (ident_of_nat 13))156 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))183 (Sassign (Expr (Evar (ident_of_nat 20)) 184 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) 157 185 (Expr (Efield (Expr (Ederef 158 (Expr (Evar (ident_of_nat 13))159 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))160 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))161 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))))186 (Expr (Evar (ident_of_nat 20)) 187 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))) 188 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2)) 189 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))) 162 190 (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0)) 163 191 (Tint I32 Signed ))))))) … … 166 194 167 195 )〉] 168 (ident_of_nat 12) 169 [〈〈ident_of_nat 15 (* l6 *), Any〉, 170 〈[(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ], 171 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉; 172 〈〈ident_of_nat 16 (* l5 *), Any〉, 173 〈[(Init_int8 (repr I8 36)) ; (Init_space 3) ; 174 (Init_addrof Any (ident_of_nat 15) 0)], 175 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉; 176 〈〈ident_of_nat 17 (* l4 *), Any〉, 177 〈[(Init_int8 (repr I8 136)) ; (Init_space 3) ; 178 (Init_addrof Any (ident_of_nat 16) 0)], 179 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉; 180 〈〈ident_of_nat 18 (* l3 *), Any〉, 181 〈[(Init_int8 (repr I8 105)) ; (Init_space 3) ; 182 (Init_addrof Any (ident_of_nat 17) 0)], 183 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉; 184 〈〈ident_of_nat 19 (* l2 *), Any〉, 185 〈[(Init_int8 (repr I8 234)) ; (Init_space 3) ; 186 (Init_addrof Any (ident_of_nat 18) 0)], 187 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉; 188 〈〈ident_of_nat 20 (* l1 *), Any〉, 189 〈[(Init_int8 (repr I8 240)) ; (Init_space 3) ; 190 (Init_addrof Any (ident_of_nat 19) 0)], 191 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉; 192 〈〈ident_of_nat 14 (* l0 *), Any〉, 193 〈[(Init_int8 (repr I8 102)) ; (Init_space 3) ; 194 (Init_addrof Any (ident_of_nat 20) 0)], 195 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉] 196 (ident_of_nat 19) 197 196 198 . 197 199 198 example exec: 199 (do s ← exec_up_to clight_fullexec myprog 1000 200 [EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0)]; 201 match s with [ finished t _ _ ⇒ OK ? t | _ ⇒ Error ? [ ] ]) = OK ? 202 [EVextcall (ident_of_nat 11) [EVint I8 (repr ? 36)] (EVint I32 (repr ? 0)); 203 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 69)] (EVint I32 (repr ? 0)); 204 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 102)] (EVint I32 (repr ? 0)); 205 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 105)] (EVint I32 (repr ? 0)); 206 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 136)] (EVint I32 (repr ? 0)); 207 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 234)] (EVint I32 (repr ? 0)); 208 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 240)] (EVint I32 (repr ? 0))] 209 . 200 (* 201 example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]). 210 202 normalize (* you can examine the result here *) 211 @refl 212 qed. 213 214 include "Clight/label.ma". 215 216 example labelled_exec: 217 (do p ← clight_label myprog; 218 do s ← exec_up_to clight_fullexec p 1000 219 [EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0)]; 220 match s with [ finished t _ _ ⇒ OK ? (remove_costs t) | _ ⇒ Error ? [ ] ]) = OK ? 221 [EVextcall (ident_of_nat 11) [EVint I8 (repr ? 36)] (EVint I32 (repr ? 0)); 222 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 69)] (EVint I32 (repr ? 0)); 223 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 102)] (EVint I32 (repr ? 0)); 224 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 105)] (EVint I32 (repr ? 0)); 225 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 136)] (EVint I32 (repr ? 0)); 226 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 234)] (EVint I32 (repr ? 0)); 227 EVextcall (ident_of_nat 11) [EVint I8 (repr ? 240)] (EVint I32 (repr ? 0))] 228 . 229 normalize (* you can examine the result here *) 230 @refl 231 qed. 203 *) -
src/Clight/test/null-op.c.ma
r965 r1513 2 2 include "common/Animation.ma". 3 3 4 definition myprog := mk_program clight_fundef 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 4 definition 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 31 20 (Expr (Evar (ident_of_nat 2)) 32 21 (Tpointer Any (Tint I8 Unsigned ))) 33 (Expr (Evar (ident_of_nat 2))22 (Expr (Evar (ident_of_nat 3)) 34 23 (Tpointer Any (Tint I8 Unsigned )))) 35 24 (Tint I32 Signed )) 36 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 37 (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)) (Tpointer Any (Tint I8 Unsigned ))) 46 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 47 (Tpointer Any (Tint I8 Unsigned )))) 48 (Ssequence 49 (Sassign (Expr (Evar (ident_of_nat 2)) 50 (Tpointer Any (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 Any (Tint I8 Unsigned )))) 54 (Tpointer Any (Tint I8 Unsigned )))) 55 (Ssequence 56 (Sassign (Expr (Evar (ident_of_nat 2)) 57 (Tpointer Any (Tint I8 Unsigned ))) 58 (Expr (Ebinop Osub 59 (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))) 60 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 61 (Tpointer Any (Tint I8 Unsigned )))) 62 (Sreturn (Some expr (Expr (Ebinop Oeq 63 (Expr (Evar (ident_of_nat 2)) 64 (Tpointer Any (Tint I8 Unsigned ))) 65 (Expr (Ecast (Tpointer Any (Tint I8 Unsigned )) 66 (Expr (Ecast (Tpointer Any Tvoid) 67 (Expr (Econst_int I8 (repr ? 0)) 68 (Tint I8 Unsigned ))) 69 (Tpointer Any Tvoid))) 70 (Tpointer Any (Tint I8 Unsigned )))) 71 (Tint I32 Signed ))))))))))) 72 73 74 75 )〉] 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 )〉] 76 79 (ident_of_nat 0) 77 []80 78 81 . 79 82 80 example exec: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 50 [ ]). 83 (* 84 example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]). 81 85 normalize (* you can examine the result here *) 82 @refl 83 qed. 86 *) -
src/Clight/test/switcher.c.ma
r978 r1513 2 2 include "common/Animation.ma". 3 3 4 definition myprog := mk_program clight_fundef type 5 [〈ident_of_nat 0 (* get *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed )〉; 6 〈ident_of_nat 1 (* main *), CL_Internal ( 7 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I32 Signed )〉 ] 8 (Ssequence 9 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 10 (Expr (Ecast (Tint I8 Unsigned ) 11 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 12 (Tint I8 Unsigned ))) 13 (Ssequence 14 (Ssequence 15 (Scall (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed ))) 16 (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed ))) 17 []) 18 (Sswitch (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) ( 19 (LScase I32 (repr ? 1) 20 Sbreak 21 (LScase I32 (repr ? 3) 22 (Ssequence 23 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 24 (Expr (Ecast (Tint I8 Unsigned ) 25 (Expr (Ebinop Oadd 26 (Expr (Ecast (Tint I32 Signed ) 27 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 28 (Tint I32 Signed )) 29 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 30 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 31 Sbreak) 32 (LScase I32 (repr ? 5) 4 definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type) 5 [][〈ident_of_nat 0 (* get *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed )〉; 6 〈ident_of_nat 1 (* main *), CL_Internal ( 7 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I32 Signed )〉 ] 8 (Ssequence 9 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 10 (Expr (Ecast (Tint I8 Unsigned ) 11 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 12 (Tint I8 Unsigned ))) 13 (Ssequence 14 (Ssequence 15 (Scall (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed ))) 16 (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed ))) 17 []) 18 (Sswitch (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) ( 19 (LScase I32 (repr ? 1) 20 Sbreak 21 (LScase I32 (repr ? 3) 22 (Ssequence 33 23 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 34 24 (Expr (Ecast (Tint I8 Unsigned ) … … 37 27 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 38 28 (Tint I32 Signed )) 39 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed )))29 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 40 30 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 41 (LScase I32 (repr ? 7)42 (Ssequence31 Sbreak) 32 (LScase I32 (repr ? 5) 43 33 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 44 34 (Expr (Ecast (Tint I8 Unsigned ) … … 47 37 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 48 38 (Tint I32 Signed )) 49 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed )))39 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 50 40 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 51 Sbreak)52 (LSdefault41 (LScase I32 (repr ? 7) 42 (Ssequence 53 43 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 54 44 (Expr (Ecast (Tint I8 Unsigned ) … … 57 47 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 58 48 (Tint I32 Signed )) 59 (Expr (Econst_int I32 (repr ? 16))49 (Expr (Econst_int I32 (repr ? 3)) 60 50 (Tint I32 Signed ))) (Tint I32 Signed ))) 61 (Tint I8 Unsigned )))))))) 62 ))) 63 (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed ) 51 (Tint I8 Unsigned ))) 52 Sbreak) 53 (LSdefault 54 (Sassign (Expr (Evar (ident_of_nat 2)) 55 (Tint I8 Unsigned )) 56 (Expr (Ecast (Tint I8 Unsigned ) 57 (Expr (Ebinop Oadd 58 (Expr (Ecast (Tint I32 Signed ) 64 59 (Expr (Evar (ident_of_nat 2)) 65 (Tint I8 Unsigned ))) (Tint I32 Signed )))))) 66 67 68 69 )〉] 60 (Tint I8 Unsigned ))) (Tint I32 Signed )) 61 (Expr (Econst_int I32 (repr ? 16)) 62 (Tint I32 Signed ))) (Tint I32 Signed ))) 63 (Tint I8 Unsigned )))))))) 64 ))) 65 (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed ) 66 (Expr (Evar (ident_of_nat 2)) 67 (Tint I8 Unsigned ))) (Tint I32 Signed )))))) 68 69 70 71 )〉] 70 72 (ident_of_nat 1) 71 []73 72 74 . 73 75 74 example exec0: finishes_with (repr I32 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 0)]). 76 (* 77 example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]). 75 78 normalize (* you can examine the result here *) 76 @refl qed. 77 78 example exec1: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 1)]). 79 normalize (* you can examine the result here *) 80 @refl qed. 81 82 example exec3: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 3)]). 83 normalize (* you can examine the result here *) 84 @refl qed. 85 86 example exec5: finishes_with (repr I32 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]). 87 normalize (* you can examine the result here *) 88 @refl qed. 89 90 example exec7: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 7)]). 91 normalize (* you can examine the result here *) 92 @refl qed. 79 *)
Note: See TracChangeset
for help on using the changeset viewer.