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

    r965 r1513  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef 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, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I8 Unsigned ))〉 ]
    7        (Ssequence
    8        (Sassign (Expr (Evar (ident_of_nat 2))
    9                   (Tpointer Any (Tint I8 Unsigned )))
    10          (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
    11            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    12            (Tpointer Any (Tint I8 Unsigned ))))
    13        (Ssequence
    14        (Sassign (Expr (Evar (ident_of_nat 3))
    15                   (Tpointer Any (Tint I8 Unsigned )))
    16          (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    17            (Tpointer Any (Tint I8 Unsigned ))))
    18        (Ssequence
    19        (Sifthenelse (Expr (Ebinop Oeq
    20                       (Expr (Evar (ident_of_nat 2))
    21                         (Tpointer Any (Tint I8 Unsigned )))
    22                       (Expr (Evar (ident_of_nat 3))
    23                         (Tpointer Any (Tint I8 Unsigned ))))
    24                       (Tint I32 Signed  ))
    25          (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
    26                                (Tint I32 Signed  ))))
    27          Sskip)
    28        (Ssequence
    29        (Sifthenelse (Expr (Ebinop Ogt
    30                       (Expr (Ebinop Osub
     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, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I8 Unsigned ))〉 ]
     7         (Ssequence
     8         (Sassign (Expr (Evar (ident_of_nat 2))
     9                    (Tpointer Any (Tint I8 Unsigned )))
     10           (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
     11             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     12             (Tpointer Any (Tint I8 Unsigned ))))
     13         (Ssequence
     14         (Sassign (Expr (Evar (ident_of_nat 3))
     15                    (Tpointer Any (Tint I8 Unsigned )))
     16           (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
     17             (Tpointer Any (Tint I8 Unsigned ))))
     18         (Ssequence
     19         (Sifthenelse (Expr (Ebinop Oeq
    3120                        (Expr (Evar (ident_of_nat 2))
    3221                          (Tpointer Any (Tint I8 Unsigned )))
    33                         (Expr (Evar (ident_of_nat 2))
     22                        (Expr (Evar (ident_of_nat 3))
    3423                          (Tpointer Any (Tint I8 Unsigned ))))
    3524                        (Tint I32 Signed  ))
    36                       (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    37                       (Tint I32 Signed  ))
    38          (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
    39                                (Tint I32 Signed  ))))
    40          Sskip)
    41        (Ssequence
    42        (Sassign (Expr (Evar (ident_of_nat 2))
    43                   (Tpointer Any (Tint I8 Unsigned )))
    44          (Expr (Ebinop Oadd
    45            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
    46            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    47            (Tpointer Any (Tint I8 Unsigned ))))
    48        (Ssequence
    49        (Sassign (Expr (Evar (ident_of_nat 2))
    50                   (Tpointer Any (Tint I8 Unsigned )))
    51          (Expr (Ebinop Oadd
    52            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
    53            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))))
    54            (Tpointer Any (Tint I8 Unsigned ))))
    55        (Ssequence
    56        (Sassign (Expr (Evar (ident_of_nat 2))
    57                   (Tpointer Any (Tint I8 Unsigned )))
    58          (Expr (Ebinop Osub
    59            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
    60            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    61            (Tpointer Any (Tint I8 Unsigned ))))
    62        (Sreturn (Some expr (Expr (Ebinop Oeq
    63                              (Expr (Evar (ident_of_nat 2))
    64                                (Tpointer Any (Tint I8 Unsigned )))
    65                              (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
    66                                (Expr (Ecast (Tpointer Any Tvoid)
    67                                  (Expr (Econst_int I8 (repr ? 0))
    68                                    (Tint I8 Unsigned )))
    69                                  (Tpointer Any Tvoid)))
    70                                (Tpointer Any (Tint I8 Unsigned ))))
    71                              (Tint I32 Signed  )))))))))))
    72      
    73      
    74      
    75    )〉]
     25           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
     26                                 (Tint I32 Signed  ))))
     27           Sskip)
     28         (Ssequence
     29         (Sifthenelse (Expr (Ebinop Ogt
     30                        (Expr (Ebinop Osub
     31                          (Expr (Evar (ident_of_nat 2))
     32                            (Tpointer Any (Tint I8 Unsigned )))
     33                          (Expr (Evar (ident_of_nat 2))
     34                            (Tpointer Any (Tint I8 Unsigned ))))
     35                          (Tint I32 Signed  ))
     36                        (Expr (Econst_int I32 (repr ? 0))
     37                          (Tint I32 Signed  ))) (Tint I32 Signed  ))
     38           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
     39                                 (Tint I32 Signed  ))))
     40           Sskip)
     41         (Ssequence
     42         (Sassign (Expr (Evar (ident_of_nat 2))
     43                    (Tpointer Any (Tint I8 Unsigned )))
     44           (Expr (Ebinop Oadd
     45             (Expr (Evar (ident_of_nat 2))
     46               (Tpointer Any (Tint I8 Unsigned )))
     47             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     48             (Tpointer Any (Tint I8 Unsigned ))))
     49         (Ssequence
     50         (Sassign (Expr (Evar (ident_of_nat 2))
     51                    (Tpointer Any (Tint I8 Unsigned )))
     52           (Expr (Ebinop Oadd
     53             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
     54             (Expr (Evar (ident_of_nat 2))
     55               (Tpointer Any (Tint I8 Unsigned ))))
     56             (Tpointer Any (Tint I8 Unsigned ))))
     57         (Ssequence
     58         (Sassign (Expr (Evar (ident_of_nat 2))
     59                    (Tpointer Any (Tint I8 Unsigned )))
     60           (Expr (Ebinop Osub
     61             (Expr (Evar (ident_of_nat 2))
     62               (Tpointer Any (Tint I8 Unsigned )))
     63             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     64             (Tpointer Any (Tint I8 Unsigned ))))
     65         (Sreturn (Some expr (Expr (Ebinop Oeq
     66                               (Expr (Evar (ident_of_nat 2))
     67                                 (Tpointer Any (Tint I8 Unsigned )))
     68                               (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
     69                                 (Expr (Ecast (Tpointer Any Tvoid)
     70                                   (Expr (Econst_int I8 (repr ? 0))
     71                                     (Tint I8 Unsigned )))
     72                                   (Tpointer Any Tvoid)))
     73                                 (Tpointer Any (Tint I8 Unsigned ))))
     74                               (Tint I32 Signed  )))))))))))
     75       
     76       
     77       
     78     )〉]
    7679  (ident_of_nat 0)
    77   []
     80 
    7881.
    7982
    80 example exec: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 50 [ ]).
     83(*
     84example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    8185normalize  (* you can examine the result here *)
    82 @refl
    83 qed.
     86*)
Note: See TracChangeset for help on using the changeset viewer.