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

Update some Clight examples.

File:
1 moved

Legend:

Unmodified
Added
Removed
  • 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.