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/search.ma

    r816 r961  
    88       (Sassign (Expr (Evar (ident_of_nat 1)) (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
     
    1717               (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
    1818               (Tint I32 Signed  ))
    19              (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     19             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2020             (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    2121       (Ssequence
     
    3939                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    4040                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
    41                (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
     41               (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    4242               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    4343         (Ssequence
     
    8080                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    8181                   (Tint I32 Signed  ))
    82                  (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     82                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    8383                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    8484           Sskip)
     
    103103                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    104104                   (Tint I32 Signed  ))
    105                  (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     105                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    106106                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    107107           Sskip)))))
    108108       Sskip)
    109109       (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
    110                              (Expr (Eunop Oneg (Expr (Econst_int (repr 1))
     110                             (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
    111111                                                 (Tint I32 Signed  )))
    112112                               (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
     
    122122                   (Expr (Evar (ident_of_nat 4))
    123123                     (Tarray Any (Tint I8 Unsigned ) 5))
    124                    (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    125                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    126         (Expr (Ecast (Tint I8 Unsigned )
    127           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    128           (Tint I8 Unsigned )))
    129       (Ssequence
    130       (Sassign (Expr (Ederef
    131                  (Expr (Ebinop Oadd
    132                    (Expr (Evar (ident_of_nat 4))
    133                      (Tarray Any (Tint I8 Unsigned ) 5))
    134                    (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    135                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    136         (Expr (Ecast (Tint I8 Unsigned )
    137           (Expr (Econst_int (repr 18)) (Tint I32 Signed  )))
    138           (Tint I8 Unsigned )))
    139       (Ssequence
    140       (Sassign (Expr (Ederef
    141                  (Expr (Ebinop Oadd
    142                    (Expr (Evar (ident_of_nat 4))
    143                      (Tarray Any (Tint I8 Unsigned ) 5))
    144                    (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    145                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    146         (Expr (Ecast (Tint I8 Unsigned )
    147           (Expr (Econst_int (repr 23)) (Tint I32 Signed  )))
    148           (Tint I8 Unsigned )))
    149       (Ssequence
    150       (Sassign (Expr (Ederef
    151                  (Expr (Ebinop Oadd
    152                    (Expr (Evar (ident_of_nat 4))
    153                      (Tarray Any (Tint I8 Unsigned ) 5))
    154                    (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
    155                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    156         (Expr (Ecast (Tint I8 Unsigned )
    157           (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
    158           (Tint I8 Unsigned )))
    159       (Ssequence
    160       (Sassign (Expr (Ederef
    161                  (Expr (Ebinop Oadd
    162                    (Expr (Evar (ident_of_nat 4))
    163                      (Tarray Any (Tint I8 Unsigned ) 5))
    164                    (Expr (Econst_int (repr 4)) (Tint I32 Signed  )))
    165                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    166         (Expr (Ecast (Tint I8 Unsigned )
    167           (Expr (Econst_int (repr 120)) (Tint I32 Signed  )))
     124                   (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     125                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     126        (Expr (Ecast (Tint I8 Unsigned )
     127          (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     128          (Tint I8 Unsigned )))
     129      (Ssequence
     130      (Sassign (Expr (Ederef
     131                 (Expr (Ebinop Oadd
     132                   (Expr (Evar (ident_of_nat 4))
     133                     (Tarray Any (Tint I8 Unsigned ) 5))
     134                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     135                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     136        (Expr (Ecast (Tint I8 Unsigned )
     137          (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed  )))
     138          (Tint I8 Unsigned )))
     139      (Ssequence
     140      (Sassign (Expr (Ederef
     141                 (Expr (Ebinop Oadd
     142                   (Expr (Evar (ident_of_nat 4))
     143                     (Tarray Any (Tint I8 Unsigned ) 5))
     144                   (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     145                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     146        (Expr (Ecast (Tint I8 Unsigned )
     147          (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed  )))
     148          (Tint I8 Unsigned )))
     149      (Ssequence
     150      (Sassign (Expr (Ederef
     151                 (Expr (Ebinop Oadd
     152                   (Expr (Evar (ident_of_nat 4))
     153                     (Tarray Any (Tint I8 Unsigned ) 5))
     154                   (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
     155                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     156        (Expr (Ecast (Tint I8 Unsigned )
     157          (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
     158          (Tint I8 Unsigned )))
     159      (Ssequence
     160      (Sassign (Expr (Ederef
     161                 (Expr (Ebinop Oadd
     162                   (Expr (Evar (ident_of_nat 4))
     163                     (Tarray Any (Tint I8 Unsigned ) 5))
     164                   (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
     165                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     166        (Expr (Ecast (Tint I8 Unsigned )
     167          (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed  )))
    168168          (Tint I8 Unsigned )))
    169169      (Ssequence
     
    173173        [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
    174174        (Expr (Ecast (Tint I8 Unsigned )
    175           (Expr (Econst_int (repr 5)) (Tint I32 Signed  )))
     175          (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
    176176          (Tint I8 Unsigned ));
    177177        (Expr (Ecast (Tint I8 Unsigned )
    178           (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
     178          (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
    179179          (Tint I8 Unsigned ))])
    180180      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
     
    189189.
    190190
    191 example exec: finishes_with (repr 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
     191example exec: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
    192192normalize  (* you can examine the result here *)
    193193@refl
     
    197197include "Cminor/semantics.ma".
    198198
    199 example e1: finishes_with (repr 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     199example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
    200200normalize
    201201@refl
Note: See TracChangeset for help on using the changeset viewer.