Changeset 978 for src/Clight/test


Ignore:
Timestamp:
Jun 16, 2011, 1:32:19 PM (8 years ago)
Author:
campbell
Message:

Update remaining Clight examples.

Location:
src/Clight/test
Files:
1 added
3 deleted
2 moved

Legend:

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

    r975 r978  
    88      (Ssequence
    99      (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    10         (Expr (Evar (ident_of_nat 0))
    11           (Tfunction Tnil (Tint I32 Signed  )))
     10        (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
    1211        [])
    1312      (Ssequence
    1413      (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    15         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    16       (Ssequence
     14        (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    1715      (Ssequence
    1816      (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    19               (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    20         (Expr (Ebinop Ole
    21           (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
     17              (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     18        (Expr (Ebinop Ole (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    2219          (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    2320          (Tint I32 Signed  ))
     
    2522          (Expr (Ebinop Oadd
    2623            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    27             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     24            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2825            (Tint I32 Signed  )))
    2926        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
     
    3330            (Tint I32 Signed  )))
    3431      )
    35       Sskip)
    36       (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
    37                             (Tint I32 Signed  )))))))
     32      (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))))))
    3833   
    3934   
     
    4439.
    4540
    46 example exec: finishes_with (repr 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 5)]).
     41example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
    4742normalize  (* you can examine the result here *)
    4843@refl qed.
  • src/Clight/test/switcher.c.ma

    r975 r978  
    99      (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    1010        (Expr (Ecast (Tint I8 Unsigned )
    11           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     11          (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1212          (Tint I8 Unsigned )))
    1313      (Ssequence
     
    1717        [])
    1818      (Sswitch (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )) (
    19         (LScase (repr 1)
     19        (LScase I32 (repr ? 1)
    2020          Sbreak
    21           (LScase (repr 3)
     21          (LScase I32 (repr ? 3)
    2222            (Ssequence
    2323            (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     
    2727                    (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    2828                    (Tint I32 Signed  ))
    29                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     29                  (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    3030                  (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    3131            Sbreak)
    32             (LScase (repr 5)
     32            (LScase I32 (repr ? 5)
    3333              (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    3434                (Expr (Ecast (Tint I8 Unsigned )
     
    3737                      (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    3838                      (Tint I32 Signed  ))
    39                     (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
     39                    (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    4040                    (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    41               (LScase (repr 7)
     41              (LScase I32 (repr ? 7)
    4242                (Ssequence
    4343                (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     
    4747                        (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    4848                        (Tint I32 Signed  ))
    49                       (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
     49                      (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
    5050                      (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    5151                Sbreak)
     
    5757                          (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    5858                          (Tint I32 Signed  ))
    59                         (Expr (Econst_int (repr 16)) (Tint I32 Signed  )))
    60                         (Tint I32 Signed  ))) (Tint I8 Unsigned ))))))))
     59                        (Expr (Econst_int I32 (repr ? 16))
     60                          (Tint I32 Signed  ))) (Tint I32 Signed  )))
     61                      (Tint I8 Unsigned ))))))))
    6162      )))
    6263      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
     
    7172.
    7273
    73 example exec0: finishes_with (repr 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).
     74example exec0: finishes_with (repr I32 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 0)]).
    7475normalize  (* you can examine the result here *)
    7576@refl qed.
    7677
    77 example exec1: finishes_with (repr 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 1)]).
     78example exec1: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 1)]).
    7879normalize  (* you can examine the result here *)
    7980@refl qed.
    8081
    81 example exec3: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 3)]).
     82example exec3: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 3)]).
    8283normalize  (* you can examine the result here *)
    8384@refl qed.
    8485
    85 example exec5: finishes_with (repr 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 5)]).
     86example exec5: finishes_with (repr I32 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
    8687normalize  (* you can examine the result here *)
    8788@refl qed.
    8889
    89 example exec7: finishes_with (repr 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)]).
     90example exec7: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 7)]).
    9091normalize  (* you can examine the result here *)
    9192@refl qed.
Note: See TracChangeset for help on using the changeset viewer.