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

    r1157 r1513  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef ((list init_data) × type)
    5   [〈ident_of_nat 0 (* copy *), CL_Internal (
    6      mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed  )〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 18, (Tpointer Any (Tint I16 Signed  ))〉 ]
    7        (Ssequence
    8        (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    9          (Expr (Ebinop Odiv
    10            (Expr (Ebinop Oadd
    11              (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed  ))
    12              (Expr (Econst_int I32 (repr ? 7)) (Tint I32 Signed  )))
    13              (Tint I32 Signed  ))
    14            (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed  )))
    15            (Tint I32 Signed  )))
    16        (Sswitch (Expr (Ebinop Omod
    17                   (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed  ))
    18                   (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed  )))
    19                   (Tint I32 Signed  )) (
    20          (LScase I32 (repr ? 0)
    21            (Slabel (ident_of_nat 22)
    22            (Ssequence
    23            (Ssequence
    24            (Sassign (Expr (Evar (ident_of_nat 17))
    25                       (Tpointer Any (Tint I16 Signed  )))
    26              (Expr (Evar (ident_of_nat 19))
    27                (Tpointer Any (Tint I16 Signed  ))))
    28            (Sassign (Expr (Evar (ident_of_nat 19))
    29                       (Tpointer Any (Tint I16 Signed  )))
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [][〈ident_of_nat 0 (* copy *), CL_Internal (
     6       mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed  )〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 18, (Tpointer Any (Tint I16 Signed  ))〉 ]
     7         (Ssequence
     8         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     9           (Expr (Ebinop Odiv
    3010             (Expr (Ebinop Oadd
    31                (Expr (Evar (ident_of_nat 17))
    32                  (Tpointer Any (Tint I16 Signed  )))
    33                (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    34                (Tpointer Any (Tint I16 Signed  )))))
    35            (Ssequence
    36            (Ssequence
    37            (Sassign (Expr (Evar (ident_of_nat 18))
    38                       (Tpointer Any (Tint I16 Signed  )))
    39              (Expr (Evar (ident_of_nat 20))
    40                (Tpointer Any (Tint I16 Signed  ))))
    41            (Sassign (Expr (Evar (ident_of_nat 20))
    42                       (Tpointer Any (Tint I16 Signed  )))
    43              (Expr (Ebinop Oadd
    44                (Expr (Evar (ident_of_nat 18))
    45                  (Tpointer Any (Tint I16 Signed  )))
    46                (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    47                (Tpointer Any (Tint I16 Signed  )))))
    48            (Sassign (Expr (Ederef
    49                       (Expr (Evar (ident_of_nat 17))
    50                         (Tpointer Any (Tint I16 Signed  ))))
    51                       (Tint I16 Signed  ))
    52              (Expr (Ederef
    53                (Expr (Evar (ident_of_nat 18))
    54                  (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
    55            (LScase I32 (repr ? 7)
     11               (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed  ))
     12               (Expr (Econst_int I32 (repr ? 7)) (Tint I32 Signed  )))
     13               (Tint I32 Signed  ))
     14             (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed  )))
     15             (Tint I32 Signed  )))
     16         (Sswitch (Expr (Ebinop Omod
     17                    (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed  ))
     18                    (Expr (Econst_int I32 (repr ? 8)) (Tint I32 Signed  )))
     19                    (Tint I32 Signed  )) (
     20           (LScase I32 (repr ? 0)
     21             (Slabel (ident_of_nat 22)
    5622             (Ssequence
    57              (Sassign (Expr (Evar (ident_of_nat 15))
     23             (Ssequence
     24             (Sassign (Expr (Evar (ident_of_nat 17))
    5825                        (Tpointer Any (Tint I16 Signed  )))
    5926               (Expr (Evar (ident_of_nat 19))
    6027                 (Tpointer Any (Tint I16 Signed  ))))
    61              (Ssequence
    6228             (Sassign (Expr (Evar (ident_of_nat 19))
    6329                        (Tpointer Any (Tint I16 Signed  )))
    6430               (Expr (Ebinop Oadd
    65                  (Expr (Evar (ident_of_nat 15))
     31                 (Expr (Evar (ident_of_nat 17))
    6632                   (Tpointer Any (Tint I16 Signed  )))
    6733                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    68                  (Tpointer Any (Tint I16 Signed  ))))
     34                 (Tpointer Any (Tint I16 Signed  )))))
    6935             (Ssequence
    70              (Sassign (Expr (Evar (ident_of_nat 16))
     36             (Ssequence
     37             (Sassign (Expr (Evar (ident_of_nat 18))
    7138                        (Tpointer Any (Tint I16 Signed  )))
    7239               (Expr (Evar (ident_of_nat 20))
    7340                 (Tpointer Any (Tint I16 Signed  ))))
    74              (Ssequence
    7541             (Sassign (Expr (Evar (ident_of_nat 20))
    7642                        (Tpointer Any (Tint I16 Signed  )))
    7743               (Expr (Ebinop Oadd
    78                  (Expr (Evar (ident_of_nat 16))
     44                 (Expr (Evar (ident_of_nat 18))
    7945                   (Tpointer Any (Tint I16 Signed  )))
    8046                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    81                  (Tpointer Any (Tint I16 Signed  ))))
     47                 (Tpointer Any (Tint I16 Signed  )))))
    8248             (Sassign (Expr (Ederef
    83                         (Expr (Evar (ident_of_nat 15))
     49                        (Expr (Evar (ident_of_nat 17))
    8450                          (Tpointer Any (Tint I16 Signed  ))))
    8551                        (Tint I16 Signed  ))
    8652               (Expr (Ederef
    87                  (Expr (Evar (ident_of_nat 16))
    88                    (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
    89              (LScase I32 (repr ? 6)
     53                 (Expr (Evar (ident_of_nat 18))
     54                   (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
     55             (LScase I32 (repr ? 7)
    9056               (Ssequence
    91                (Sassign (Expr (Evar (ident_of_nat 13))
     57               (Sassign (Expr (Evar (ident_of_nat 15))
    9258                          (Tpointer Any (Tint I16 Signed  )))
    9359                 (Expr (Evar (ident_of_nat 19))
     
    9763                          (Tpointer Any (Tint I16 Signed  )))
    9864                 (Expr (Ebinop Oadd
    99                    (Expr (Evar (ident_of_nat 13))
     65                   (Expr (Evar (ident_of_nat 15))
    10066                     (Tpointer Any (Tint I16 Signed  )))
    10167                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    10268                   (Tpointer Any (Tint I16 Signed  ))))
    10369               (Ssequence
    104                (Sassign (Expr (Evar (ident_of_nat 14))
     70               (Sassign (Expr (Evar (ident_of_nat 16))
    10571                          (Tpointer Any (Tint I16 Signed  )))
    10672                 (Expr (Evar (ident_of_nat 20))
     
    11076                          (Tpointer Any (Tint I16 Signed  )))
    11177                 (Expr (Ebinop Oadd
    112                    (Expr (Evar (ident_of_nat 14))
     78                   (Expr (Evar (ident_of_nat 16))
    11379                     (Tpointer Any (Tint I16 Signed  )))
    11480                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    11581                   (Tpointer Any (Tint I16 Signed  ))))
    11682               (Sassign (Expr (Ederef
    117                           (Expr (Evar (ident_of_nat 13))
     83                          (Expr (Evar (ident_of_nat 15))
    11884                            (Tpointer Any (Tint I16 Signed  ))))
    11985                          (Tint I16 Signed  ))
    12086                 (Expr (Ederef
    121                    (Expr (Evar (ident_of_nat 14))
     87                   (Expr (Evar (ident_of_nat 16))
    12288                     (Tpointer Any (Tint I16 Signed  ))))
    12389                   (Tint I16 Signed  )))))))
    124                (LScase I32 (repr ? 5)
     90               (LScase I32 (repr ? 6)
    12591                 (Ssequence
    126                  (Sassign (Expr (Evar (ident_of_nat 11))
     92                 (Sassign (Expr (Evar (ident_of_nat 13))
    12793                            (Tpointer Any (Tint I16 Signed  )))
    12894                   (Expr (Evar (ident_of_nat 19))
     
    13298                            (Tpointer Any (Tint I16 Signed  )))
    13399                   (Expr (Ebinop Oadd
    134                      (Expr (Evar (ident_of_nat 11))
     100                     (Expr (Evar (ident_of_nat 13))
    135101                       (Tpointer Any (Tint I16 Signed  )))
    136102                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    137103                     (Tpointer Any (Tint I16 Signed  ))))
    138104                 (Ssequence
    139                  (Sassign (Expr (Evar (ident_of_nat 12))
     105                 (Sassign (Expr (Evar (ident_of_nat 14))
    140106                            (Tpointer Any (Tint I16 Signed  )))
    141107                   (Expr (Evar (ident_of_nat 20))
     
    145111                            (Tpointer Any (Tint I16 Signed  )))
    146112                   (Expr (Ebinop Oadd
    147                      (Expr (Evar (ident_of_nat 12))
     113                     (Expr (Evar (ident_of_nat 14))
    148114                       (Tpointer Any (Tint I16 Signed  )))
    149115                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    150116                     (Tpointer Any (Tint I16 Signed  ))))
    151117                 (Sassign (Expr (Ederef
    152                             (Expr (Evar (ident_of_nat 11))
     118                            (Expr (Evar (ident_of_nat 13))
    153119                              (Tpointer Any (Tint I16 Signed  ))))
    154120                            (Tint I16 Signed  ))
    155121                   (Expr (Ederef
    156                      (Expr (Evar (ident_of_nat 12))
     122                     (Expr (Evar (ident_of_nat 14))
    157123                       (Tpointer Any (Tint I16 Signed  ))))
    158124                     (Tint I16 Signed  )))))))
    159                  (LScase I32 (repr ? 4)
     125                 (LScase I32 (repr ? 5)
    160126                   (Ssequence
    161                    (Sassign (Expr (Evar (ident_of_nat 9))
     127                   (Sassign (Expr (Evar (ident_of_nat 11))
    162128                              (Tpointer Any (Tint I16 Signed  )))
    163129                     (Expr (Evar (ident_of_nat 19))
     
    167133                              (Tpointer Any (Tint I16 Signed  )))
    168134                     (Expr (Ebinop Oadd
    169                        (Expr (Evar (ident_of_nat 9))
     135                       (Expr (Evar (ident_of_nat 11))
    170136                         (Tpointer Any (Tint I16 Signed  )))
    171137                       (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    172138                       (Tpointer Any (Tint I16 Signed  ))))
    173139                   (Ssequence
    174                    (Sassign (Expr (Evar (ident_of_nat 10))
     140                   (Sassign (Expr (Evar (ident_of_nat 12))
    175141                              (Tpointer Any (Tint I16 Signed  )))
    176142                     (Expr (Evar (ident_of_nat 20))
     
    180146                              (Tpointer Any (Tint I16 Signed  )))
    181147                     (Expr (Ebinop Oadd
    182                        (Expr (Evar (ident_of_nat 10))
     148                       (Expr (Evar (ident_of_nat 12))
    183149                         (Tpointer Any (Tint I16 Signed  )))
    184150                       (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    185151                       (Tpointer Any (Tint I16 Signed  ))))
    186152                   (Sassign (Expr (Ederef
    187                               (Expr (Evar (ident_of_nat 9))
     153                              (Expr (Evar (ident_of_nat 11))
    188154                                (Tpointer Any (Tint I16 Signed  ))))
    189155                              (Tint I16 Signed  ))
    190156                     (Expr (Ederef
    191                        (Expr (Evar (ident_of_nat 10))
     157                       (Expr (Evar (ident_of_nat 12))
    192158                         (Tpointer Any (Tint I16 Signed  ))))
    193159                       (Tint I16 Signed  )))))))
    194                    (LScase I32 (repr ? 3)
     160                   (LScase I32 (repr ? 4)
    195161                     (Ssequence
    196                      (Sassign (Expr (Evar (ident_of_nat 7))
     162                     (Sassign (Expr (Evar (ident_of_nat 9))
    197163                                (Tpointer Any (Tint I16 Signed  )))
    198164                       (Expr (Evar (ident_of_nat 19))
     
    202168                                (Tpointer Any (Tint I16 Signed  )))
    203169                       (Expr (Ebinop Oadd
    204                          (Expr (Evar (ident_of_nat 7))
     170                         (Expr (Evar (ident_of_nat 9))
    205171                           (Tpointer Any (Tint I16 Signed  )))
    206172                         (Expr (Econst_int I32 (repr ? 1))
     
    208174                         (Tpointer Any (Tint I16 Signed  ))))
    209175                     (Ssequence
    210                      (Sassign (Expr (Evar (ident_of_nat 8))
     176                     (Sassign (Expr (Evar (ident_of_nat 10))
    211177                                (Tpointer Any (Tint I16 Signed  )))
    212178                       (Expr (Evar (ident_of_nat 20))
     
    216182                                (Tpointer Any (Tint I16 Signed  )))
    217183                       (Expr (Ebinop Oadd
    218                          (Expr (Evar (ident_of_nat 8))
     184                         (Expr (Evar (ident_of_nat 10))
    219185                           (Tpointer Any (Tint I16 Signed  )))
    220186                         (Expr (Econst_int I32 (repr ? 1))
     
    222188                         (Tpointer Any (Tint I16 Signed  ))))
    223189                     (Sassign (Expr (Ederef
    224                                 (Expr (Evar (ident_of_nat 7))
     190                                (Expr (Evar (ident_of_nat 9))
    225191                                  (Tpointer Any (Tint I16 Signed  ))))
    226192                                (Tint I16 Signed  ))
    227193                       (Expr (Ederef
    228                          (Expr (Evar (ident_of_nat 8))
     194                         (Expr (Evar (ident_of_nat 10))
    229195                           (Tpointer Any (Tint I16 Signed  ))))
    230196                         (Tint I16 Signed  )))))))
    231                      (LScase I32 (repr ? 2)
     197                     (LScase I32 (repr ? 3)
    232198                       (Ssequence
    233                        (Sassign (Expr (Evar (ident_of_nat 5))
     199                       (Sassign (Expr (Evar (ident_of_nat 7))
    234200                                  (Tpointer Any (Tint I16 Signed  )))
    235201                         (Expr (Evar (ident_of_nat 19))
     
    239205                                  (Tpointer Any (Tint I16 Signed  )))
    240206                         (Expr (Ebinop Oadd
    241                            (Expr (Evar (ident_of_nat 5))
     207                           (Expr (Evar (ident_of_nat 7))
    242208                             (Tpointer Any (Tint I16 Signed  )))
    243209                           (Expr (Econst_int I32 (repr ? 1))
     
    245211                           (Tpointer Any (Tint I16 Signed  ))))
    246212                       (Ssequence
    247                        (Sassign (Expr (Evar (ident_of_nat 6))
     213                       (Sassign (Expr (Evar (ident_of_nat 8))
    248214                                  (Tpointer Any (Tint I16 Signed  )))
    249215                         (Expr (Evar (ident_of_nat 20))
     
    253219                                  (Tpointer Any (Tint I16 Signed  )))
    254220                         (Expr (Ebinop Oadd
    255                            (Expr (Evar (ident_of_nat 6))
     221                           (Expr (Evar (ident_of_nat 8))
    256222                             (Tpointer Any (Tint I16 Signed  )))
    257223                           (Expr (Econst_int I32 (repr ? 1))
     
    259225                           (Tpointer Any (Tint I16 Signed  ))))
    260226                       (Sassign (Expr (Ederef
    261                                   (Expr (Evar (ident_of_nat 5))
     227                                  (Expr (Evar (ident_of_nat 7))
    262228                                    (Tpointer Any (Tint I16 Signed  ))))
    263229                                  (Tint I16 Signed  ))
    264230                         (Expr (Ederef
    265                            (Expr (Evar (ident_of_nat 6))
     231                           (Expr (Evar (ident_of_nat 8))
    266232                             (Tpointer Any (Tint I16 Signed  ))))
    267233                           (Tint I16 Signed  )))))))
    268                        (LScase I32 (repr ? 1)
     234                       (LScase I32 (repr ? 2)
    269235                         (Ssequence
    270                          (Sassign (Expr (Evar (ident_of_nat 3))
     236                         (Sassign (Expr (Evar (ident_of_nat 5))
    271237                                    (Tpointer Any (Tint I16 Signed  )))
    272238                           (Expr (Evar (ident_of_nat 19))
     
    276242                                    (Tpointer Any (Tint I16 Signed  )))
    277243                           (Expr (Ebinop Oadd
    278                              (Expr (Evar (ident_of_nat 3))
     244                             (Expr (Evar (ident_of_nat 5))
    279245                               (Tpointer Any (Tint I16 Signed  )))
    280246                             (Expr (Econst_int I32 (repr ? 1))
     
    282248                             (Tpointer Any (Tint I16 Signed  ))))
    283249                         (Ssequence
    284                          (Sassign (Expr (Evar (ident_of_nat 4))
     250                         (Sassign (Expr (Evar (ident_of_nat 6))
    285251                                    (Tpointer Any (Tint I16 Signed  )))
    286252                           (Expr (Evar (ident_of_nat 20))
     
    290256                                    (Tpointer Any (Tint I16 Signed  )))
    291257                           (Expr (Ebinop Oadd
    292                              (Expr (Evar (ident_of_nat 4))
     258                             (Expr (Evar (ident_of_nat 6))
    293259                               (Tpointer Any (Tint I16 Signed  )))
    294260                             (Expr (Econst_int I32 (repr ? 1))
    295261                               (Tint I32 Signed  )))
    296262                             (Tpointer Any (Tint I16 Signed  ))))
    297                          (Ssequence
    298263                         (Sassign (Expr (Ederef
    299                                     (Expr (Evar (ident_of_nat 3))
     264                                    (Expr (Evar (ident_of_nat 5))
    300265                                      (Tpointer Any (Tint I16 Signed  ))))
    301266                                    (Tint I16 Signed  ))
    302267                           (Expr (Ederef
    303                              (Expr (Evar (ident_of_nat 4))
     268                             (Expr (Evar (ident_of_nat 6))
    304269                               (Tpointer Any (Tint I16 Signed  ))))
    305                              (Tint I16 Signed  )))
    306                          (Ssequence
    307                          (Sassign (Expr (Evar (ident_of_nat 2))
    308                                     (Tint I32 Signed  ))
    309                            (Expr (Ebinop Osub
    310                              (Expr (Evar (ident_of_nat 1))
    311                                (Tint I32 Signed  ))
    312                              (Expr (Econst_int I32 (repr ? 1))
    313                                (Tint I32 Signed  ))) (Tint I32 Signed  )))
    314                          (Ssequence
    315                          (Sassign (Expr (Evar (ident_of_nat 1))
    316                                     (Tint I32 Signed  ))
    317                            (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    318                          (Sifthenelse (Expr (Ebinop Ogt
    319                                         (Expr (Evar (ident_of_nat 2))
     270                             (Tint I16 Signed  )))))))
     271                         (LScase I32 (repr ? 1)
     272                           (Ssequence
     273                           (Sassign (Expr (Evar (ident_of_nat 3))
     274                                      (Tpointer Any (Tint I16 Signed  )))
     275                             (Expr (Evar (ident_of_nat 19))
     276                               (Tpointer Any (Tint I16 Signed  ))))
     277                           (Ssequence
     278                           (Sassign (Expr (Evar (ident_of_nat 19))
     279                                      (Tpointer Any (Tint I16 Signed  )))
     280                             (Expr (Ebinop Oadd
     281                               (Expr (Evar (ident_of_nat 3))
     282                                 (Tpointer Any (Tint I16 Signed  )))
     283                               (Expr (Econst_int I32 (repr ? 1))
     284                                 (Tint I32 Signed  )))
     285                               (Tpointer Any (Tint I16 Signed  ))))
     286                           (Ssequence
     287                           (Sassign (Expr (Evar (ident_of_nat 4))
     288                                      (Tpointer Any (Tint I16 Signed  )))
     289                             (Expr (Evar (ident_of_nat 20))
     290                               (Tpointer Any (Tint I16 Signed  ))))
     291                           (Ssequence
     292                           (Sassign (Expr (Evar (ident_of_nat 20))
     293                                      (Tpointer Any (Tint I16 Signed  )))
     294                             (Expr (Ebinop Oadd
     295                               (Expr (Evar (ident_of_nat 4))
     296                                 (Tpointer Any (Tint I16 Signed  )))
     297                               (Expr (Econst_int I32 (repr ? 1))
     298                                 (Tint I32 Signed  )))
     299                               (Tpointer Any (Tint I16 Signed  ))))
     300                           (Ssequence
     301                           (Sassign (Expr (Ederef
     302                                      (Expr (Evar (ident_of_nat 3))
     303                                        (Tpointer Any (Tint I16 Signed  ))))
     304                                      (Tint I16 Signed  ))
     305                             (Expr (Ederef
     306                               (Expr (Evar (ident_of_nat 4))
     307                                 (Tpointer Any (Tint I16 Signed  ))))
     308                               (Tint I16 Signed  )))
     309                           (Ssequence
     310                           (Sassign (Expr (Evar (ident_of_nat 2))
     311                                      (Tint I32 Signed  ))
     312                             (Expr (Ebinop Osub
     313                               (Expr (Evar (ident_of_nat 1))
     314                                 (Tint I32 Signed  ))
     315                               (Expr (Econst_int I32 (repr ? 1))
     316                                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
     317                           (Ssequence
     318                           (Sassign (Expr (Evar (ident_of_nat 1))
     319                                      (Tint I32 Signed  ))
     320                             (Expr (Evar (ident_of_nat 2))
     321                               (Tint I32 Signed  )))
     322                           (Sifthenelse (Expr (Ebinop Ogt
     323                                          (Expr (Evar (ident_of_nat 2))
     324                                            (Tint I32 Signed  ))
     325                                          (Expr (Econst_int I32 (repr ? 0))
     326                                            (Tint I32 Signed  )))
    320327                                          (Tint I32 Signed  ))
    321                                         (Expr (Econst_int I32 (repr ? 0))
    322                                           (Tint I32 Signed  )))
    323                                         (Tint I32 Signed  ))
    324                            (Sgoto (ident_of_nat 22))
    325                            Sskip))))))))
    326                          (LSdefault
    327                            Sskip)))))))))
    328        )))
    329      
    330      
    331      
    332    )〉;
    333   〈ident_of_nat 23 (* main *), CL_Internal (
    334     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 24, (Tarray Any (Tint I16 Signed  ) 3)〉 ; 〈ident_of_nat 25, (Tarray Any (Tint I16 Signed  ) 3)〉 ]
    335       (Ssequence
    336       (Sassign (Expr (Ederef
    337                  (Expr (Ebinop Oadd
    338                    (Expr (Evar (ident_of_nat 24))
    339                      (Tarray Any (Tint I16 Signed  ) 3))
    340                    (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    341                    (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))
    342         (Expr (Ecast (Tint I16 Signed  )
    343           (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    344           (Tint I16 Signed  )))
    345       (Ssequence
    346       (Sassign (Expr (Ederef
    347                  (Expr (Ebinop Oadd
    348                    (Expr (Evar (ident_of_nat 24))
    349                      (Tarray Any (Tint I16 Signed  ) 3))
    350                    (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    351                    (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))
    352         (Expr (Ecast (Tint I16 Signed  )
    353           (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    354           (Tint I16 Signed  )))
    355       (Ssequence
    356       (Sassign (Expr (Ederef
    357                  (Expr (Ebinop Oadd
    358                    (Expr (Evar (ident_of_nat 24))
    359                      (Tarray Any (Tint I16 Signed  ) 3))
    360                    (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    361                    (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))
    362         (Expr (Ecast (Tint I16 Signed  )
    363           (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
    364           (Tint I16 Signed  )))
    365       (Ssequence
    366       (Scall (None expr) (Expr (Evar (ident_of_nat 0))
    367                            (Tfunction (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid))
    368         [(Expr (Evar (ident_of_nat 25)) (Tarray Any (Tint I16 Signed  ) 3));
    369         (Expr (Evar (ident_of_nat 24)) (Tarray Any (Tint I16 Signed  ) 3));
    370         (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  ))])
    371       (Sreturn (Some expr (Expr (Ebinop Oadd
    372                             (Expr (Ebinop Oadd
     328                             (Sgoto (ident_of_nat 22))
     329                             Sskip))))))))
     330                           (LSdefault
     331                             Sskip)))))))))
     332         )))
     333       
     334       
     335       
     336     )〉;
     337    〈ident_of_nat 23 (* main *), CL_Internal (
     338      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 24, (Tarray Any (Tint I16 Signed  ) 3)〉 ; 〈ident_of_nat 25, (Tarray Any (Tint I16 Signed  ) 3)〉 ]
     339        (Ssequence
     340        (Sassign (Expr (Ederef
     341                   (Expr (Ebinop Oadd
     342                     (Expr (Evar (ident_of_nat 24))
     343                       (Tarray Any (Tint I16 Signed  ) 3))
     344                     (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     345                     (Tpointer Any (Tint I16 Signed  ))))
     346                   (Tint I16 Signed  ))
     347          (Expr (Ecast (Tint I16 Signed  )
     348            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     349            (Tint I16 Signed  )))
     350        (Ssequence
     351        (Sassign (Expr (Ederef
     352                   (Expr (Ebinop Oadd
     353                     (Expr (Evar (ident_of_nat 24))
     354                       (Tarray Any (Tint I16 Signed  ) 3))
     355                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     356                     (Tpointer Any (Tint I16 Signed  ))))
     357                   (Tint I16 Signed  ))
     358          (Expr (Ecast (Tint I16 Signed  )
     359            (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     360            (Tint I16 Signed  )))
     361        (Ssequence
     362        (Sassign (Expr (Ederef
     363                   (Expr (Ebinop Oadd
     364                     (Expr (Evar (ident_of_nat 24))
     365                       (Tarray Any (Tint I16 Signed  ) 3))
     366                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     367                     (Tpointer Any (Tint I16 Signed  ))))
     368                   (Tint I16 Signed  ))
     369          (Expr (Ecast (Tint I16 Signed  )
     370            (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
     371            (Tint I16 Signed  )))
     372        (Ssequence
     373        (Scall (None expr) (Expr (Evar (ident_of_nat 0))
     374                             (Tfunction (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid))
     375          [(Expr (Evar (ident_of_nat 25)) (Tarray Any (Tint I16 Signed  ) 3));
     376          (Expr (Evar (ident_of_nat 24)) (Tarray Any (Tint I16 Signed  ) 3));
     377          (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  ))])
     378        (Sreturn (Some expr (Expr (Ebinop Oadd
     379                              (Expr (Ebinop Oadd
     380                                (Expr (Ecast (Tint I32 Signed  )
     381                                  (Expr (Ederef
     382                                    (Expr (Ebinop Oadd
     383                                      (Expr (Evar (ident_of_nat 25))
     384                                        (Tarray Any (Tint I16 Signed  ) 3))
     385                                      (Expr (Econst_int I32 (repr ? 0))
     386                                        (Tint I32 Signed  )))
     387                                      (Tpointer Any (Tint I16 Signed  ))))
     388                                    (Tint I16 Signed  )))
     389                                  (Tint I32 Signed  ))
     390                                (Expr (Ecast (Tint I32 Signed  )
     391                                  (Expr (Ederef
     392                                    (Expr (Ebinop Oadd
     393                                      (Expr (Evar (ident_of_nat 25))
     394                                        (Tarray Any (Tint I16 Signed  ) 3))
     395                                      (Expr (Econst_int I32 (repr ? 1))
     396                                        (Tint I32 Signed  )))
     397                                      (Tpointer Any (Tint I16 Signed  ))))
     398                                    (Tint I16 Signed  )))
     399                                  (Tint I32 Signed  ))) (Tint I32 Signed  ))
    373400                              (Expr (Ecast (Tint I32 Signed  )
    374401                                (Expr (Ederef
     
    376403                                    (Expr (Evar (ident_of_nat 25))
    377404                                      (Tarray Any (Tint I16 Signed  ) 3))
    378                                     (Expr (Econst_int I32 (repr ? 0))
    379                                       (Tint I32 Signed  )))
    380                                     (Tpointer Any (Tint I16 Signed  ))))
    381                                   (Tint I16 Signed  ))) (Tint I32 Signed  ))
    382                               (Expr (Ecast (Tint I32 Signed  )
    383                                 (Expr (Ederef
    384                                   (Expr (Ebinop Oadd
    385                                     (Expr (Evar (ident_of_nat 25))
    386                                       (Tarray Any (Tint I16 Signed  ) 3))
    387                                     (Expr (Econst_int I32 (repr ? 1))
     405                                    (Expr (Econst_int I32 (repr ? 2))
    388406                                      (Tint I32 Signed  )))
    389407                                    (Tpointer Any (Tint I16 Signed  ))))
    390408                                  (Tint I16 Signed  ))) (Tint I32 Signed  )))
    391                               (Tint I32 Signed  ))
    392                             (Expr (Ecast (Tint I32 Signed  )
    393                               (Expr (Ederef
    394                                 (Expr (Ebinop Oadd
    395                                   (Expr (Evar (ident_of_nat 25))
    396                                     (Tarray Any (Tint I16 Signed  ) 3))
    397                                   (Expr (Econst_int I32 (repr ? 2))
    398                                     (Tint I32 Signed  )))
    399                                   (Tpointer Any (Tint I16 Signed  ))))
    400                                 (Tint I16 Signed  ))) (Tint I32 Signed  )))
    401                             (Tint I32 Signed  ))))))))
    402    
    403    
    404    
    405   )〉]
     409                              (Tint I32 Signed  ))))))))
     410     
     411     
     412     
     413    )〉]
    406414  (ident_of_nat 23)
    407   []
     415 
    408416.
    409417
    410 example exec: finishes_with (repr I32 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
     418(*
     419example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    411420normalize  (* you can examine the result here *)
    412 @refl
    413 qed.
     421*)
Note: See TracChangeset for help on using the changeset viewer.