Ignore:
Timestamp:
Nov 17, 2011, 4:50:46 PM (9 years ago)
Author:
campbell
Message:

Fix up Clight examples.

File:
1 edited

Legend:

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

    r978 r1513  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
    5   [〈ident_of_nat 0 (* get *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
    6   〈ident_of_nat 1 (* main *), CL_Internal (
    7     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ]
    8       (Ssequence
    9       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    10         (Expr (Ecast (Tint I8 Unsigned )
    11           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    12           (Tint I8 Unsigned )))
    13       (Ssequence
    14       (Ssequence
    15       (Scall (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
    16         (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
    17         [])
    18       (Sswitch (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )) (
    19         (LScase I32 (repr ? 1)
    20           Sbreak
    21           (LScase I32 (repr ? 3)
    22             (Ssequence
    23             (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    24               (Expr (Ecast (Tint I8 Unsigned )
    25                 (Expr (Ebinop Oadd
    26                   (Expr (Ecast (Tint I32 Signed  )
    27                     (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    28                     (Tint I32 Signed  ))
    29                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    30                   (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    31             Sbreak)
    32             (LScase I32 (repr ? 5)
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [][〈ident_of_nat 0 (* get *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
     6    〈ident_of_nat 1 (* main *), CL_Internal (
     7      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ]
     8        (Ssequence
     9        (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     10          (Expr (Ecast (Tint I8 Unsigned )
     11            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     12            (Tint I8 Unsigned )))
     13        (Ssequence
     14        (Ssequence
     15        (Scall (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
     16          (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
     17          [])
     18        (Sswitch (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )) (
     19          (LScase I32 (repr ? 1)
     20            Sbreak
     21            (LScase I32 (repr ? 3)
     22              (Ssequence
    3323              (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    3424                (Expr (Ecast (Tint I8 Unsigned )
     
    3727                      (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    3828                      (Tint I32 Signed  ))
    39                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     29                    (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    4030                    (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    41               (LScase I32 (repr ? 7)
    42                 (Ssequence
     31              Sbreak)
     32              (LScase I32 (repr ? 5)
    4333                (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    4434                  (Expr (Ecast (Tint I8 Unsigned )
     
    4737                        (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    4838                        (Tint I32 Signed  ))
    49                       (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
     39                      (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    5040                      (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    51                 Sbreak)
    52                 (LSdefault
     41                (LScase I32 (repr ? 7)
     42                  (Ssequence
    5343                  (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    5444                    (Expr (Ecast (Tint I8 Unsigned )
     
    5747                          (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    5848                          (Tint I32 Signed  ))
    59                         (Expr (Econst_int I32 (repr ? 16))
     49                        (Expr (Econst_int I32 (repr ? 3))
    6050                          (Tint I32 Signed  ))) (Tint I32 Signed  )))
    61                       (Tint I8 Unsigned ))))))))
    62       )))
    63       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
     51                      (Tint I8 Unsigned )))
     52                  Sbreak)
     53                  (LSdefault
     54                    (Sassign (Expr (Evar (ident_of_nat 2))
     55                               (Tint I8 Unsigned ))
     56                      (Expr (Ecast (Tint I8 Unsigned )
     57                        (Expr (Ebinop Oadd
     58                          (Expr (Ecast (Tint I32 Signed  )
    6459                            (Expr (Evar (ident_of_nat 2))
    65                               (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
    66    
    67    
    68    
    69   )〉]
     60                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
     61                          (Expr (Econst_int I32 (repr ? 16))
     62                            (Tint I32 Signed  ))) (Tint I32 Signed  )))
     63                        (Tint I8 Unsigned ))))))))
     64        )))
     65        (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
     66                              (Expr (Evar (ident_of_nat 2))
     67                                (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
     68     
     69     
     70     
     71    )〉]
    7072  (ident_of_nat 1)
    71   []
     73 
    7274.
    7375
    74 example exec0: finishes_with (repr I32 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 0)]).
     76(*
     77example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    7578normalize  (* you can examine the result here *)
    76 @refl qed.
    77 
    78 example exec1: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 1)]).
    79 normalize  (* you can examine the result here *)
    80 @refl qed.
    81 
    82 example exec3: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 3)]).
    83 normalize  (* you can examine the result here *)
    84 @refl qed.
    85 
    86 example exec5: finishes_with (repr I32 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
    87 normalize  (* you can examine the result here *)
    88 @refl qed.
    89 
    90 example exec7: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 7)]).
    91 normalize  (* you can examine the result here *)
    92 @refl qed.
     79*)
Note: See TracChangeset for help on using the changeset viewer.