Changeset 2176 for src/Clight/test


Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (8 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

Location:
src/Clight/test
Files:
6 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/test/duff.c.ma

    r1513 r2176  
    44definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
    55  [][〈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  ))〉 ]
     6       mk_function Tvoid [〈ident_of_nat 19, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 20, (Tpointer (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 (Tint I16 Signed  ))〉 ; 〈ident_of_nat 4, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 7, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 8, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 9, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 10, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 11, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 12, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 13, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 14, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 15, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 16, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 17, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 18, (Tpointer (Tint I16 Signed  ))〉 ]
    77         (Ssequence
    88         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    … …  
    2323             (Ssequence
    2424             (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  ))))
     25                        (Tpointer (Tint I16 Signed  )))
     26               (Expr (Evar (ident_of_nat 19)) (Tpointer (Tint I16 Signed  ))))
    2827             (Sassign (Expr (Evar (ident_of_nat 19))
    29                         (Tpointer Any (Tint I16 Signed  )))
     28                        (Tpointer (Tint I16 Signed  )))
    3029               (Expr (Ebinop Oadd
    3130                 (Expr (Evar (ident_of_nat 17))
    32                    (Tpointer Any (Tint I16 Signed  )))
     31                   (Tpointer (Tint I16 Signed  )))
    3332                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    34                  (Tpointer Any (Tint I16 Signed  )))))
     33                 (Tpointer (Tint I16 Signed  )))))
    3534             (Ssequence
    3635             (Ssequence
    3736             (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  ))))
     37                        (Tpointer (Tint I16 Signed  )))
     38               (Expr (Evar (ident_of_nat 20)) (Tpointer (Tint I16 Signed  ))))
    4139             (Sassign (Expr (Evar (ident_of_nat 20))
    42                         (Tpointer Any (Tint I16 Signed  )))
     40                        (Tpointer (Tint I16 Signed  )))
    4341               (Expr (Ebinop Oadd
    4442                 (Expr (Evar (ident_of_nat 18))
    45                    (Tpointer Any (Tint I16 Signed  )))
     43                   (Tpointer (Tint I16 Signed  )))
    4644                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    47                  (Tpointer Any (Tint I16 Signed  )))))
     45                 (Tpointer (Tint I16 Signed  )))))
    4846             (Sassign (Expr (Ederef
    4947                        (Expr (Evar (ident_of_nat 17))
    50                           (Tpointer Any (Tint I16 Signed  ))))
     48                          (Tpointer (Tint I16 Signed  ))))
    5149                        (Tint I16 Signed  ))
    5250               (Expr (Ederef
    5351                 (Expr (Evar (ident_of_nat 18))
    54                    (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
     52                   (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
    5553             (LScase I32 (repr ? 7)
    5654               (Ssequence
    5755               (Sassign (Expr (Evar (ident_of_nat 15))
    58                           (Tpointer Any (Tint I16 Signed  )))
     56                          (Tpointer (Tint I16 Signed  )))
    5957                 (Expr (Evar (ident_of_nat 19))
    60                    (Tpointer Any (Tint I16 Signed  ))))
     58                   (Tpointer (Tint I16 Signed  ))))
    6159               (Ssequence
    6260               (Sassign (Expr (Evar (ident_of_nat 19))
    63                           (Tpointer Any (Tint I16 Signed  )))
     61                          (Tpointer (Tint I16 Signed  )))
    6462                 (Expr (Ebinop Oadd
    6563                   (Expr (Evar (ident_of_nat 15))
    66                      (Tpointer Any (Tint I16 Signed  )))
     64                     (Tpointer (Tint I16 Signed  )))
    6765                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    68                    (Tpointer Any (Tint I16 Signed  ))))
     66                   (Tpointer (Tint I16 Signed  ))))
    6967               (Ssequence
    7068               (Sassign (Expr (Evar (ident_of_nat 16))
    71                           (Tpointer Any (Tint I16 Signed  )))
     69                          (Tpointer (Tint I16 Signed  )))
    7270                 (Expr (Evar (ident_of_nat 20))
    73                    (Tpointer Any (Tint I16 Signed  ))))
     71                   (Tpointer (Tint I16 Signed  ))))
    7472               (Ssequence
    7573               (Sassign (Expr (Evar (ident_of_nat 20))
    76                           (Tpointer Any (Tint I16 Signed  )))
     74                          (Tpointer (Tint I16 Signed  )))
    7775                 (Expr (Ebinop Oadd
    7876                   (Expr (Evar (ident_of_nat 16))
    79                      (Tpointer Any (Tint I16 Signed  )))
     77                     (Tpointer (Tint I16 Signed  )))
    8078                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    81                    (Tpointer Any (Tint I16 Signed  ))))
     79                   (Tpointer (Tint I16 Signed  ))))
    8280               (Sassign (Expr (Ederef
    8381                          (Expr (Evar (ident_of_nat 15))
    84                             (Tpointer Any (Tint I16 Signed  ))))
     82                            (Tpointer (Tint I16 Signed  ))))
    8583                          (Tint I16 Signed  ))
    8684                 (Expr (Ederef
    8785                   (Expr (Evar (ident_of_nat 16))
    88                      (Tpointer Any (Tint I16 Signed  ))))
    89                    (Tint I16 Signed  )))))))
     86                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
    9087               (LScase I32 (repr ? 6)
    9188                 (Ssequence
    9289                 (Sassign (Expr (Evar (ident_of_nat 13))
    93                             (Tpointer Any (Tint I16 Signed  )))
     90                            (Tpointer (Tint I16 Signed  )))
    9491                   (Expr (Evar (ident_of_nat 19))
    95                      (Tpointer Any (Tint I16 Signed  ))))
     92                     (Tpointer (Tint I16 Signed  ))))
    9693                 (Ssequence
    9794                 (Sassign (Expr (Evar (ident_of_nat 19))
    98                             (Tpointer Any (Tint I16 Signed  )))
     95                            (Tpointer (Tint I16 Signed  )))
    9996                   (Expr (Ebinop Oadd
    10097                     (Expr (Evar (ident_of_nat 13))
    101                        (Tpointer Any (Tint I16 Signed  )))
     98                       (Tpointer (Tint I16 Signed  )))
    10299                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    103                      (Tpointer Any (Tint I16 Signed  ))))
     100                     (Tpointer (Tint I16 Signed  ))))
    104101                 (Ssequence
    105102                 (Sassign (Expr (Evar (ident_of_nat 14))
    106                             (Tpointer Any (Tint I16 Signed  )))
     103                            (Tpointer (Tint I16 Signed  )))
    107104                   (Expr (Evar (ident_of_nat 20))
    108                      (Tpointer Any (Tint I16 Signed  ))))
     105                     (Tpointer (Tint I16 Signed  ))))
    109106                 (Ssequence
    110107                 (Sassign (Expr (Evar (ident_of_nat 20))
    111                             (Tpointer Any (Tint I16 Signed  )))
     108                            (Tpointer (Tint I16 Signed  )))
    112109                   (Expr (Ebinop Oadd
    113110                     (Expr (Evar (ident_of_nat 14))
    114                        (Tpointer Any (Tint I16 Signed  )))
     111                       (Tpointer (Tint I16 Signed  )))
    115112                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    116                      (Tpointer Any (Tint I16 Signed  ))))
     113                     (Tpointer (Tint I16 Signed  ))))
    117114                 (Sassign (Expr (Ederef
    118115                            (Expr (Evar (ident_of_nat 13))
    119                               (Tpointer Any (Tint I16 Signed  ))))
     116                              (Tpointer (Tint I16 Signed  ))))
    120117                            (Tint I16 Signed  ))
    121118                   (Expr (Ederef
    122119                     (Expr (Evar (ident_of_nat 14))
    123                        (Tpointer Any (Tint I16 Signed  ))))
    124                      (Tint I16 Signed  )))))))
     120                       (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
    125121                 (LScase I32 (repr ? 5)
    126122                   (Ssequence
    127123                   (Sassign (Expr (Evar (ident_of_nat 11))
    128                               (Tpointer Any (Tint I16 Signed  )))
     124                              (Tpointer (Tint I16 Signed  )))
    129125                     (Expr (Evar (ident_of_nat 19))
    130                        (Tpointer Any (Tint I16 Signed  ))))
     126                       (Tpointer (Tint I16 Signed  ))))
    131127                   (Ssequence
    132128                   (Sassign (Expr (Evar (ident_of_nat 19))
    133                               (Tpointer Any (Tint I16 Signed  )))
     129                              (Tpointer (Tint I16 Signed  )))
    134130                     (Expr (Ebinop Oadd
    135131                       (Expr (Evar (ident_of_nat 11))
    136                          (Tpointer Any (Tint I16 Signed  )))
     132                         (Tpointer (Tint I16 Signed  )))
    137133                       (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    138                        (Tpointer Any (Tint I16 Signed  ))))
     134                       (Tpointer (Tint I16 Signed  ))))
    139135                   (Ssequence
    140136                   (Sassign (Expr (Evar (ident_of_nat 12))
    141                               (Tpointer Any (Tint I16 Signed  )))
     137                              (Tpointer (Tint I16 Signed  )))
    142138                     (Expr (Evar (ident_of_nat 20))
    143                        (Tpointer Any (Tint I16 Signed  ))))
     139                       (Tpointer (Tint I16 Signed  ))))
    144140                   (Ssequence
    145141                   (Sassign (Expr (Evar (ident_of_nat 20))
    146                               (Tpointer Any (Tint I16 Signed  )))
     142                              (Tpointer (Tint I16 Signed  )))
    147143                     (Expr (Ebinop Oadd
    148144                       (Expr (Evar (ident_of_nat 12))
    149                          (Tpointer Any (Tint I16 Signed  )))
     145                         (Tpointer (Tint I16 Signed  )))
    150146                       (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    151                        (Tpointer Any (Tint I16 Signed  ))))
     147                       (Tpointer (Tint I16 Signed  ))))
    152148                   (Sassign (Expr (Ederef
    153149                              (Expr (Evar (ident_of_nat 11))
    154                                 (Tpointer Any (Tint I16 Signed  ))))
     150                                (Tpointer (Tint I16 Signed  ))))
    155151                              (Tint I16 Signed  ))
    156152                     (Expr (Ederef
    157153                       (Expr (Evar (ident_of_nat 12))
    158                          (Tpointer Any (Tint I16 Signed  ))))
     154                         (Tpointer (Tint I16 Signed  ))))
    159155                       (Tint I16 Signed  )))))))
    160156                   (LScase I32 (repr ? 4)
    161157                     (Ssequence
    162158                     (Sassign (Expr (Evar (ident_of_nat 9))
    163                                 (Tpointer Any (Tint I16 Signed  )))
     159                                (Tpointer (Tint I16 Signed  )))
    164160                       (Expr (Evar (ident_of_nat 19))
    165                          (Tpointer Any (Tint I16 Signed  ))))
     161                         (Tpointer (Tint I16 Signed  ))))
    166162                     (Ssequence
    167163                     (Sassign (Expr (Evar (ident_of_nat 19))
    168                                 (Tpointer Any (Tint I16 Signed  )))
     164                                (Tpointer (Tint I16 Signed  )))
    169165                       (Expr (Ebinop Oadd
    170166                         (Expr (Evar (ident_of_nat 9))
    171                            (Tpointer Any (Tint I16 Signed  )))
     167                           (Tpointer (Tint I16 Signed  )))
    172168                         (Expr (Econst_int I32 (repr ? 1))
    173169                           (Tint I32 Signed  )))
    174                          (Tpointer Any (Tint I16 Signed  ))))
     170                         (Tpointer (Tint I16 Signed  ))))
    175171                     (Ssequence
    176172                     (Sassign (Expr (Evar (ident_of_nat 10))
    177                                 (Tpointer Any (Tint I16 Signed  )))
     173                                (Tpointer (Tint I16 Signed  )))
    178174                       (Expr (Evar (ident_of_nat 20))
    179                          (Tpointer Any (Tint I16 Signed  ))))
     175                         (Tpointer (Tint I16 Signed  ))))
    180176                     (Ssequence
    181177                     (Sassign (Expr (Evar (ident_of_nat 20))
    182                                 (Tpointer Any (Tint I16 Signed  )))
     178                                (Tpointer (Tint I16 Signed  )))
    183179                       (Expr (Ebinop Oadd
    184180                         (Expr (Evar (ident_of_nat 10))
    185                            (Tpointer Any (Tint I16 Signed  )))
     181                           (Tpointer (Tint I16 Signed  )))
    186182                         (Expr (Econst_int I32 (repr ? 1))
    187183                           (Tint I32 Signed  )))
    188                          (Tpointer Any (Tint I16 Signed  ))))
     184                         (Tpointer (Tint I16 Signed  ))))
    189185                     (Sassign (Expr (Ederef
    190186                                (Expr (Evar (ident_of_nat 9))
    191                                   (Tpointer Any (Tint I16 Signed  ))))
     187                                  (Tpointer (Tint I16 Signed  ))))
    192188                                (Tint I16 Signed  ))
    193189                       (Expr (Ederef
    194190                         (Expr (Evar (ident_of_nat 10))
    195                            (Tpointer Any (Tint I16 Signed  ))))
     191                           (Tpointer (Tint I16 Signed  ))))
    196192                         (Tint I16 Signed  )))))))
    197193                     (LScase I32 (repr ? 3)
    198194                       (Ssequence
    199195                       (Sassign (Expr (Evar (ident_of_nat 7))
    200                                   (Tpointer Any (Tint I16 Signed  )))
     196                                  (Tpointer (Tint I16 Signed  )))
    201197                         (Expr (Evar (ident_of_nat 19))
    202                            (Tpointer Any (Tint I16 Signed  ))))
     198                           (Tpointer (Tint I16 Signed  ))))
    203199                       (Ssequence
    204200                       (Sassign (Expr (Evar (ident_of_nat 19))
    205                                   (Tpointer Any (Tint I16 Signed  )))
     201                                  (Tpointer (Tint I16 Signed  )))
    206202                         (Expr (Ebinop Oadd
    207203                           (Expr (Evar (ident_of_nat 7))
    208                              (Tpointer Any (Tint I16 Signed  )))
     204                             (Tpointer (Tint I16 Signed  )))
    209205                           (Expr (Econst_int I32 (repr ? 1))
    210206                             (Tint I32 Signed  )))
    211                            (Tpointer Any (Tint I16 Signed  ))))
     207                           (Tpointer (Tint I16 Signed  ))))
    212208                       (Ssequence
    213209                       (Sassign (Expr (Evar (ident_of_nat 8))
    214                                   (Tpointer Any (Tint I16 Signed  )))
     210                                  (Tpointer (Tint I16 Signed  )))
    215211                         (Expr (Evar (ident_of_nat 20))
    216                            (Tpointer Any (Tint I16 Signed  ))))
     212                           (Tpointer (Tint I16 Signed  ))))
    217213                       (Ssequence
    218214                       (Sassign (Expr (Evar (ident_of_nat 20))
    219                                   (Tpointer Any (Tint I16 Signed  )))
     215                                  (Tpointer (Tint I16 Signed  )))
    220216                         (Expr (Ebinop Oadd
    221217                           (Expr (Evar (ident_of_nat 8))
    222                              (Tpointer Any (Tint I16 Signed  )))
     218                             (Tpointer (Tint I16 Signed  )))
    223219                           (Expr (Econst_int I32 (repr ? 1))
    224220                             (Tint I32 Signed  )))
    225                            (Tpointer Any (Tint I16 Signed  ))))
     221                           (Tpointer (Tint I16 Signed  ))))
    226222                       (Sassign (Expr (Ederef
    227223                                  (Expr (Evar (ident_of_nat 7))
    228                                     (Tpointer Any (Tint I16 Signed  ))))
     224                                    (Tpointer (Tint I16 Signed  ))))
    229225                                  (Tint I16 Signed  ))
    230226                         (Expr (Ederef
    231227                           (Expr (Evar (ident_of_nat 8))
    232                              (Tpointer Any (Tint I16 Signed  ))))
     228                             (Tpointer (Tint I16 Signed  ))))
    233229                           (Tint I16 Signed  )))))))
    234230                       (LScase I32 (repr ? 2)
    235231                         (Ssequence
    236232                         (Sassign (Expr (Evar (ident_of_nat 5))
    237                                     (Tpointer Any (Tint I16 Signed  )))
     233                                    (Tpointer (Tint I16 Signed  )))
    238234                           (Expr (Evar (ident_of_nat 19))
    239                              (Tpointer Any (Tint I16 Signed  ))))
     235                             (Tpointer (Tint I16 Signed  ))))
    240236                         (Ssequence
    241237                         (Sassign (Expr (Evar (ident_of_nat 19))
    242                                     (Tpointer Any (Tint I16 Signed  )))
     238                                    (Tpointer (Tint I16 Signed  )))
    243239                           (Expr (Ebinop Oadd
    244240                             (Expr (Evar (ident_of_nat 5))
    245                                (Tpointer Any (Tint I16 Signed  )))
     241                               (Tpointer (Tint I16 Signed  )))
    246242                             (Expr (Econst_int I32 (repr ? 1))
    247243                               (Tint I32 Signed  )))
    248                              (Tpointer Any (Tint I16 Signed  ))))
     244                             (Tpointer (Tint I16 Signed  ))))
    249245                         (Ssequence
    250246                         (Sassign (Expr (Evar (ident_of_nat 6))
    251                                     (Tpointer Any (Tint I16 Signed  )))
     247                                    (Tpointer (Tint I16 Signed  )))
    252248                           (Expr (Evar (ident_of_nat 20))
    253                              (Tpointer Any (Tint I16 Signed  ))))
     249                             (Tpointer (Tint I16 Signed  ))))
    254250                         (Ssequence
    255251                         (Sassign (Expr (Evar (ident_of_nat 20))
    256                                     (Tpointer Any (Tint I16 Signed  )))
     252                                    (Tpointer (Tint I16 Signed  )))
    257253                           (Expr (Ebinop Oadd
    258254                             (Expr (Evar (ident_of_nat 6))
    259                                (Tpointer Any (Tint I16 Signed  )))
     255                               (Tpointer (Tint I16 Signed  )))
    260256                             (Expr (Econst_int I32 (repr ? 1))
    261257                               (Tint I32 Signed  )))
    262                              (Tpointer Any (Tint I16 Signed  ))))
     258                             (Tpointer (Tint I16 Signed  ))))
    263259                         (Sassign (Expr (Ederef
    264260                                    (Expr (Evar (ident_of_nat 5))
    265                                       (Tpointer Any (Tint I16 Signed  ))))
     261                                      (Tpointer (Tint I16 Signed  ))))
    266262                                    (Tint I16 Signed  ))
    267263                           (Expr (Ederef
    268264                             (Expr (Evar (ident_of_nat 6))
    269                                (Tpointer Any (Tint I16 Signed  ))))
     265                               (Tpointer (Tint I16 Signed  ))))
    270266                             (Tint I16 Signed  )))))))
    271267                         (LScase I32 (repr ? 1)
    272268                           (Ssequence
    273269                           (Sassign (Expr (Evar (ident_of_nat 3))
    274                                       (Tpointer Any (Tint I16 Signed  )))
     270                                      (Tpointer (Tint I16 Signed  )))
    275271                             (Expr (Evar (ident_of_nat 19))
    276                                (Tpointer Any (Tint I16 Signed  ))))
     272                               (Tpointer (Tint I16 Signed  ))))
    277273                           (Ssequence
    278274                           (Sassign (Expr (Evar (ident_of_nat 19))
    279                                       (Tpointer Any (Tint I16 Signed  )))
     275                                      (Tpointer (Tint I16 Signed  )))
    280276                             (Expr (Ebinop Oadd
    281277                               (Expr (Evar (ident_of_nat 3))
    282                                  (Tpointer Any (Tint I16 Signed  )))
     278                                 (Tpointer (Tint I16 Signed  )))
    283279                               (Expr (Econst_int I32 (repr ? 1))
    284280                                 (Tint I32 Signed  )))
    285                                (Tpointer Any (Tint I16 Signed  ))))
     281                               (Tpointer (Tint I16 Signed  ))))
    286282                           (Ssequence
    287283                           (Sassign (Expr (Evar (ident_of_nat 4))
    288                                       (Tpointer Any (Tint I16 Signed  )))
     284                                      (Tpointer (Tint I16 Signed  )))
    289285                             (Expr (Evar (ident_of_nat 20))
    290                                (Tpointer Any (Tint I16 Signed  ))))
     286                               (Tpointer (Tint I16 Signed  ))))
    291287                           (Ssequence
    292288                           (Sassign (Expr (Evar (ident_of_nat 20))
    293                                       (Tpointer Any (Tint I16 Signed  )))
     289                                      (Tpointer (Tint I16 Signed  )))
    294290                             (Expr (Ebinop Oadd
    295291                               (Expr (Evar (ident_of_nat 4))
    296                                  (Tpointer Any (Tint I16 Signed  )))
     292                                 (Tpointer (Tint I16 Signed  )))
    297293                               (Expr (Econst_int I32 (repr ? 1))
    298294                                 (Tint I32 Signed  )))
    299                                (Tpointer Any (Tint I16 Signed  ))))
     295                               (Tpointer (Tint I16 Signed  ))))
    300296                           (Ssequence
    301297                           (Sassign (Expr (Ederef
    302298                                      (Expr (Evar (ident_of_nat 3))
    303                                         (Tpointer Any (Tint I16 Signed  ))))
     299                                        (Tpointer (Tint I16 Signed  ))))
    304300                                      (Tint I16 Signed  ))
    305301                             (Expr (Ederef
    306302                               (Expr (Evar (ident_of_nat 4))
    307                                  (Tpointer Any (Tint I16 Signed  ))))
     303                                 (Tpointer (Tint I16 Signed  ))))
    308304                               (Tint I16 Signed  )))
    309305                           (Ssequence
    … …  
    336332     )〉;
    337333    〈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)〉 ]
     334      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 24, (Tarray (Tint I16 Signed  ) 3)〉 ; 〈ident_of_nat 25, (Tarray (Tint I16 Signed  ) 3)〉 ]
    339335        (Ssequence
    340336        (Sassign (Expr (Ederef
    341337                   (Expr (Ebinop Oadd
    342338                     (Expr (Evar (ident_of_nat 24))
    343                        (Tarray Any (Tint I16 Signed  ) 3))
     339                       (Tarray (Tint I16 Signed  ) 3))
    344340                     (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    345                      (Tpointer Any (Tint I16 Signed  ))))
    346                    (Tint I16 Signed  ))
     341                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))
    347342          (Expr (Ecast (Tint I16 Signed  )
    348343            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    … …  
    352347                   (Expr (Ebinop Oadd
    353348                     (Expr (Evar (ident_of_nat 24))
    354                        (Tarray Any (Tint I16 Signed  ) 3))
     349                       (Tarray (Tint I16 Signed  ) 3))
    355350                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    356                      (Tpointer Any (Tint I16 Signed  ))))
    357                    (Tint I16 Signed  ))
     351                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))
    358352          (Expr (Ecast (Tint I16 Signed  )
    359353            (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    … …  
    363357                   (Expr (Ebinop Oadd
    364358                     (Expr (Evar (ident_of_nat 24))
    365                        (Tarray Any (Tint I16 Signed  ) 3))
     359                       (Tarray (Tint I16 Signed  ) 3))
    366360                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    367                      (Tpointer Any (Tint I16 Signed  ))))
    368                    (Tint I16 Signed  ))
     361                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))
    369362          (Expr (Ecast (Tint I16 Signed  )
    370363            (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
    … …  
    372365        (Ssequence
    373366        (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));
     367                             (Tfunction (Tcons (Tpointer (Tint I16 Signed  )) (Tcons (Tpointer (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid))
     368          [(Expr (Evar (ident_of_nat 25)) (Tarray (Tint I16 Signed  ) 3));
     369          (Expr (Evar (ident_of_nat 24)) (Tarray (Tint I16 Signed  ) 3));
    377370          (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  ))])
    378371        (Sreturn (Some expr (Expr (Ebinop Oadd
    … …  
    382375                                    (Expr (Ebinop Oadd
    383376                                      (Expr (Evar (ident_of_nat 25))
    384                                         (Tarray Any (Tint I16 Signed  ) 3))
     377                                        (Tarray (Tint I16 Signed  ) 3))
    385378                                      (Expr (Econst_int I32 (repr ? 0))
    386379                                        (Tint I32 Signed  )))
    387                                       (Tpointer Any (Tint I16 Signed  ))))
     380                                      (Tpointer (Tint I16 Signed  ))))
    388381                                    (Tint I16 Signed  )))
    389382                                  (Tint I32 Signed  ))
    … …  
    392385                                    (Expr (Ebinop Oadd
    393386                                      (Expr (Evar (ident_of_nat 25))
    394                                         (Tarray Any (Tint I16 Signed  ) 3))
     387                                        (Tarray (Tint I16 Signed  ) 3))
    395388                                      (Expr (Econst_int I32 (repr ? 1))
    396389                                        (Tint I32 Signed  )))
    397                                       (Tpointer Any (Tint I16 Signed  ))))
     390                                      (Tpointer (Tint I16 Signed  ))))
    398391                                    (Tint I16 Signed  )))
    399392                                  (Tint I32 Signed  ))) (Tint I32 Signed  ))
    … …  
    402395                                  (Expr (Ebinop Oadd
    403396                                    (Expr (Evar (ident_of_nat 25))
    404                                       (Tarray Any (Tint I16 Signed  ) 3))
     397                                      (Tarray (Tint I16 Signed  ) 3))
    405398                                    (Expr (Econst_int I32 (repr ? 2))
    406399                                      (Tint I32 Signed  )))
    407                                     (Tpointer Any (Tint I16 Signed  ))))
     400                                    (Tpointer (Tint I16 Signed  ))))
    408401                                  (Tint I16 Signed  ))) (Tint I32 Signed  )))
    409402                              (Tint I32 Signed  ))))))))

  • src/Clight/test/insertsort.c.ma

    r1513 r2176  
    66
    77definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
    8   [〈〈ident_of_nat 3 (* l6 *), Any〉,
     8  [〈〈ident_of_nat 3 (* l6 *), XData〉,
    99     〈[(Init_int8 (repr I8 69)) ; (Init_space 3) ;
    10         (Init_null Any) ],
    11      (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    12   〈〈ident_of_nat 4 (* l5 *), Any〉,
     10        (Init_null) ],
     11     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     12  〈〈ident_of_nat 4 (* l5 *), XData〉,
    1313    〈[(Init_int8 (repr I8 36)) ; (Init_space 3) ;
    14        (Init_addrof Any (ident_of_nat 3) 0)],
    15     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    16   〈〈ident_of_nat 5 (* l4 *), Any〉,
     14       (Init_addrof (ident_of_nat 3) 0)],
     15    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     16  〈〈ident_of_nat 5 (* l4 *), XData〉,
    1717    〈[(Init_int8 (repr I8 136)) ; (Init_space 3) ;
    18        (Init_addrof Any (ident_of_nat 4) 0)],
    19     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    20   〈〈ident_of_nat 6 (* l3 *), Any〉,
     18       (Init_addrof (ident_of_nat 4) 0)],
     19    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     20  〈〈ident_of_nat 6 (* l3 *), XData〉,
    2121    〈[(Init_int8 (repr I8 105)) ; (Init_space 3) ;
    22        (Init_addrof Any (ident_of_nat 5) 0)],
    23     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    24   〈〈ident_of_nat 7 (* l2 *), Any〉,
     22       (Init_addrof (ident_of_nat 5) 0)],
     23    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     24  〈〈ident_of_nat 7 (* l2 *), XData〉,
    2525    〈[(Init_int8 (repr I8 234)) ; (Init_space 3) ;
    26        (Init_addrof Any (ident_of_nat 6) 0)],
    27     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    28   〈〈ident_of_nat 8 (* l1 *), Any〉,
     26       (Init_addrof (ident_of_nat 6) 0)],
     27    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     28  〈〈ident_of_nat 8 (* l1 *), XData〉,
    2929    〈[(Init_int8 (repr I8 240)) ; (Init_space 3) ;
    30        (Init_addrof Any (ident_of_nat 7) 0)],
    31     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    32   〈〈ident_of_nat 9 (* l0 *), Any〉,
     30       (Init_addrof (ident_of_nat 7) 0)],
     31    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     32  〈〈ident_of_nat 9 (* l0 *), XData〉,
    3333    〈[(Init_int8 (repr I8 102)) ; (Init_space 3) ;
    34        (Init_addrof Any (ident_of_nat 8) 0)],
    35     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉]
     34       (Init_addrof (ident_of_nat 8) 0)],
     35    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉]
    3636  [〈ident_of_nat 10 (* insert *), CL_Internal (
    37      mk_function Tvoid [〈ident_of_nat 12, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 11, (Tint I32 Signed  )〉 ]
     37     mk_function Tvoid [〈ident_of_nat 12, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 13, (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 11, (Tint I32 Signed  )〉 ]
    3838       (Ssequence
    3939       (Sifthenelse (Expr (Ebinop Oeq
    4040                      (Expr (Ederef
    4141                        (Expr (Evar (ident_of_nat 13))
    42                           (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    43                         (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    44                       (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))
    45                         (Expr (Ecast (Tpointer Any Tvoid)
     42                          (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     43                        (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
     44                      (Expr (Ecast (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))
     45                        (Expr (Ecast (Tpointer Tvoid)
    4646                          (Expr (Econst_int I8 (repr ? 0))
    47                             (Tint I8 Unsigned ))) (Tpointer Any Tvoid)))
    48                         (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     47                            (Tint I8 Unsigned ))) (Tpointer Tvoid)))
     48                        (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    4949                      (Tint I32 Signed  ))
    5050         (Sassign (Expr (Evar (ident_of_nat 11)) (Tint I32 Signed  ))
    … …  
    5757                                 (Expr (Ederef
    5858                                   (Expr (Evar (ident_of_nat 13))
    59                                      (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    60                                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    61                                  (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
     59                                     (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     60                                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     61                                 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    6262                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    6363               (Expr (Ecast (Tint I32 Signed  )
    6464                 (Expr (Efield (Expr (Ederef
    6565                                 (Expr (Evar (ident_of_nat 12))
    66                                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    67                                  (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
     66                                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     67                                 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    6868                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    6969               (Tint I32 Signed  ))
    … …  
    7474         (Sassign (Expr (Efield (Expr (Ederef
    7575                                  (Expr (Evar (ident_of_nat 12))
    76                                     (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    77                                   (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
    78                     (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     76                                    (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     77                                  (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     78                    (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    7979           (Expr (Ederef
    8080             (Expr (Evar (ident_of_nat 13))
    81                (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    82              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     81               (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     82             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    8383         (Sassign (Expr (Ederef
    8484                    (Expr (Evar (ident_of_nat 13))
    85                       (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    86                     (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     85                      (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     86                    (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    8787           (Expr (Evar (ident_of_nat 12))
    88              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
     88             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
    8989         (Scall (None expr) (Expr (Evar (ident_of_nat 10))
    90                               (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
     90                              (Tfunction (Tcons (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
    9191           [(Expr (Evar (ident_of_nat 12))
    92               (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))));
     92              (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))));
    9393           (Expr (Eaddrof
    9494             (Expr (Efield (Expr (Ederef
    9595                             (Expr (Ederef
    9696                               (Expr (Evar (ident_of_nat 13))
    97                                  (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    98                                (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    99                              (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
    100                (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    101              (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))])))
     97                                 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     98                               (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     99                             (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     100               (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     101             (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))])))
    102102     
    103103     
    … …  
    105105   )〉;
    106106  〈ident_of_nat 14 (* sort *), CL_Internal (
    107     mk_function Tvoid [〈ident_of_nat 17, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 15, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 2, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ]
     107    mk_function Tvoid [〈ident_of_nat 17, (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 15, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 2, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 16, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ]
    108108      (Ssequence
    109109      (Sassign (Expr (Evar (ident_of_nat 2))
    110                  (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     110                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    111111        (Expr (Ederef
    112112          (Expr (Evar (ident_of_nat 17))
    113             (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    114           (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     113            (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     114          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    115115      (Ssequence
    116116      (Sassign (Expr (Evar (ident_of_nat 16))
    117                  (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    118         (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))
     117                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
     118        (Expr (Ecast (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))
    119119          (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    120           (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     120          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    121121      (Ssequence
    122122      (Swhile (Expr (Evar (ident_of_nat 2))
    123                 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     123                (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    124124        (Ssequence
    125125        (Sassign (Expr (Evar (ident_of_nat 15))
    126                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     126                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    127127          (Expr (Evar (ident_of_nat 2))
    128             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     128            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    129129        (Ssequence
    130130        (Sassign (Expr (Evar (ident_of_nat 2))
    131                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     131                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    132132          (Expr (Efield (Expr (Ederef
    133133                          (Expr (Evar (ident_of_nat 2))
    134                             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    135                           (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
    136             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     134                            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     135                          (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     136            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    137137        (Scall (None expr) (Expr (Evar (ident_of_nat 10))
    138                              (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
     138                             (Tfunction (Tcons (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
    139139          [(Expr (Evar (ident_of_nat 15))
    140              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))));
     140             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))));
    141141          (Expr (Eaddrof
    142142            (Expr (Evar (ident_of_nat 16))
    143               (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    144             (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))]))))
     143              (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     144            (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))]))))
    145145      (Sassign (Expr (Ederef
    146146                 (Expr (Evar (ident_of_nat 17))
    147                    (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    148                  (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     147                   (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     148                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    149149        (Expr (Evar (ident_of_nat 16))
    150           (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))))
     150          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))))
    151151   
    152152   
    … …  
    155155  〈ident_of_nat 18 (* out *), CL_External (ident_of_nat 18) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;
    156156  〈ident_of_nat 19 (* main *), CL_Internal (
    157     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 20, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ]
     157    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 20, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ]
    158158      (Ssequence
    159159      (Sassign (Expr (Evar (ident_of_nat 20))
    160                  (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     160                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    161161        (Expr (Eaddrof
    162162          (Expr (Evar (ident_of_nat 9))
    163             (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    164           (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     163            (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
     164          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    165165      (Ssequence
    166166      (Scall (None expr) (Expr (Evar (ident_of_nat 14))
    167                            (Tfunction (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil) Tvoid))
     167                           (Tfunction (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil) Tvoid))
    168168        [(Expr (Eaddrof
    169169           (Expr (Evar (ident_of_nat 20))
    170              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    171            (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))])
     170             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     171           (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))])
    172172      (Ssequence
    173173      (Swhile (Expr (Evar (ident_of_nat 20))
    174                 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     174                (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    175175        (Ssequence
    176176        (Scall (None expr) (Expr (Evar (ident_of_nat 18))
    … …  
    178178          [(Expr (Efield (Expr (Ederef
    179179                           (Expr (Evar (ident_of_nat 20))
    180                              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    181                            (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
     180                             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     181                           (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    182182             (Tint I8 Unsigned ))])
    183183        (Sassign (Expr (Evar (ident_of_nat 20))
    184                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     184                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    185185          (Expr (Efield (Expr (Ederef
    186186                          (Expr (Evar (ident_of_nat 20))
    187                             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    188                           (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
    189             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))))
     187                            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     188                          (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     189            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))))
    190190      (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
    191191                            (Tint I32 Signed  )))))))

  • src/Clight/test/memorymodel.ma

    r1993 r2176  
    2121   store. *)
    2222definition store0 := empty.
    23 definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 Any.
     23definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 XData.
    2424definition store1 : mem ≝ fst ?? store1block.
    2525definition block :block := pi1 … (snd ?? store1block).
    … …  
    2727(* write a value *)
    2828definition store2 : mem.
    29   letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer Any block (same_compat …) zero_offset) (Vint I16 (repr ? 1)));
     29  letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer block zero_offset) (Vint I16 (repr ? 1)))
    3030
    3131  lapply (refl ? r); elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
    … …  
    3434(* overwrite the first byte of the value *)
    3535definition store3 : mem.
    36   letin r ≝ (store (ASTint I8 Unsigned) store2 (mk_pointer Any block (same_compat …) zero_offset) (Vint I8 (repr ? 1)));
     36  letin r ≝ (store (ASTint I8 Unsigned) store2 (mk_pointer block zero_offset) (Vint I8 (repr ? 1)))
    3737
    3838  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
    … …  
    4141(* This is what happened under the original CompCert 1.6 ported memory model:
    4242   The size checking rejects the read and gives us Some Vundef.
    43 example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? Vundef. @refl qed.
     43example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? Vundef. @refl qed.
    4444*)
    4545(* Now we do byte-wise values and get to see the altered integer. *)
    46 example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.
     46example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.
    4747
    4848(* The read is successful and returns the value. *)
    49 example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed.
     49example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer block zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed.
    5050
    5151(* NB: Double frees are allowed by the memory model (although not necessarily
    … …  
    5757   stack memory in the semantics. *)
    5858definition storeA := empty.
    59 definition storeBblkB := alloc storeA 0 4 Any.
    60 definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
     59definition storeBblkB := alloc storeA 0 4 XData.
     60definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 XData.
    6161definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
    6262definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
    … …  
    6767   doesn't currently expose parts of pointers. *)
    6868definition storeI := empty.
    69 definition storeIIblk := alloc storeI 0 4 Any.
     69definition storeIIblk := alloc storeI 0 4 XData.
    7070definition storeIII : mem.
    71  letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset) (Vint I32 (repr ? 1)));
     71 letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer (snd ?? storeIIblk) zero_offset) (Vint I32 (repr ? 1)));
    7272  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
    7373  | #rr #_ @rr ] qed.
    74 definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset).
     74definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer (snd ?? storeIIblk) zero_offset).
    7575example byteundef: byte = Some ? (Vint I8 (repr ? 0)). // qed. (* :) *)
     76

  • src/Clight/test/null-op.c.ma

    r1513 r2176  
    44definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
    55  [][〈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 ))〉 ]
     6       mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer (Tint I8 Unsigned ))〉 ]
    77         (Ssequence
    88         (Sassign (Expr (Evar (ident_of_nat 2))
    9                     (Tpointer Any (Tint I8 Unsigned )))
    10            (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
     9                    (Tpointer (Tint I8 Unsigned )))
     10           (Expr (Ecast (Tpointer (Tint I8 Unsigned ))
    1111             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    12              (Tpointer Any (Tint I8 Unsigned ))))
     12             (Tpointer (Tint I8 Unsigned ))))
    1313         (Ssequence
    1414         (Sassign (Expr (Evar (ident_of_nat 3))
    15                     (Tpointer Any (Tint I8 Unsigned )))
     15                    (Tpointer (Tint I8 Unsigned )))
    1616           (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    17              (Tpointer Any (Tint I8 Unsigned ))))
     17             (Tpointer (Tint I8 Unsigned ))))
    1818         (Ssequence
    1919         (Sifthenelse (Expr (Ebinop Oeq
    2020                        (Expr (Evar (ident_of_nat 2))
    21                           (Tpointer Any (Tint I8 Unsigned )))
     21                          (Tpointer (Tint I8 Unsigned )))
    2222                        (Expr (Evar (ident_of_nat 3))
    23                           (Tpointer Any (Tint I8 Unsigned ))))
     23                          (Tpointer (Tint I8 Unsigned ))))
    2424                        (Tint I32 Signed  ))
    2525           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
    … …  
    3030                        (Expr (Ebinop Osub
    3131                          (Expr (Evar (ident_of_nat 2))
    32                             (Tpointer Any (Tint I8 Unsigned )))
     32                            (Tpointer (Tint I8 Unsigned )))
    3333                          (Expr (Evar (ident_of_nat 2))
    34                             (Tpointer Any (Tint I8 Unsigned ))))
     34                            (Tpointer (Tint I8 Unsigned ))))
    3535                          (Tint I32 Signed  ))
    3636                        (Expr (Econst_int I32 (repr ? 0))
    … …  
    4141         (Ssequence
    4242         (Sassign (Expr (Evar (ident_of_nat 2))
    43                     (Tpointer Any (Tint I8 Unsigned )))
     43                    (Tpointer (Tint I8 Unsigned )))
    4444           (Expr (Ebinop Oadd
    45              (Expr (Evar (ident_of_nat 2))
    46                (Tpointer Any (Tint I8 Unsigned )))
     45             (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned )))
    4746             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    48              (Tpointer Any (Tint I8 Unsigned ))))
     47             (Tpointer (Tint I8 Unsigned ))))
    4948         (Ssequence
    5049         (Sassign (Expr (Evar (ident_of_nat 2))
    51                     (Tpointer Any (Tint I8 Unsigned )))
     50                    (Tpointer (Tint I8 Unsigned )))
    5251           (Expr (Ebinop Oadd
    5352             (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 ))))
     53             (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned ))))
     54             (Tpointer (Tint I8 Unsigned ))))
    5755         (Ssequence
    5856         (Sassign (Expr (Evar (ident_of_nat 2))
    59                     (Tpointer Any (Tint I8 Unsigned )))
     57                    (Tpointer (Tint I8 Unsigned )))
    6058           (Expr (Ebinop Osub
    61              (Expr (Evar (ident_of_nat 2))
    62                (Tpointer Any (Tint I8 Unsigned )))
     59             (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned )))
    6360             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    64              (Tpointer Any (Tint I8 Unsigned ))))
     61             (Tpointer (Tint I8 Unsigned ))))
    6562         (Sreturn (Some expr (Expr (Ebinop Oeq
    6663                               (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)
     64                                 (Tpointer (Tint I8 Unsigned )))
     65                               (Expr (Ecast (Tpointer (Tint I8 Unsigned ))
     66                                 (Expr (Ecast (Tpointer Tvoid)
    7067                                   (Expr (Econst_int I8 (repr ? 0))
    71                                      (Tint I8 Unsigned )))
    72                                    (Tpointer Any Tvoid)))
    73                                  (Tpointer Any (Tint I8 Unsigned ))))
     68                                     (Tint I8 Unsigned ))) (Tpointer Tvoid)))
     69                                 (Tpointer (Tint I8 Unsigned ))))
    7470                               (Tint I32 Signed  )))))))))))
    7571       

  • src/Clight/test/search.c.ma

    r1991 r2176  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program (λ_.clight_fundef) ((list init_data) × type)
    5   []
    6   [〈ident_of_nat 0 (* search *), CL_Internal (
    7      mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
    8        (Ssequence
    9        (Sassign (Expr (Evar (ident_of_nat 1)) (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        (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    15          (Expr (Ecast (Tint I8 Unsigned )
    16            (Expr (Ebinop Osub
    17              (Expr (Ecast (Tint I32 Signed  )
    18                (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
    19                (Tint I32 Signed  ))
    20              (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    21              (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    22        (Ssequence
    23        (Swhile (Expr (Ebinop Oge
    24                  (Expr (Ecast (Tint I32 Signed  )
    25                    (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    26                    (Tint I32 Signed  ))
    27                  (Expr (Ecast (Tint I32 Signed  )
    28                    (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    29                    (Tint I32 Signed  ))) (Tint I32 Signed  ))
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [][〈ident_of_nat 0 (* search *), CL_Internal (
     6       mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
    307         (Ssequence
    31          (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
     8         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    329           (Expr (Ecast (Tint I8 Unsigned )
    33              (Expr (Ebinop Odiv
    34                (Expr (Ebinop Oadd
    35                  (Expr (Ecast (Tint I32 Signed  )
    36                    (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    37                    (Tint I32 Signed  ))
    38                  (Expr (Ecast (Tint I32 Signed  )
    39                    (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    40                    (Tint I32 Signed  ))) (Tint I32 Signed  ))
    41                (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     10             (Expr (Econst_int I32 (repr ? 0)) (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 (Ebinop Osub
     16               (Expr (Ecast (Tint I32 Signed  )
     17                 (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
     18                 (Tint I32 Signed  ))
     19               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    4220               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    4321         (Ssequence
    44          (Sifthenelse (Expr (Ebinop Oeq
    45                         (Expr (Ecast (Tint I32 Signed  )
    46                           (Expr (Ederef
    47                             (Expr (Ebinop Oadd
    48                               (Expr (Evar (ident_of_nat 4))
    49                                 (Tpointer Any (Tint I8 Unsigned )))
    50                               (Expr (Evar (ident_of_nat 3))
    51                                 (Tint I8 Unsigned )))
    52                               (Tpointer Any (Tint I8 Unsigned ))))
    53                             (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    54                         (Expr (Ecast (Tint I32 Signed  )
    55                           (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned )))
    56                           (Tint I32 Signed  ))) (Tint I32 Signed  ))
    57            (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
    58                                  (Tint I8 Unsigned ))))
    59            Sskip)
    60          (Ssequence
    61          (Sifthenelse (Expr (Ebinop Ogt
    62                         (Expr (Ecast (Tint I32 Signed  )
    63                           (Expr (Ederef
    64                             (Expr (Ebinop Oadd
    65                               (Expr (Evar (ident_of_nat 4))
    66                                 (Tpointer Any (Tint I8 Unsigned )))
    67                               (Expr (Evar (ident_of_nat 3))
    68                                 (Tint I8 Unsigned )))
    69                               (Tpointer Any (Tint I8 Unsigned ))))
    70                             (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    71                         (Expr (Ecast (Tint I32 Signed  )
    72                           (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned )))
    73                           (Tint I32 Signed  ))) (Tint I32 Signed  ))
    74            (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     22         (Swhile (Expr (Ebinop Oge
     23                   (Expr (Ecast (Tint I32 Signed  )
     24                     (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
     25                     (Tint I32 Signed  ))
     26                   (Expr (Ecast (Tint I32 Signed  )
     27                     (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
     28                     (Tint I32 Signed  ))) (Tint I32 Signed  ))
     29           (Ssequence
     30           (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    7531             (Expr (Ecast (Tint I8 Unsigned )
    76                (Expr (Ebinop Osub
    77                  (Expr (Ecast (Tint I32 Signed  )
    78                    (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    79                    (Tint I32 Signed  ))
    80                  (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     32               (Expr (Ebinop Odiv
     33                 (Expr (Ebinop Oadd
     34                   (Expr (Ecast (Tint I32 Signed  )
     35                     (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
     36                     (Tint I32 Signed  ))
     37                   (Expr (Ecast (Tint I32 Signed  )
     38                     (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
     39                     (Tint I32 Signed  ))) (Tint I32 Signed  ))
     40                 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    8141                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    82            Sskip)
    83          (Sifthenelse (Expr (Ebinop Olt
    84                         (Expr (Ecast (Tint I32 Signed  )
    85                           (Expr (Ederef
    86                             (Expr (Ebinop Oadd
    87                               (Expr (Evar (ident_of_nat 4))
    88                                 (Tpointer Any (Tint I8 Unsigned )))
    89                               (Expr (Evar (ident_of_nat 3))
    90                                 (Tint I8 Unsigned )))
    91                               (Tpointer Any (Tint I8 Unsigned ))))
    92                             (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    93                         (Expr (Ecast (Tint I32 Signed  )
    94                           (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned )))
    95                           (Tint I32 Signed  ))) (Tint I32 Signed  ))
    96            (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    97              (Expr (Ecast (Tint I8 Unsigned )
    98                (Expr (Ebinop Oadd
    99                  (Expr (Ecast (Tint I32 Signed  )
    100                    (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    101                    (Tint I32 Signed  ))
    102                  (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    103                  (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    104            Sskip)))))
    105        (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
    106                              (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
    107                                                  (Tint I32 Signed  )))
    108                                (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
    109      
    110      
    111      
    112    )〉;
    113   〈ident_of_nat 7 (* main *), CL_Internal (
    114     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ]
    115       (Ssequence
    116       (Sassign (Expr (Ederef
     42           (Ssequence
     43           (Sifthenelse (Expr (Ebinop Oeq
     44                          (Expr (Ecast (Tint I32 Signed  )
     45                            (Expr (Ederef
     46                              (Expr (Ebinop Oadd
     47                                (Expr (Evar (ident_of_nat 4))
     48                                  (Tpointer (Tint I8 Unsigned )))
     49                                (Expr (Evar (ident_of_nat 3))
     50                                  (Tint I8 Unsigned )))
     51                                (Tpointer (Tint I8 Unsigned ))))
     52                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
     53                          (Expr (Ecast (Tint I32 Signed  )
     54                            (Expr (Evar (ident_of_nat 6))
     55                              (Tint I8 Unsigned ))) (Tint I32 Signed  )))
     56                          (Tint I32 Signed  ))
     57             (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
     58                                   (Tint I8 Unsigned ))))
     59             Sskip)
     60           (Ssequence
     61           (Sifthenelse (Expr (Ebinop Ogt
     62                          (Expr (Ecast (Tint I32 Signed  )
     63                            (Expr (Ederef
     64                              (Expr (Ebinop Oadd
     65                                (Expr (Evar (ident_of_nat 4))
     66                                  (Tpointer (Tint I8 Unsigned )))
     67                                (Expr (Evar (ident_of_nat 3))
     68                                  (Tint I8 Unsigned )))
     69                                (Tpointer (Tint I8 Unsigned ))))
     70                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
     71                          (Expr (Ecast (Tint I32 Signed  )
     72                            (Expr (Evar (ident_of_nat 6))
     73                              (Tint I8 Unsigned ))) (Tint I32 Signed  )))
     74                          (Tint I32 Signed  ))
     75             (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     76               (Expr (Ecast (Tint I8 Unsigned )
     77                 (Expr (Ebinop Osub
     78                   (Expr (Ecast (Tint I32 Signed  )
     79                     (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
     80                     (Tint I32 Signed  ))
     81                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     82                   (Tint I32 Signed  ))) (Tint I8 Unsigned )))
     83             Sskip)
     84           (Sifthenelse (Expr (Ebinop Olt
     85                          (Expr (Ecast (Tint I32 Signed  )
     86                            (Expr (Ederef
     87                              (Expr (Ebinop Oadd
     88                                (Expr (Evar (ident_of_nat 4))
     89                                  (Tpointer (Tint I8 Unsigned )))
     90                                (Expr (Evar (ident_of_nat 3))
     91                                  (Tint I8 Unsigned )))
     92                                (Tpointer (Tint I8 Unsigned ))))
     93                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
     94                          (Expr (Ecast (Tint I32 Signed  )
     95                            (Expr (Evar (ident_of_nat 6))
     96                              (Tint I8 Unsigned ))) (Tint I32 Signed  )))
     97                          (Tint I32 Signed  ))
     98             (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
     99               (Expr (Ecast (Tint I8 Unsigned )
    117100                 (Expr (Ebinop Oadd
    118                    (Expr (Evar (ident_of_nat 4))
    119                      (Tarray Any (Tint I8 Unsigned ) 5))
    120                    (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    121                    (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
    122         (Expr (Ecast (Tint I8 Unsigned )
    123           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    124           (Tint I8 Unsigned )))
    125       (Ssequence
    126       (Sassign (Expr (Ederef
    127                  (Expr (Ebinop Oadd
    128                    (Expr (Evar (ident_of_nat 4))
    129                      (Tarray Any (Tint I8 Unsigned ) 5))
     101                   (Expr (Ecast (Tint I32 Signed  )
     102                     (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
     103                     (Tint I32 Signed  ))
    130104                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    131                    (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
    132         (Expr (Ecast (Tint I8 Unsigned )
    133           (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed  )))
    134           (Tint I8 Unsigned )))
    135       (Ssequence
    136       (Sassign (Expr (Ederef
    137                  (Expr (Ebinop Oadd
    138                    (Expr (Evar (ident_of_nat 4))
    139                      (Tarray Any (Tint I8 Unsigned ) 5))
    140                    (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    141                    (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
    142         (Expr (Ecast (Tint I8 Unsigned )
    143           (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed  )))
    144           (Tint I8 Unsigned )))
    145       (Ssequence
    146       (Sassign (Expr (Ederef
    147                  (Expr (Ebinop Oadd
    148                    (Expr (Evar (ident_of_nat 4))
    149                      (Tarray Any (Tint I8 Unsigned ) 5))
    150                    (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
    151                    (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
    152         (Expr (Ecast (Tint I8 Unsigned )
    153           (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
    154           (Tint I8 Unsigned )))
    155       (Ssequence
    156       (Sassign (Expr (Ederef
    157                  (Expr (Ebinop Oadd
    158                    (Expr (Evar (ident_of_nat 4))
    159                      (Tarray Any (Tint I8 Unsigned ) 5))
    160                    (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
    161                    (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
    162         (Expr (Ecast (Tint I8 Unsigned )
    163           (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed  )))
    164           (Tint I8 Unsigned )))
    165       (Ssequence
    166       (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned )))
    167         (Expr (Evar (ident_of_nat 0))
    168           (Tfunction (Tcons (Tpointer Any (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned )))
    169         [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
    170         (Expr (Ecast (Tint I8 Unsigned )
    171           (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
    172           (Tint I8 Unsigned ));
    173         (Expr (Ecast (Tint I8 Unsigned )
    174           (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
    175           (Tint I8 Unsigned ))])
    176       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    177                             (Expr (Evar (ident_of_nat 8))
    178                               (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))))))
    179    
    180    
    181    
    182   )〉]
     105                   (Tint I32 Signed  ))) (Tint I8 Unsigned )))
     106             Sskip)))))
     107         (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
     108                               (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
     109                                                   (Tint I32 Signed  )))
     110                                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
     111       
     112       
     113       
     114     )〉;
     115    〈ident_of_nat 7 (* main *), CL_Internal (
     116      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 4, (Tarray (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ]
     117        (Ssequence
     118        (Sassign (Expr (Ederef
     119                   (Expr (Ebinop Oadd
     120                     (Expr (Evar (ident_of_nat 4))
     121                       (Tarray (Tint I8 Unsigned ) 5))
     122                     (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     123                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
     124          (Expr (Ecast (Tint I8 Unsigned )
     125            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     126            (Tint I8 Unsigned )))
     127        (Ssequence
     128        (Sassign (Expr (Ederef
     129                   (Expr (Ebinop Oadd
     130                     (Expr (Evar (ident_of_nat 4))
     131                       (Tarray (Tint I8 Unsigned ) 5))
     132                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     133                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
     134          (Expr (Ecast (Tint I8 Unsigned )
     135            (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed  )))
     136            (Tint I8 Unsigned )))
     137        (Ssequence
     138        (Sassign (Expr (Ederef
     139                   (Expr (Ebinop Oadd
     140                     (Expr (Evar (ident_of_nat 4))
     141                       (Tarray (Tint I8 Unsigned ) 5))
     142                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     143                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
     144          (Expr (Ecast (Tint I8 Unsigned )
     145            (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed  )))
     146            (Tint I8 Unsigned )))
     147        (Ssequence
     148        (Sassign (Expr (Ederef
     149                   (Expr (Ebinop Oadd
     150                     (Expr (Evar (ident_of_nat 4))
     151                       (Tarray (Tint I8 Unsigned ) 5))
     152                     (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
     153                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
     154          (Expr (Ecast (Tint I8 Unsigned )
     155            (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
     156            (Tint I8 Unsigned )))
     157        (Ssequence
     158        (Sassign (Expr (Ederef
     159                   (Expr (Ebinop Oadd
     160                     (Expr (Evar (ident_of_nat 4))
     161                       (Tarray (Tint I8 Unsigned ) 5))
     162                     (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
     163                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
     164          (Expr (Ecast (Tint I8 Unsigned )
     165            (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed  )))
     166            (Tint I8 Unsigned )))
     167        (Ssequence
     168        (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned )))
     169          (Expr (Evar (ident_of_nat 0))
     170            (Tfunction (Tcons (Tpointer (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned )))
     171          [(Expr (Evar (ident_of_nat 4)) (Tarray (Tint I8 Unsigned ) 5));
     172          (Expr (Ecast (Tint I8 Unsigned )
     173            (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
     174            (Tint I8 Unsigned ));
     175          (Expr (Ecast (Tint I8 Unsigned )
     176            (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
     177            (Tint I8 Unsigned ))])
     178        (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
     179                              (Expr (Evar (ident_of_nat 8))
     180                                (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))))))
     181     
     182     
     183     
     184    )〉]
    183185  (ident_of_nat 7)
     186 
    184187.
    185188
     189(*
     190example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
     191normalize  (* you can examine the result here *)
     192*)

  • src/Clight/test/sum.c.ma

    r1226 r2176  
    33
    44definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
    5   [〈〈ident_of_nat 0 (* src *), Any〉,
     5  [〈〈ident_of_nat 0 (* src *), XData〉,
    66     〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
    77        (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
    8         (Init_int8 (repr I8 4)) ], (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
     8        (Init_int8 (repr I8 4)) ], (Tarray (Tint I8 Unsigned ) 5)〉〉]
    99  [〈ident_of_nat 1 (* main *), CL_Internal (
    1010     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
    … …  
    2121             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    2222             (Tint I32 Unsigned))
    23            (Expr (Esizeof (Tarray Any (Tint I8 Unsigned ) 5))
     23           (Expr (Esizeof (Tarray (Tint I8 Unsigned ) 5))
    2424             (Tint I32 Unsigned))) (Tint I32 Signed  ))
    2525         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    … …  
    3838                   (Expr (Ebinop Oadd
    3939                     (Expr (Evar (ident_of_nat 0))
    40                        (Tarray Any (Tint I8 Unsigned ) 5))
     40                       (Tarray (Tint I8 Unsigned ) 5))
    4141                     (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    42                      (Tpointer Any (Tint I8 Unsigned ))))
    43                    (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    44                (Tint I32 Signed  ))) (Tint I8 Unsigned )))
     42                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned )))
     43                 (Tint I32 Signed ))) (Tint I32 Signed  )))
     44             (Tint I8 Unsigned )))
    4545       )
    4646       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
Note: See TracChangeset for help on using the changeset viewer.