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/castremoval.c.ma

    r1198 r1513  
    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 I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 4, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ]
    7        (Ssequence
    8        (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    9          (Expr (Ecast (Tint I8 Unsigned )
    10            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    11            (Tint I8 Unsigned )))
    12        (Ssequence
    13        (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    14          (Expr (Ecast (Tint I8 Unsigned )
    15            (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    16            (Tint I8 Unsigned )))
    17        (Ssequence
    18        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    19          (Expr (Ecast (Tint I8 Unsigned )
    20            (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
    21            (Tint I8 Unsigned )))
    22        (Ssequence
    23        (Sassign (Expr (Evar (ident_of_nat 4)) (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 1)) (Tint I8 Unsigned )))
    28                (Tint I32 Signed  ))
    29              (Expr (Ecast (Tint I32 Signed  )
    30                (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    31                (Tint I32 Signed  ))) (Tint I32 Signed  )))
    32            (Tint I8 Unsigned )))
    33        (Ssequence
    34        (Sassign (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned ))
    35          (Expr (Ecast (Tint I8 Unsigned )
    36            (Expr (Ebinop Oadd
     4definition myprog := mk_program (\lambda _. 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 I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 4, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ]
     7         (Ssequence
     8         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
     9           (Expr (Ecast (Tint I8 Unsigned )
     10             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     11             (Tint I8 Unsigned )))
     12         (Ssequence
     13         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     14           (Expr (Ecast (Tint I8 Unsigned )
     15             (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     16             (Tint I8 Unsigned )))
     17         (Ssequence
     18         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
     19           (Expr (Ecast (Tint I8 Unsigned )
     20             (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
     21             (Tint I8 Unsigned )))
     22         (Ssequence
     23         (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I8 Unsigned ))
     24           (Expr (Ecast (Tint I8 Unsigned )
    3725             (Expr (Ebinop Oadd
    3826               (Expr (Ecast (Tint I32 Signed  )
     
    4129               (Expr (Ecast (Tint I32 Signed  )
    4230                 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    43                  (Tint I32 Signed  ))) (Tint I32 Signed  ))
    44              (Expr (Ecast (Tint I32 Signed  )
    45                (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    46                (Tint I32 Signed  ))) (Tint I32 Signed  )))
    47            (Tint I8 Unsigned )))
    48        (Sreturn (Some expr (Expr (Ebinop Oeq
    49                              (Expr (Ecast (Tint I32 Signed  )
    50                                (Expr (Evar (ident_of_nat 5))
    51                                  (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    52                              (Expr (Ebinop Oadd
     31                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
     32             (Tint I8 Unsigned )))
     33         (Ssequence
     34         (Sassign (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned ))
     35           (Expr (Ecast (Tint I8 Unsigned )
     36             (Expr (Ebinop Oadd
     37               (Expr (Ebinop Oadd
     38                 (Expr (Ecast (Tint I32 Signed  )
     39                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
     40                   (Tint I32 Signed  ))
     41                 (Expr (Ecast (Tint I32 Signed  )
     42                   (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
     43                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
     44               (Expr (Ecast (Tint I32 Signed  )
     45                 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
     46                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
     47             (Tint I8 Unsigned )))
     48         (Sreturn (Some expr (Expr (Ebinop Oeq
    5349                               (Expr (Ecast (Tint I32 Signed  )
    54                                  (Expr (Evar (ident_of_nat 4))
     50                                 (Expr (Evar (ident_of_nat 5))
    5551                                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    56                                (Expr (Ecast (Tint I32 Signed  )
    57                                  (Expr (Evar (ident_of_nat 3))
    58                                    (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    59                                (Tint I32 Signed  ))) (Tint I32 Signed  )))))))))
    60      
    61      
    62      
    63    )〉]
     52                               (Expr (Ebinop Oadd
     53                                 (Expr (Ecast (Tint I32 Signed  )
     54                                   (Expr (Evar (ident_of_nat 4))
     55                                     (Tint I8 Unsigned )))
     56                                   (Tint I32 Signed  ))
     57                                 (Expr (Ecast (Tint I32 Signed  )
     58                                   (Expr (Evar (ident_of_nat 3))
     59                                     (Tint I8 Unsigned )))
     60                                   (Tint I32 Signed  ))) (Tint I32 Signed  )))
     61                               (Tint I32 Signed  )))))))))
     62       
     63       
     64       
     65     )〉]
    6466  (ident_of_nat 0)
    65   []
     67 
    6668.
    6769
    68 example exec: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
     70(*
     71example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    6972normalize  (* you can examine the result here *)
    70 @refl
    71 qed.
    72 
    73 include "Clight/SimplifyCasts.ma".
    74 
    75 example simplified: result ? (simplify_program myprog).
    76 normalize
    77 %
    78 qed.
    79 
    80 example exec_s: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [EVint I32 (repr I32 0)]).
    81 normalize  (* you can examine the result here *)
    82 @refl
    83 qed.
    84 
     73*)
Note: See TracChangeset for help on using the changeset viewer.