Changeset 965 for src/Clight/test
- Timestamp:
- Jun 15, 2011, 4:15:56 PM (10 years ago)
- Location:
- src/Clight/test
- Files:
-
- 2 added
- 2 deleted
- 1 edited
- 2 moved
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/insertsort.c
r485 r965 1 /* Remove memory region for now. */ 2 #define __pdata 3 1 4 struct list { 2 5 unsigned char i; -
src/Clight/test/null-op.c.ma
r964 r965 9 9 (Tpointer Any (Tint I8 Unsigned ))) 10 10 (Expr (Ecast (Tpointer Any (Tint I8 Unsigned )) 11 (Expr (Econst_int (repr0)) (Tint I32 Signed )))11 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 12 12 (Tpointer Any (Tint I8 Unsigned )))) 13 13 (Ssequence … … 23 23 (Tpointer Any (Tint I8 Unsigned )))) 24 24 (Tint I32 Signed )) 25 (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed )))) 25 (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0)) 26 (Tint I32 Signed )))) 26 27 Sskip) 27 28 (Ssequence … … 33 34 (Tpointer Any (Tint I8 Unsigned )))) 34 35 (Tint I32 Signed )) 35 (Expr (Econst_int (repr0)) (Tint I32 Signed )))36 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 36 37 (Tint I32 Signed )) 37 (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed )))) 38 (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0)) 39 (Tint I32 Signed )))) 38 40 Sskip) 39 41 (Ssequence … … 42 44 (Expr (Ebinop Oadd 43 45 (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))) 44 (Expr (Econst_int (repr0)) (Tint I32 Signed )))46 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 45 47 (Tpointer Any (Tint I8 Unsigned )))) 46 48 (Ssequence 47 49 (Sassign (Expr (Evar (ident_of_nat 2)) 48 50 (Tpointer Any (Tint I8 Unsigned ))) 49 (Expr (Ebinop Oadd (Expr (Econst_int (repr 0)) (Tint I32 Signed )) 51 (Expr (Ebinop Oadd 52 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed )) 50 53 (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))) 51 54 (Tpointer Any (Tint I8 Unsigned )))) … … 55 58 (Expr (Ebinop Osub 56 59 (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))) 57 (Expr (Econst_int (repr0)) (Tint I32 Signed )))60 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 58 61 (Tpointer Any (Tint I8 Unsigned )))) 59 62 (Sreturn (Some expr (Expr (Ebinop Oeq … … 62 65 (Expr (Ecast (Tpointer Any (Tint I8 Unsigned )) 63 66 (Expr (Ecast (Tpointer Any Tvoid) 64 (Expr (Econst_int (repr0))65 (Tint I 32 Unsigned)))67 (Expr (Econst_int I8 (repr ? 0)) 68 (Tint I8 Unsigned ))) 66 69 (Tpointer Any Tvoid))) 67 70 (Tpointer Any (Tint I8 Unsigned )))) -
src/Clight/test/sum.c.ma
r964 r965 1 include "Clight/Cexec.ma". 1 2 include "common/Animation.ma". 2 include "Clight/Cexec.ma".3 3 4 4 definition myprog := mk_program clight_fundef type … … 10 10 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 11 11 (Tint I8 Unsigned ))) 12 (Ssequence13 12 (Ssequence 14 13 (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed )) … … 37 36 (Tarray Any (Tint I8 Unsigned ) 5)) 38 37 (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed ))) 39 (T array Any (Tint I8 Unsigned ) 5)))38 (Tpointer Any (Tint I8 Unsigned )))) 40 39 (Tint I8 Unsigned ))) (Tint I32 Signed ))) 41 40 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 42 41 ) 43 Sskip)44 42 (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed ) 45 43 (Expr (Evar (ident_of_nat 2)) … … 51 49 (ident_of_nat 0) 52 50 [〈〈〈ident_of_nat 3 (* src *), 53 [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 17)) ; 54 (Init_int8 (repr I8 8)) ; (Init_int8 (repr I8 4)) ]〉, Any〉, 51 [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ; 52 (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ; 53 (Init_int8 (repr I8 4)) ]〉, Any〉, 55 54 (Tarray Any (Tint I8 Unsigned ) 5)〉] 56 55 . … … 64 63 include "Cminor/semantics.ma". 65 64 66 example e1: finishes_with (repr 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).65 example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]). 67 66 normalize 68 67 @refl … … 72 71 include "RTLabs/semantics.ma". 73 72 74 example e2: finishes_with (repr 74) ? (73 example e2: finishes_with (repr I32 74) ? ( 75 74 do p1 ← clight_to_cminor myprog; 76 75 do p2 ← cminor_to_rtlabs p1;
Note: See TracChangeset
for help on using the changeset viewer.