Changeset 1513 for src/Clight/test/null-op.c.ma
- Timestamp:
- Nov 17, 2011, 4:50:46 PM (9 years ago)
- File:
-
- 1 edited
-
src/Clight/test/null-op.c.ma (modified) (1 diff)
Legend:
- Unmodified
- Added
- Removed
-
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 *)
Note: See TracChangeset
for help on using the changeset viewer.
