Changeset 1226 for src/Clight/test


Ignore:
Timestamp:
Sep 16, 2011, 7:16:44 PM (8 years ago)
Author:
campbell
Message:

Adjust pretty printers for change in program records, try a test of each.

Location:
src/Clight/test
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/sum.c.ma

    r1198 r1226  
    22include "common/Animation.ma".
    33
    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 I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ]
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [〈〈ident_of_nat 0 (* src *), Any〉,
     6     〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
     7        (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
     8        (Init_int8 (repr I8 4)) ], (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
     9  [〈ident_of_nat 1 (* main *), CL_Internal (
     10     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
    711       (Ssequence
    8        (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     12       (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    913         (Expr (Ecast (Tint I8 Unsigned )
    1014           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1115           (Tint I8 Unsigned )))
    1216       (Ssequence
    13        (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     17       (Sfor (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    1418               (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1519         (Expr (Ebinop Olt
    1620           (Expr (Ecast (Tint I32 Unsigned)
    17              (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
     21             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    1822             (Tint I32 Unsigned))
    1923           (Expr (Esizeof (Tarray Any (Tint I8 Unsigned ) 5))
    2024             (Tint I32 Unsigned))) (Tint I32 Signed  ))
    21          (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     25         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    2226           (Expr (Ebinop Oadd
    23              (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     27             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    2428             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2529             (Tint I32 Signed  )))
    26          (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     30         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    2731           (Expr (Ecast (Tint I8 Unsigned )
    2832             (Expr (Ebinop Oadd
    2933               (Expr (Ecast (Tint I32 Signed  )
    30                  (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
     34                 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    3135                 (Tint I32 Signed  ))
    3236               (Expr (Ecast (Tint I32 Signed  )
    3337                 (Expr (Ederef
    3438                   (Expr (Ebinop Oadd
    35                      (Expr (Evar (ident_of_nat 3))
     39                     (Expr (Evar (ident_of_nat 0))
    3640                       (Tarray Any (Tint I8 Unsigned ) 5))
    37                      (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
     41                     (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    3842                     (Tpointer Any (Tint I8 Unsigned ))))
    3943                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
     
    4145       )
    4246       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    43                              (Expr (Evar (ident_of_nat 2))
     47                             (Expr (Evar (ident_of_nat 3))
    4448                               (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
    4549     
     
    4751     
    4852   )〉]
    49   (ident_of_nat 0)
    50   [〈〈ident_of_nat 3 (* src *), 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)) ],
    54      (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
     53  (ident_of_nat 1)
     54 
    5555.
    5656
    57 example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
     57(*
     58example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    5859normalize  (* you can examine the result here *)
    59 @refl
    60 qed.
    61 
    62 include "Clight/SimplifyCasts.ma".
    63 
    64 example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
    65 normalize  (* you can examine the result here *)
    66 @refl
    67 qed.
    68 
    69 include "Clight/toCminor.ma".
    70 include "Cminor/semantics.ma".
    71 
    72 example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor (simplify_program myprog); exec_up_to Cminor_fullexec p 1000 [ ]).
    73 normalize
    74 @refl
    75 qed.
    76 
    77 include "Cminor/toRTLabs.ma".
    78 include "RTLabs/semantics.ma".
    79 
    80 example e2: finishes_with (repr I32 74) ? (
    81 do p1 ← clight_to_cminor (simplify_program myprog);
    82 do p2 ← cminor_to_rtlabs p1;
    83  exec_up_to RTLabs_fullexec p2 1000 [ ]).
    84 normalize
    85 @refl
    86 qed.
     60*)
Note: See TracChangeset for help on using the changeset viewer.