Changeset 961 for src/Clight/test/sum.ma


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

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

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

    r881 r961  
    88       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    99         (Expr (Ecast (Tint I8 Unsigned )
    10            (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     10           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1111           (Tint I8 Unsigned )))
    1212       (Ssequence
    1313       (Ssequence
    1414       (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    15                (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     15               (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1616         (Expr (Ebinop Olt
    1717           (Expr (Ecast (Tint I32 Unsigned)
     
    2323           (Expr (Ebinop Oadd
    2424             (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    25              (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     25             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2626             (Tint I32 Signed  )))
    2727         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     
    5151  (ident_of_nat 0)
    5252  [〈〈〈ident_of_nat 3 (* src *),
    53      [(Init_int8 (repr 28)) ; (Init_int8 (repr 17)) ; (Init_int8 (repr 17)) ;
    54      (Init_int8 (repr 8)) ; (Init_int8 (repr 4)) ]〉, Any〉,
     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〉,
    5555     (Tarray Any (Tint I8 Unsigned ) 5)〉]
    5656.
    5757
    58 example exec: finishes_with (repr 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
     58example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
    5959normalize  (* you can examine the result here *)
    6060@refl
Note: See TracChangeset for help on using the changeset viewer.