Changeset 965 for src/Clight/test


Ignore:
Timestamp:
Jun 15, 2011, 4:15:56 PM (9 years ago)
Author:
campbell
Message:

Update some Clight examples.

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
    14struct list {
    25  unsigned char i;
  • src/Clight/test/null-op.c.ma

    r964 r965  
    99                  (Tpointer Any (Tint I8 Unsigned )))
    1010         (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
    11            (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     11           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1212           (Tpointer Any (Tint I8 Unsigned ))))
    1313       (Ssequence
     
    2323                        (Tpointer Any (Tint I8 Unsigned ))))
    2424                      (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  ))))
    2627         Sskip)
    2728       (Ssequence
     
    3334                          (Tpointer Any (Tint I8 Unsigned ))))
    3435                        (Tint I32 Signed  ))
    35                       (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     36                      (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    3637                      (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  ))))
    3840         Sskip)
    3941       (Ssequence
     
    4244         (Expr (Ebinop Oadd
    4345           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
    44            (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     46           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    4547           (Tpointer Any (Tint I8 Unsigned ))))
    4648       (Ssequence
    4749       (Sassign (Expr (Evar (ident_of_nat 2))
    4850                  (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  ))
    5053           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))))
    5154           (Tpointer Any (Tint I8 Unsigned ))))
     
    5558         (Expr (Ebinop Osub
    5659           (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
    57            (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     60           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    5861           (Tpointer Any (Tint I8 Unsigned ))))
    5962       (Sreturn (Some expr (Expr (Ebinop Oeq
     
    6265                             (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
    6366                               (Expr (Ecast (Tpointer Any Tvoid)
    64                                  (Expr (Econst_int (repr 0))
    65                                    (Tint I32 Unsigned)))
     67                                 (Expr (Econst_int I8 (repr ? 0))
     68                                   (Tint I8 Unsigned )))
    6669                                 (Tpointer Any Tvoid)))
    6770                               (Tpointer Any (Tint I8 Unsigned ))))
  • src/Clight/test/sum.c.ma

    r964 r965  
     1include "Clight/Cexec.ma".
    12include "common/Animation.ma".
    2 include "Clight/Cexec.ma".
    33
    44definition myprog := mk_program clight_fundef type
     
    1010           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1111           (Tint I8 Unsigned )))
    12        (Ssequence
    1312       (Ssequence
    1413       (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     
    3736                       (Tarray Any (Tint I8 Unsigned ) 5))
    3837                     (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
    39                      (Tarray Any (Tint I8 Unsigned ) 5)))
     38                     (Tpointer Any (Tint I8 Unsigned ))))
    4039                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    4140               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    4241       )
    43        Sskip)
    4442       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    4543                             (Expr (Evar (ident_of_nat 2))
     
    5149  (ident_of_nat 0)
    5250  [〈〈〈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〉,
    5554     (Tarray Any (Tint I8 Unsigned ) 5)〉]
    5655.
     
    6463include "Cminor/semantics.ma".
    6564
    66 example e1: finishes_with (repr 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     65example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
    6766normalize
    6867@refl
     
    7271include "RTLabs/semantics.ma".
    7372
    74 example e2: finishes_with (repr 74) ? (
     73example e2: finishes_with (repr I32 74) ? (
    7574do p1 ← clight_to_cminor myprog;
    7675do p2 ← cminor_to_rtlabs p1;
Note: See TracChangeset for help on using the changeset viewer.