Changeset 726 for src/Clight/test


Ignore:
Timestamp:
Mar 30, 2011, 6:47:35 PM (9 years ago)
Author:
campbell
Message:

Change identifiers to Words in Clight and RTLabs semantics.

Location:
src/Clight/test
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/duff.ma

    r725 r726  
    22
    33definition myprog := mk_program clight_fundef type
    4   [〈succ_pos_of_nat 0 (* copy *), CL_Internal (
    5      mk_function Tvoid [〈succ_pos_of_nat 19, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 20, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 21, (Tint I32 Signed  )〉 ] [〈succ_pos_of_nat 1, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 3, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 4, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 5, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 6, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 7, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 8, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 9, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 10, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 11, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 12, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 13, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 14, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 15, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 16, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 17, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 18, (Tpointer Any (Tint I16 Signed  ))〉 ]
     4  [〈ident_of_nat 0 (* copy *), CL_Internal (
     5     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  ))〉 ]
    66       (Ssequence
    7        (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I32 Signed  ))
     7       (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    88         (Expr (Ebinop Odiv
    99           (Expr (Ebinop Oadd
    10              (Expr (Evar (succ_pos_of_nat 21)) (Tint I32 Signed  ))
     10             (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed  ))
    1111             (Expr (Econst_int (repr 7)) (Tint I32 Signed  )))
    1212             (Tint I32 Signed  ))
     
    1414           (Tint I32 Signed  )))
    1515       (Sswitch (Expr (Ebinop Omod
    16                   (Expr (Evar (succ_pos_of_nat 21)) (Tint I32 Signed  ))
     16                  (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed  ))
    1717                  (Expr (Econst_int (repr 8)) (Tint I32 Signed  )))
    1818                  (Tint I32 Signed  )) (
    1919         (LScase (repr 0)
    20            (Slabel (succ_pos_of_nat 22)
     20           (Slabel (ident_of_nat 22)
    2121           (Ssequence
    2222           (Ssequence
    23            (Sassign (Expr (Evar (succ_pos_of_nat 17))
     23           (Sassign (Expr (Evar (ident_of_nat 17))
    2424                      (Tpointer Any (Tint I16 Signed  )))
    25              (Expr (Evar (succ_pos_of_nat 19))
     25             (Expr (Evar (ident_of_nat 19))
    2626               (Tpointer Any (Tint I16 Signed  ))))
    27            (Sassign (Expr (Evar (succ_pos_of_nat 19))
     27           (Sassign (Expr (Evar (ident_of_nat 19))
    2828                      (Tpointer Any (Tint I16 Signed  )))
    2929             (Expr (Ebinop Oadd
    30                (Expr (Evar (succ_pos_of_nat 17))
     30               (Expr (Evar (ident_of_nat 17))
    3131                 (Tpointer Any (Tint I16 Signed  )))
    3232               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    3434           (Ssequence
    3535           (Ssequence
    36            (Sassign (Expr (Evar (succ_pos_of_nat 18))
     36           (Sassign (Expr (Evar (ident_of_nat 18))
    3737                      (Tpointer Any (Tint I16 Signed  )))
    38              (Expr (Evar (succ_pos_of_nat 20))
     38             (Expr (Evar (ident_of_nat 20))
    3939               (Tpointer Any (Tint I16 Signed  ))))
    40            (Sassign (Expr (Evar (succ_pos_of_nat 20))
     40           (Sassign (Expr (Evar (ident_of_nat 20))
    4141                      (Tpointer Any (Tint I16 Signed  )))
    4242             (Expr (Ebinop Oadd
    43                (Expr (Evar (succ_pos_of_nat 18))
     43               (Expr (Evar (ident_of_nat 18))
    4444                 (Tpointer Any (Tint I16 Signed  )))
    4545               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    4646               (Tpointer Any (Tint I16 Signed  )))))
    4747           (Sassign (Expr (Ederef
    48                       (Expr (Evar (succ_pos_of_nat 17))
     48                      (Expr (Evar (ident_of_nat 17))
    4949                        (Tpointer Any (Tint I16 Signed  ))))
    5050                      (Tint I16 Signed  ))
    5151             (Expr (Ederef
    52                (Expr (Evar (succ_pos_of_nat 18))
     52               (Expr (Evar (ident_of_nat 18))
    5353                 (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
    5454           (LScase (repr 7)
    5555             (Ssequence
    56              (Sassign (Expr (Evar (succ_pos_of_nat 15))
     56             (Sassign (Expr (Evar (ident_of_nat 15))
    5757                        (Tpointer Any (Tint I16 Signed  )))
    58                (Expr (Evar (succ_pos_of_nat 19))
     58               (Expr (Evar (ident_of_nat 19))
    5959                 (Tpointer Any (Tint I16 Signed  ))))
    6060             (Ssequence
    61              (Sassign (Expr (Evar (succ_pos_of_nat 19))
     61             (Sassign (Expr (Evar (ident_of_nat 19))
    6262                        (Tpointer Any (Tint I16 Signed  )))
    6363               (Expr (Ebinop Oadd
    64                  (Expr (Evar (succ_pos_of_nat 15))
     64                 (Expr (Evar (ident_of_nat 15))
    6565                   (Tpointer Any (Tint I16 Signed  )))
    6666                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    6767                 (Tpointer Any (Tint I16 Signed  ))))
    6868             (Ssequence
    69              (Sassign (Expr (Evar (succ_pos_of_nat 16))
     69             (Sassign (Expr (Evar (ident_of_nat 16))
    7070                        (Tpointer Any (Tint I16 Signed  )))
    71                (Expr (Evar (succ_pos_of_nat 20))
     71               (Expr (Evar (ident_of_nat 20))
    7272                 (Tpointer Any (Tint I16 Signed  ))))
    7373             (Ssequence
    74              (Sassign (Expr (Evar (succ_pos_of_nat 20))
     74             (Sassign (Expr (Evar (ident_of_nat 20))
    7575                        (Tpointer Any (Tint I16 Signed  )))
    7676               (Expr (Ebinop Oadd
    77                  (Expr (Evar (succ_pos_of_nat 16))
     77                 (Expr (Evar (ident_of_nat 16))
    7878                   (Tpointer Any (Tint I16 Signed  )))
    7979                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    8080                 (Tpointer Any (Tint I16 Signed  ))))
    8181             (Sassign (Expr (Ederef
    82                         (Expr (Evar (succ_pos_of_nat 15))
     82                        (Expr (Evar (ident_of_nat 15))
    8383                          (Tpointer Any (Tint I16 Signed  ))))
    8484                        (Tint I16 Signed  ))
    8585               (Expr (Ederef
    86                  (Expr (Evar (succ_pos_of_nat 16))
     86                 (Expr (Evar (ident_of_nat 16))
    8787                   (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
    8888             (LScase (repr 6)
    8989               (Ssequence
    90                (Sassign (Expr (Evar (succ_pos_of_nat 13))
     90               (Sassign (Expr (Evar (ident_of_nat 13))
    9191                          (Tpointer Any (Tint I16 Signed  )))
    92                  (Expr (Evar (succ_pos_of_nat 19))
     92                 (Expr (Evar (ident_of_nat 19))
    9393                   (Tpointer Any (Tint I16 Signed  ))))
    9494               (Ssequence
    95                (Sassign (Expr (Evar (succ_pos_of_nat 19))
     95               (Sassign (Expr (Evar (ident_of_nat 19))
    9696                          (Tpointer Any (Tint I16 Signed  )))
    9797                 (Expr (Ebinop Oadd
    98                    (Expr (Evar (succ_pos_of_nat 13))
     98                   (Expr (Evar (ident_of_nat 13))
    9999                     (Tpointer Any (Tint I16 Signed  )))
    100100                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    101101                   (Tpointer Any (Tint I16 Signed  ))))
    102102               (Ssequence
    103                (Sassign (Expr (Evar (succ_pos_of_nat 14))
     103               (Sassign (Expr (Evar (ident_of_nat 14))
    104104                          (Tpointer Any (Tint I16 Signed  )))
    105                  (Expr (Evar (succ_pos_of_nat 20))
     105                 (Expr (Evar (ident_of_nat 20))
    106106                   (Tpointer Any (Tint I16 Signed  ))))
    107107               (Ssequence
    108                (Sassign (Expr (Evar (succ_pos_of_nat 20))
     108               (Sassign (Expr (Evar (ident_of_nat 20))
    109109                          (Tpointer Any (Tint I16 Signed  )))
    110110                 (Expr (Ebinop Oadd
    111                    (Expr (Evar (succ_pos_of_nat 14))
     111                   (Expr (Evar (ident_of_nat 14))
    112112                     (Tpointer Any (Tint I16 Signed  )))
    113113                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    114114                   (Tpointer Any (Tint I16 Signed  ))))
    115115               (Sassign (Expr (Ederef
    116                           (Expr (Evar (succ_pos_of_nat 13))
     116                          (Expr (Evar (ident_of_nat 13))
    117117                            (Tpointer Any (Tint I16 Signed  ))))
    118118                          (Tint I16 Signed  ))
    119119                 (Expr (Ederef
    120                    (Expr (Evar (succ_pos_of_nat 14))
     120                   (Expr (Evar (ident_of_nat 14))
    121121                     (Tpointer Any (Tint I16 Signed  ))))
    122122                   (Tint I16 Signed  )))))))
    123123               (LScase (repr 5)
    124124                 (Ssequence
    125                  (Sassign (Expr (Evar (succ_pos_of_nat 11))
     125                 (Sassign (Expr (Evar (ident_of_nat 11))
    126126                            (Tpointer Any (Tint I16 Signed  )))
    127                    (Expr (Evar (succ_pos_of_nat 19))
     127                   (Expr (Evar (ident_of_nat 19))
    128128                     (Tpointer Any (Tint I16 Signed  ))))
    129129                 (Ssequence
    130                  (Sassign (Expr (Evar (succ_pos_of_nat 19))
     130                 (Sassign (Expr (Evar (ident_of_nat 19))
    131131                            (Tpointer Any (Tint I16 Signed  )))
    132132                   (Expr (Ebinop Oadd
    133                      (Expr (Evar (succ_pos_of_nat 11))
     133                     (Expr (Evar (ident_of_nat 11))
    134134                       (Tpointer Any (Tint I16 Signed  )))
    135135                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    136136                     (Tpointer Any (Tint I16 Signed  ))))
    137137                 (Ssequence
    138                  (Sassign (Expr (Evar (succ_pos_of_nat 12))
     138                 (Sassign (Expr (Evar (ident_of_nat 12))
    139139                            (Tpointer Any (Tint I16 Signed  )))
    140                    (Expr (Evar (succ_pos_of_nat 20))
     140                   (Expr (Evar (ident_of_nat 20))
    141141                     (Tpointer Any (Tint I16 Signed  ))))
    142142                 (Ssequence
    143                  (Sassign (Expr (Evar (succ_pos_of_nat 20))
     143                 (Sassign (Expr (Evar (ident_of_nat 20))
    144144                            (Tpointer Any (Tint I16 Signed  )))
    145145                   (Expr (Ebinop Oadd
    146                      (Expr (Evar (succ_pos_of_nat 12))
     146                     (Expr (Evar (ident_of_nat 12))
    147147                       (Tpointer Any (Tint I16 Signed  )))
    148148                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    149149                     (Tpointer Any (Tint I16 Signed  ))))
    150150                 (Sassign (Expr (Ederef
    151                             (Expr (Evar (succ_pos_of_nat 11))
     151                            (Expr (Evar (ident_of_nat 11))
    152152                              (Tpointer Any (Tint I16 Signed  ))))
    153153                            (Tint I16 Signed  ))
    154154                   (Expr (Ederef
    155                      (Expr (Evar (succ_pos_of_nat 12))
     155                     (Expr (Evar (ident_of_nat 12))
    156156                       (Tpointer Any (Tint I16 Signed  ))))
    157157                     (Tint I16 Signed  )))))))
    158158                 (LScase (repr 4)
    159159                   (Ssequence
    160                    (Sassign (Expr (Evar (succ_pos_of_nat 9))
     160                   (Sassign (Expr (Evar (ident_of_nat 9))
    161161                              (Tpointer Any (Tint I16 Signed  )))
    162                      (Expr (Evar (succ_pos_of_nat 19))
     162                     (Expr (Evar (ident_of_nat 19))
    163163                       (Tpointer Any (Tint I16 Signed  ))))
    164164                   (Ssequence
    165                    (Sassign (Expr (Evar (succ_pos_of_nat 19))
     165                   (Sassign (Expr (Evar (ident_of_nat 19))
    166166                              (Tpointer Any (Tint I16 Signed  )))
    167167                     (Expr (Ebinop Oadd
    168                        (Expr (Evar (succ_pos_of_nat 9))
     168                       (Expr (Evar (ident_of_nat 9))
    169169                         (Tpointer Any (Tint I16 Signed  )))
    170170                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    171171                       (Tpointer Any (Tint I16 Signed  ))))
    172172                   (Ssequence
    173                    (Sassign (Expr (Evar (succ_pos_of_nat 10))
     173                   (Sassign (Expr (Evar (ident_of_nat 10))
    174174                              (Tpointer Any (Tint I16 Signed  )))
    175                      (Expr (Evar (succ_pos_of_nat 20))
     175                     (Expr (Evar (ident_of_nat 20))
    176176                       (Tpointer Any (Tint I16 Signed  ))))
    177177                   (Ssequence
    178                    (Sassign (Expr (Evar (succ_pos_of_nat 20))
     178                   (Sassign (Expr (Evar (ident_of_nat 20))
    179179                              (Tpointer Any (Tint I16 Signed  )))
    180180                     (Expr (Ebinop Oadd
    181                        (Expr (Evar (succ_pos_of_nat 10))
     181                       (Expr (Evar (ident_of_nat 10))
    182182                         (Tpointer Any (Tint I16 Signed  )))
    183183                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    184184                       (Tpointer Any (Tint I16 Signed  ))))
    185185                   (Sassign (Expr (Ederef
    186                               (Expr (Evar (succ_pos_of_nat 9))
     186                              (Expr (Evar (ident_of_nat 9))
    187187                                (Tpointer Any (Tint I16 Signed  ))))
    188188                              (Tint I16 Signed  ))
    189189                     (Expr (Ederef
    190                        (Expr (Evar (succ_pos_of_nat 10))
     190                       (Expr (Evar (ident_of_nat 10))
    191191                         (Tpointer Any (Tint I16 Signed  ))))
    192192                       (Tint I16 Signed  )))))))
    193193                   (LScase (repr 3)
    194194                     (Ssequence
    195                      (Sassign (Expr (Evar (succ_pos_of_nat 7))
     195                     (Sassign (Expr (Evar (ident_of_nat 7))
    196196                                (Tpointer Any (Tint I16 Signed  )))
    197                        (Expr (Evar (succ_pos_of_nat 19))
     197                       (Expr (Evar (ident_of_nat 19))
    198198                         (Tpointer Any (Tint I16 Signed  ))))
    199199                     (Ssequence
    200                      (Sassign (Expr (Evar (succ_pos_of_nat 19))
     200                     (Sassign (Expr (Evar (ident_of_nat 19))
    201201                                (Tpointer Any (Tint I16 Signed  )))
    202202                       (Expr (Ebinop Oadd
    203                          (Expr (Evar (succ_pos_of_nat 7))
     203                         (Expr (Evar (ident_of_nat 7))
    204204                           (Tpointer Any (Tint I16 Signed  )))
    205205                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    206206                         (Tpointer Any (Tint I16 Signed  ))))
    207207                     (Ssequence
    208                      (Sassign (Expr (Evar (succ_pos_of_nat 8))
     208                     (Sassign (Expr (Evar (ident_of_nat 8))
    209209                                (Tpointer Any (Tint I16 Signed  )))
    210                        (Expr (Evar (succ_pos_of_nat 20))
     210                       (Expr (Evar (ident_of_nat 20))
    211211                         (Tpointer Any (Tint I16 Signed  ))))
    212212                     (Ssequence
    213                      (Sassign (Expr (Evar (succ_pos_of_nat 20))
     213                     (Sassign (Expr (Evar (ident_of_nat 20))
    214214                                (Tpointer Any (Tint I16 Signed  )))
    215215                       (Expr (Ebinop Oadd
    216                          (Expr (Evar (succ_pos_of_nat 8))
     216                         (Expr (Evar (ident_of_nat 8))
    217217                           (Tpointer Any (Tint I16 Signed  )))
    218218                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    219219                         (Tpointer Any (Tint I16 Signed  ))))
    220220                     (Sassign (Expr (Ederef
    221                                 (Expr (Evar (succ_pos_of_nat 7))
     221                                (Expr (Evar (ident_of_nat 7))
    222222                                  (Tpointer Any (Tint I16 Signed  ))))
    223223                                (Tint I16 Signed  ))
    224224                       (Expr (Ederef
    225                          (Expr (Evar (succ_pos_of_nat 8))
     225                         (Expr (Evar (ident_of_nat 8))
    226226                           (Tpointer Any (Tint I16 Signed  ))))
    227227                         (Tint I16 Signed  )))))))
    228228                     (LScase (repr 2)
    229229                       (Ssequence
    230                        (Sassign (Expr (Evar (succ_pos_of_nat 5))
     230                       (Sassign (Expr (Evar (ident_of_nat 5))
    231231                                  (Tpointer Any (Tint I16 Signed  )))
    232                          (Expr (Evar (succ_pos_of_nat 19))
     232                         (Expr (Evar (ident_of_nat 19))
    233233                           (Tpointer Any (Tint I16 Signed  ))))
    234234                       (Ssequence
    235                        (Sassign (Expr (Evar (succ_pos_of_nat 19))
     235                       (Sassign (Expr (Evar (ident_of_nat 19))
    236236                                  (Tpointer Any (Tint I16 Signed  )))
    237237                         (Expr (Ebinop Oadd
    238                            (Expr (Evar (succ_pos_of_nat 5))
     238                           (Expr (Evar (ident_of_nat 5))
    239239                             (Tpointer Any (Tint I16 Signed  )))
    240240                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    241241                           (Tpointer Any (Tint I16 Signed  ))))
    242242                       (Ssequence
    243                        (Sassign (Expr (Evar (succ_pos_of_nat 6))
     243                       (Sassign (Expr (Evar (ident_of_nat 6))
    244244                                  (Tpointer Any (Tint I16 Signed  )))
    245                          (Expr (Evar (succ_pos_of_nat 20))
     245                         (Expr (Evar (ident_of_nat 20))
    246246                           (Tpointer Any (Tint I16 Signed  ))))
    247247                       (Ssequence
    248                        (Sassign (Expr (Evar (succ_pos_of_nat 20))
     248                       (Sassign (Expr (Evar (ident_of_nat 20))
    249249                                  (Tpointer Any (Tint I16 Signed  )))
    250250                         (Expr (Ebinop Oadd
    251                            (Expr (Evar (succ_pos_of_nat 6))
     251                           (Expr (Evar (ident_of_nat 6))
    252252                             (Tpointer Any (Tint I16 Signed  )))
    253253                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    254254                           (Tpointer Any (Tint I16 Signed  ))))
    255255                       (Sassign (Expr (Ederef
    256                                   (Expr (Evar (succ_pos_of_nat 5))
     256                                  (Expr (Evar (ident_of_nat 5))
    257257                                    (Tpointer Any (Tint I16 Signed  ))))
    258258                                  (Tint I16 Signed  ))
    259259                         (Expr (Ederef
    260                            (Expr (Evar (succ_pos_of_nat 6))
     260                           (Expr (Evar (ident_of_nat 6))
    261261                             (Tpointer Any (Tint I16 Signed  ))))
    262262                           (Tint I16 Signed  )))))))
    263263                       (LScase (repr 1)
    264264                         (Ssequence
    265                          (Sassign (Expr (Evar (succ_pos_of_nat 3))
     265                         (Sassign (Expr (Evar (ident_of_nat 3))
    266266                                    (Tpointer Any (Tint I16 Signed  )))
    267                            (Expr (Evar (succ_pos_of_nat 19))
     267                           (Expr (Evar (ident_of_nat 19))
    268268                             (Tpointer Any (Tint I16 Signed  ))))
    269269                         (Ssequence
    270                          (Sassign (Expr (Evar (succ_pos_of_nat 19))
     270                         (Sassign (Expr (Evar (ident_of_nat 19))
    271271                                    (Tpointer Any (Tint I16 Signed  )))
    272272                           (Expr (Ebinop Oadd
    273                              (Expr (Evar (succ_pos_of_nat 3))
     273                             (Expr (Evar (ident_of_nat 3))
    274274                               (Tpointer Any (Tint I16 Signed  )))
    275275                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    276276                             (Tpointer Any (Tint I16 Signed  ))))
    277277                         (Ssequence
    278                          (Sassign (Expr (Evar (succ_pos_of_nat 4))
     278                         (Sassign (Expr (Evar (ident_of_nat 4))
    279279                                    (Tpointer Any (Tint I16 Signed  )))
    280                            (Expr (Evar (succ_pos_of_nat 20))
     280                           (Expr (Evar (ident_of_nat 20))
    281281                             (Tpointer Any (Tint I16 Signed  ))))
    282282                         (Ssequence
    283                          (Sassign (Expr (Evar (succ_pos_of_nat 20))
     283                         (Sassign (Expr (Evar (ident_of_nat 20))
    284284                                    (Tpointer Any (Tint I16 Signed  )))
    285285                           (Expr (Ebinop Oadd
    286                              (Expr (Evar (succ_pos_of_nat 4))
     286                             (Expr (Evar (ident_of_nat 4))
    287287                               (Tpointer Any (Tint I16 Signed  )))
    288288                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    290290                         (Ssequence
    291291                         (Sassign (Expr (Ederef
    292                                     (Expr (Evar (succ_pos_of_nat 3))
     292                                    (Expr (Evar (ident_of_nat 3))
    293293                                      (Tpointer Any (Tint I16 Signed  ))))
    294294                                    (Tint I16 Signed  ))
    295295                           (Expr (Ederef
    296                              (Expr (Evar (succ_pos_of_nat 4))
     296                             (Expr (Evar (ident_of_nat 4))
    297297                               (Tpointer Any (Tint I16 Signed  ))))
    298298                             (Tint I16 Signed  )))
    299299                         (Ssequence
    300                          (Sassign (Expr (Evar (succ_pos_of_nat 2))
     300                         (Sassign (Expr (Evar (ident_of_nat 2))
    301301                                    (Tint I32 Signed  ))
    302302                           (Expr (Ebinop Osub
    303                              (Expr (Evar (succ_pos_of_nat 1))
     303                             (Expr (Evar (ident_of_nat 1))
    304304                               (Tint I32 Signed  ))
    305305                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    306306                             (Tint I32 Signed  )))
    307307                         (Ssequence
    308                          (Sassign (Expr (Evar (succ_pos_of_nat 1))
     308                         (Sassign (Expr (Evar (ident_of_nat 1))
    309309                                    (Tint I32 Signed  ))
    310                            (Expr (Evar (succ_pos_of_nat 2))
     310                           (Expr (Evar (ident_of_nat 2))
    311311                             (Tint I32 Signed  )))
    312312                         (Sifthenelse (Expr (Ebinop Ogt
    313                                         (Expr (Evar (succ_pos_of_nat 2))
     313                                        (Expr (Evar (ident_of_nat 2))
    314314                                          (Tint I32 Signed  ))
    315315                                        (Expr (Econst_int (repr 0))
    316316                                          (Tint I32 Signed  )))
    317317                                        (Tint I32 Signed  ))
    318                            (Sgoto (succ_pos_of_nat 22))
     318                           (Sgoto (ident_of_nat 22))
    319319                           Sskip))))))))
    320320                         (LSdefault
     
    325325     
    326326   )〉;
    327   〈succ_pos_of_nat 23 (* main *), CL_Internal (
    328     mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 24, (Tarray Any (Tint I16 Signed  ) 3)〉 ; 〈succ_pos_of_nat 25, (Tarray Any (Tint I16 Signed  ) 3)〉 ]
     327  〈ident_of_nat 23 (* main *), CL_Internal (
     328    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)〉 ]
    329329      (Ssequence
    330330      (Sassign (Expr (Ederef
    331331                 (Expr (Ebinop Oadd
    332                    (Expr (Evar (succ_pos_of_nat 24))
     332                   (Expr (Evar (ident_of_nat 24))
    333333                     (Tarray Any (Tint I16 Signed  ) 3))
    334334                   (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     
    340340      (Sassign (Expr (Ederef
    341341                 (Expr (Ebinop Oadd
    342                    (Expr (Evar (succ_pos_of_nat 24))
     342                   (Expr (Evar (ident_of_nat 24))
    343343                     (Tarray Any (Tint I16 Signed  ) 3))
    344344                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    350350      (Sassign (Expr (Ederef
    351351                 (Expr (Ebinop Oadd
    352                    (Expr (Evar (succ_pos_of_nat 24))
     352                   (Expr (Evar (ident_of_nat 24))
    353353                     (Tarray Any (Tint I16 Signed  ) 3))
    354354                   (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
     
    358358          (Tint I16 Signed  )))
    359359      (Ssequence
    360       (Scall (None expr) (Expr (Evar (succ_pos_of_nat 0))
     360      (Scall (None expr) (Expr (Evar (ident_of_nat 0))
    361361                           (Tfunction (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid))
    362         [(Expr (Evar (succ_pos_of_nat 25))
     362        [(Expr (Evar (ident_of_nat 25))
    363363           (Tarray Any (Tint I16 Signed  ) 3));
    364         (Expr (Evar (succ_pos_of_nat 24)) (Tarray Any (Tint I16 Signed  ) 3));
     364        (Expr (Evar (ident_of_nat 24)) (Tarray Any (Tint I16 Signed  ) 3));
    365365        (Expr (Econst_int (repr 3)) (Tint I32 Signed  ))])
    366366      (Sreturn (Some expr (Expr (Ebinop Oadd
     
    369369                                (Expr (Ederef
    370370                                  (Expr (Ebinop Oadd
    371                                     (Expr (Evar (succ_pos_of_nat 25))
     371                                    (Expr (Evar (ident_of_nat 25))
    372372                                      (Tarray Any (Tint I16 Signed  ) 3))
    373373                                    (Expr (Econst_int (repr 0))
     
    378378                                (Expr (Ederef
    379379                                  (Expr (Ebinop Oadd
    380                                     (Expr (Evar (succ_pos_of_nat 25))
     380                                    (Expr (Evar (ident_of_nat 25))
    381381                                      (Tarray Any (Tint I16 Signed  ) 3))
    382382                                    (Expr (Econst_int (repr 1))
     
    388388                              (Expr (Ederef
    389389                                (Expr (Ebinop Oadd
    390                                   (Expr (Evar (succ_pos_of_nat 25))
     390                                  (Expr (Evar (ident_of_nat 25))
    391391                                    (Tarray Any (Tint I16 Signed  ) 3))
    392392                                  (Expr (Econst_int (repr 2))
     
    399399   
    400400  )〉]
    401   (succ_pos_of_nat 23)
     401  (ident_of_nat 23)
    402402  []
    403403.
  • src/Clight/test/factorial.ma

    r725 r726  
    22
    33definition myprog := mk_program clight_fundef type
    4   [〈succ_pos_of_nat 0 (* get_input *), CL_External (succ_pos_of_nat 0) Tnil (Tint I32 Signed  )〉;
    5   〈succ_pos_of_nat 1 (* main *), CL_Internal (
    6     mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 3, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 4, (Tint I32 Signed  )〉 ]
     4  [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
     5  〈ident_of_nat 1 (* main *), CL_Internal (
     6    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ; 〈ident_of_nat 4, (Tint I32 Signed  )〉 ]
    77      (Ssequence
    8       (Scall (Some expr (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
    9         (Expr (Evar (succ_pos_of_nat 0))
     8      (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
     9        (Expr (Evar (ident_of_nat 0))
    1010          (Tfunction Tnil (Tint I32 Signed  )))
    1111        [])
    1212      (Ssequence
    13       (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
     13      (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    1414        (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    1515      (Ssequence
    1616      (Ssequence
    17       (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
     17      (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    1818              (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    1919        (Expr (Ebinop Ole
    20           (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
    21           (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
     20          (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
     21          (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    2222          (Tint I32 Signed  ))
    23         (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
     23        (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    2424          (Expr (Ebinop Oadd
    25             (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
     25            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    2626            (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    2727            (Tint I32 Signed  )))
    28         (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
     28        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    2929          (Expr (Ebinop Omul
    30             (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
    31             (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  )))
     30            (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
     31            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
    3232            (Tint I32 Signed  )))
    3333      )
    3434      Sskip)
    35       (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 3))
     35      (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
    3636                            (Tint I32 Signed  )))))))
    3737   
     
    3939   
    4040  )〉]
    41   (succ_pos_of_nat 1)
     41  (ident_of_nat 1)
    4242  []
    4343.
  • src/Clight/test/insertsort.ma

    r725 r726  
    22
    33definition myprog := mk_program clight_fundef type
    4   [〈succ_pos_of_nat 0 (* insert *), CL_Internal (
    5      mk_function Tvoid [〈succ_pos_of_nat 2, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 6, (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))〉 ] [〈succ_pos_of_nat 1, (Tint I32 Signed  )〉 ]
     4  [〈ident_of_nat 0 (* insert *), CL_Internal (
     5     mk_function Tvoid [〈ident_of_nat 2, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ]
    66       (Ssequence
    77       (Sifthenelse (Expr (Ebinop Oeq
    88                      (Expr (Ederef
    9                         (Expr (Evar (succ_pos_of_nat 6))
    10                           (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    11                         (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    12                       (Expr (Ecast (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))
     9                        (Expr (Evar (ident_of_nat 6))
     10                          (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     11                        (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     12                      (Expr (Ecast (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))
    1313                        (Expr (Ecast (Tpointer Any Tvoid)
    1414                          (Expr (Econst_int (repr 0)) (Tint I32 Unsigned)))
    1515                          (Tpointer Any Tvoid)))
    16                         (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
     16                        (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
    1717                      (Tint I32 Signed  ))
    18          (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I32 Signed  ))
     18         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    1919           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    20          (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I32 Signed  ))
     20         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    2121           (Expr (Ebinop One
    2222             (Expr (Ebinop Oge
     
    2424                 (Expr (Efield (Expr (Ederef
    2525                                 (Expr (Ederef
    26                                    (Expr (Evar (succ_pos_of_nat 6))
    27                                      (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    28                                    (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    29                                  (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 4))
     26                                   (Expr (Evar (ident_of_nat 6))
     27                                     (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     28                                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     29                                 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
    3030                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    3131               (Expr (Ecast (Tint I32 Signed  )
    3232                 (Expr (Efield (Expr (Ederef
    33                                  (Expr (Evar (succ_pos_of_nat 2))
    34                                    (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    35                                  (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 4))
     33                                 (Expr (Evar (ident_of_nat 2))
     34                                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     35                                 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
    3636                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    3737               (Tint I32 Signed  ))
    3838             (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    3939             (Tint I32 Signed  ))))
    40        (Sifthenelse (Expr (Evar (succ_pos_of_nat 1)) (Tint I32 Signed  ))
     40       (Sifthenelse (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    4141         (Ssequence
    4242         (Sassign (Expr (Efield (Expr (Ederef
    43                                   (Expr (Evar (succ_pos_of_nat 2))
    44                                     (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    45                                   (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))
    46                     (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     43                                  (Expr (Evar (ident_of_nat 2))
     44                                    (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     45                                  (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
     46                    (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    4747           (Expr (Ederef
    48              (Expr (Evar (succ_pos_of_nat 6))
    49                (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    50              (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
     48             (Expr (Evar (ident_of_nat 6))
     49               (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     50             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
    5151         (Sassign (Expr (Ederef
    52                     (Expr (Evar (succ_pos_of_nat 6))
    53                       (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    54                     (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    55            (Expr (Evar (succ_pos_of_nat 2))
    56              (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    57          (Scall (None expr) (Expr (Evar (succ_pos_of_nat 0))
    58                               (Tfunction (Tcons (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))) Tnil)) Tvoid))
    59            [(Expr (Evar (succ_pos_of_nat 2))
    60               (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))));
    61            (Expr (Ecast (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     52                    (Expr (Evar (ident_of_nat 6))
     53                      (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     54                    (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     55           (Expr (Evar (ident_of_nat 2))
     56             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     57         (Scall (None expr) (Expr (Evar (ident_of_nat 0))
     58                              (Tfunction (Tcons (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid))
     59           [(Expr (Evar (ident_of_nat 2))
     60              (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))));
     61           (Expr (Ecast (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    6262             (Expr (Eaddrof
    6363               (Expr (Efield (Expr (Ederef
    6464                               (Expr (Ederef
    65                                  (Expr (Evar (succ_pos_of_nat 6))
    66                                    (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    67                                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    68                                (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))
    69                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    70                (Tpointer PData (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    71              (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))])))
     65                                 (Expr (Evar (ident_of_nat 6))
     66                                   (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     67                                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     68                               (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
     69                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     70               (Tpointer PData (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     71             (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))])))
    7272     
    7373     
    7474     
    7575   )〉;
    76   〈succ_pos_of_nat 7 (* sort *), CL_Internal (
    77     mk_function Tvoid [〈succ_pos_of_nat 10, (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))〉 ] [〈succ_pos_of_nat 8, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 5, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 9, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ]
    78       (Ssequence
    79       (Sassign (Expr (Evar (succ_pos_of_nat 5))
    80                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     76  〈ident_of_nat 7 (* sort *), CL_Internal (
     77    mk_function Tvoid [〈ident_of_nat 10, (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 8, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 5, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 9, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ]
     78      (Ssequence
     79      (Sassign (Expr (Evar (ident_of_nat 5))
     80                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    8181        (Expr (Ederef
    82           (Expr (Evar (succ_pos_of_nat 10))
    83             (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    84           (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    85       (Ssequence
    86       (Sassign (Expr (Evar (succ_pos_of_nat 9))
    87                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    88         (Expr (Ecast (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))
     82          (Expr (Evar (ident_of_nat 10))
     83            (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     84          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     85      (Ssequence
     86      (Sassign (Expr (Evar (ident_of_nat 9))
     87                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     88        (Expr (Ecast (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))
    8989          (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    90           (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    91       (Ssequence
    92       (Ssequence
    93       (Swhile (Expr (Evar (succ_pos_of_nat 5))
    94                 (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     90          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     91      (Ssequence
     92      (Ssequence
     93      (Swhile (Expr (Evar (ident_of_nat 5))
     94                (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    9595        (Ssequence
    96         (Sassign (Expr (Evar (succ_pos_of_nat 8))
    97                    (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    98           (Expr (Evar (succ_pos_of_nat 5))
    99             (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
     96        (Sassign (Expr (Evar (ident_of_nat 8))
     97                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     98          (Expr (Evar (ident_of_nat 5))
     99            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
    100100        (Ssequence
    101         (Sassign (Expr (Evar (succ_pos_of_nat 5))
    102                    (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     101        (Sassign (Expr (Evar (ident_of_nat 5))
     102                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    103103          (Expr (Efield (Expr (Ederef
    104                           (Expr (Evar (succ_pos_of_nat 5))
    105                             (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    106                           (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))
    107             (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    108         (Scall (None expr) (Expr (Evar (succ_pos_of_nat 0))
    109                              (Tfunction (Tcons (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))) Tnil)) Tvoid))
    110           [(Expr (Evar (succ_pos_of_nat 8))
    111              (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))));
     104                          (Expr (Evar (ident_of_nat 5))
     105                            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     106                          (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
     107            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     108        (Scall (None expr) (Expr (Evar (ident_of_nat 0))
     109                             (Tfunction (Tcons (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid))
     110          [(Expr (Evar (ident_of_nat 8))
     111             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))));
    112112          (Expr (Eaddrof
    113             (Expr (Evar (succ_pos_of_nat 9))
    114               (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    115             (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))]))))
     113            (Expr (Evar (ident_of_nat 9))
     114              (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     115            (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))]))))
    116116      Sskip)
    117117      (Sassign (Expr (Ederef
    118                  (Expr (Evar (succ_pos_of_nat 10))
    119                    (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    120                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    121         (Expr (Evar (succ_pos_of_nat 9))
    122           (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))))
     118                 (Expr (Evar (ident_of_nat 10))
     119                   (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     120                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     121        (Expr (Evar (ident_of_nat 9))
     122          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))))
    123123   
    124124   
    125125   
    126126  )〉;
    127   〈succ_pos_of_nat 11 (* out *), CL_External (succ_pos_of_nat 11) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;
    128   〈succ_pos_of_nat 12 (* main *), CL_Internal (
    129     mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 13, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ]
    130       (Ssequence
    131       (Sassign (Expr (Evar (succ_pos_of_nat 13))
    132                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     127  〈ident_of_nat 11 (* out *), CL_External (ident_of_nat 11) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;
     128  〈ident_of_nat 12 (* main *), CL_Internal (
     129    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 13, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ]
     130      (Ssequence
     131      (Sassign (Expr (Evar (ident_of_nat 13))
     132                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    133133        (Expr (Eaddrof
    134           (Expr (Evar (succ_pos_of_nat 14))
    135             (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    136           (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    137       (Ssequence
    138       (Scall (None expr) (Expr (Evar (succ_pos_of_nat 7))
    139                            (Tfunction (Tcons (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))) Tnil) Tvoid))
     134          (Expr (Evar (ident_of_nat 14))
     135            (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     136          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     137      (Ssequence
     138      (Scall (None expr) (Expr (Evar (ident_of_nat 7))
     139                           (Tfunction (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil) Tvoid))
    140140        [(Expr (Eaddrof
    141            (Expr (Evar (succ_pos_of_nat 13))
    142              (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    143            (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))])
    144       (Ssequence
    145       (Ssequence
    146       (Swhile (Expr (Evar (succ_pos_of_nat 13))
    147                 (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     141           (Expr (Evar (ident_of_nat 13))
     142             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     143           (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))])
     144      (Ssequence
     145      (Ssequence
     146      (Swhile (Expr (Evar (ident_of_nat 13))
     147                (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    148148        (Ssequence
    149         (Scall (None expr) (Expr (Evar (succ_pos_of_nat 11))
     149        (Scall (None expr) (Expr (Evar (ident_of_nat 11))
    150150                             (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) Tvoid))
    151151          [(Expr (Efield (Expr (Ederef
    152                            (Expr (Evar (succ_pos_of_nat 13))
    153                              (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    154                            (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 4))
     152                           (Expr (Evar (ident_of_nat 13))
     153                             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     154                           (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
    155155             (Tint I8 Unsigned ))])
    156         (Sassign (Expr (Evar (succ_pos_of_nat 13))
    157                    (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     156        (Sassign (Expr (Evar (ident_of_nat 13))
     157                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    158158          (Expr (Efield (Expr (Ederef
    159                           (Expr (Evar (succ_pos_of_nat 13))
    160                             (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    161                           (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))
    162             (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))))
     159                          (Expr (Evar (ident_of_nat 13))
     160                            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     161                          (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
     162            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))))
    163163      Sskip)
    164164      (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))))))
     
    167167   
    168168  )〉]
    169   (succ_pos_of_nat 12)
    170   [〈〈〈succ_pos_of_nat 15 (* l6 *),
     169  (ident_of_nat 12)
     170  [〈〈〈ident_of_nat 15 (* l6 *),
    171171     [(Init_int8 (repr 69)) ; (Init_space 3) ; (Init_null PData) ;
    172172     (Init_space 3) ]〉, PData〉,
    173      (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    174   〈〈〈succ_pos_of_nat 16 (* l5 *),
     173     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     174  〈〈〈ident_of_nat 16 (* l5 *),
    175175    [(Init_int8 (repr 36)) ; (Init_space 3) ;
    176     (Init_addrof PData (succ_pos_of_nat 15) (repr 0))]〉, PData〉,
    177     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    178   〈〈〈succ_pos_of_nat 17 (* l4 *),
     176    (Init_addrof PData (ident_of_nat 15) (repr 0))]〉, PData〉,
     177    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     178  〈〈〈ident_of_nat 17 (* l4 *),
    179179    [(Init_int8 (repr 136)) ; (Init_space 3) ;
    180     (Init_addrof PData (succ_pos_of_nat 16) (repr 0))]〉, PData〉,
    181     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    182   〈〈〈succ_pos_of_nat 18 (* l3 *),
     180    (Init_addrof PData (ident_of_nat 16) (repr 0))]〉, PData〉,
     181    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     182  〈〈〈ident_of_nat 18 (* l3 *),
    183183    [(Init_int8 (repr 105)) ; (Init_space 3) ;
    184     (Init_addrof PData (succ_pos_of_nat 17) (repr 0))]〉, PData〉,
    185     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    186   〈〈〈succ_pos_of_nat 19 (* l2 *),
     184    (Init_addrof PData (ident_of_nat 17) (repr 0))]〉, PData〉,
     185    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     186  〈〈〈ident_of_nat 19 (* l2 *),
    187187    [(Init_int8 (repr 234)) ; (Init_space 3) ;
    188     (Init_addrof PData (succ_pos_of_nat 18) (repr 0))]〉, PData〉,
    189     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    190   〈〈〈succ_pos_of_nat 20 (* l1 *),
     188    (Init_addrof PData (ident_of_nat 18) (repr 0))]〉, PData〉,
     189    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     190  〈〈〈ident_of_nat 20 (* l1 *),
    191191    [(Init_int8 (repr 240)) ; (Init_space 3) ;
    192     (Init_addrof PData (succ_pos_of_nat 19) (repr 0))]〉, PData〉,
    193     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    194   〈〈〈succ_pos_of_nat 14 (* l0 *),
     192    (Init_addrof PData (ident_of_nat 19) (repr 0))]〉, PData〉,
     193    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     194  〈〈〈ident_of_nat 14 (* l0 *),
    195195    [(Init_int8 (repr 102)) ; (Init_space 3) ;
    196     (Init_addrof PData (succ_pos_of_nat 20) (repr 0))]〉, PData〉,
    197     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉]
     196    (Init_addrof PData (ident_of_nat 20) (repr 0))]〉, PData〉,
     197    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉]
    198198.
    199199
     
    201201  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
    202202   OK ? t) = OK ?
    203 [EVextcall (succ_pos_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
    204  EVextcall (succ_pos_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
    205  EVextcall (succ_pos_of_nat 11) [EVint (repr 102)] (EVint (repr 0));
    206  EVextcall (succ_pos_of_nat 11) [EVint (repr 105)] (EVint (repr 0));
    207  EVextcall (succ_pos_of_nat 11) [EVint (repr 136)] (EVint (repr 0));
    208  EVextcall (succ_pos_of_nat 11) [EVint (repr 234)] (EVint (repr 0));
    209  EVextcall (succ_pos_of_nat 11) [EVint (repr 240)] (EVint (repr 0))]
     203[EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
     204 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
     205 EVextcall (ident_of_nat 11) [EVint (repr 102)] (EVint (repr 0));
     206 EVextcall (ident_of_nat 11) [EVint (repr 105)] (EVint (repr 0));
     207 EVextcall (ident_of_nat 11) [EVint (repr 136)] (EVint (repr 0));
     208 EVextcall (ident_of_nat 11) [EVint (repr 234)] (EVint (repr 0));
     209 EVextcall (ident_of_nat 11) [EVint (repr 240)] (EVint (repr 0))]
    210210.
    211211normalize  (* you can examine the result here *)
  • src/Clight/test/io.ma

    r725 r726  
    22
    33definition myprog := mk_program clight_fundef type
    4   [〈succ_pos_of_nat 0 (* dosomething *), CL_External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
    5   〈succ_pos_of_nat 1 (* main *), CL_Internal (
    6     mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ]
     4  [〈ident_of_nat 0 (* dosomething *), CL_External (ident_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
     5  〈ident_of_nat 1 (* main *), CL_Internal (
     6    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ]
    77      (Ssequence
    8       (Scall (Some expr (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
    9         (Expr (Evar (succ_pos_of_nat 0))
     8      (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
     9        (Expr (Evar (ident_of_nat 0))
    1010          (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
    1111        [(Expr (Econst_int (repr 10)) (Tint I32 Signed  ))])
    12       (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 2))
     12      (Sreturn (Some expr (Expr (Evar (ident_of_nat 2))
    1313                            (Tint I32 Signed  )))))
    1414   
     
    1616   
    1717  )〉]
    18   (succ_pos_of_nat 1)
     18  (ident_of_nat 1)
    1919  []
    2020.
     
    2222example exec:
    2323 (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) =
    24  OK ? 〈[EVextcall (succ_pos_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
     24 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
    2525normalize  (* you can examine the result here *)
    2626@refl
  • src/Clight/test/io2.ma

    r725 r726  
    22
    33definition myprog := mk_program clight_fundef type
    4   [〈succ_pos_of_nat 0 (* dosomething *), CL_External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
    5   〈succ_pos_of_nat 1 (* main *), CL_Internal (
    6     mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 3, (Tint I32 Signed  )〉 ]
     4  [〈ident_of_nat 0 (* dosomething *), CL_External (ident_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
     5  〈ident_of_nat 1 (* main *), CL_Internal (
     6    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ]
    77      (Ssequence
    8       (Sassign (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  ))
     8      (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    99        (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    1010      (Ssequence
    1111      (Ssequence
    12       (Scall (Some expr (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  )))
    13         (Expr (Evar (succ_pos_of_nat 0))
     12      (Scall (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
     13        (Expr (Evar (ident_of_nat 0))
    1414          (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
    1515        [(Expr (Econst_int (repr 10)) (Tint I32 Signed  ))])
    16       (Sassign (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  ))
     16      (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    1717        (Expr (Ebinop Oadd
    18           (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  ))
    19           (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  )))
     18          (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
     19          (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
    2020          (Tint I32 Signed  ))))
    21       (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 2))
     21      (Sreturn (Some expr (Expr (Evar (ident_of_nat 2))
    2222                            (Tint I32 Signed  ))))))
    2323   
     
    2525   
    2626  )〉]
    27   (succ_pos_of_nat 1)
     27  (ident_of_nat 1)
    2828  []
    2929.
     
    3131example exec:
    3232 (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) =
    33  OK ? 〈[EVextcall (succ_pos_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 9〉.
     33 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 9〉.
    3434normalize  (* you can examine the result here *)
    3535@refl
  • src/Clight/test/search.ma

    r725 r726  
    22
    33definition myprog := mk_program clight_fundef type
    4   [〈succ_pos_of_nat 0 (* search *), CL_Internal (
    5      mk_function (Tint I8 Unsigned ) [〈succ_pos_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈succ_pos_of_nat 5, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 6, (Tint I8 Unsigned )〉 ] [〈succ_pos_of_nat 1, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 2, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 3, (Tint I8 Unsigned )〉 ]
     4  [〈ident_of_nat 0 (* search *), CL_Internal (
     5     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 )〉 ]
    66       (Ssequence
    7        (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I8 Unsigned ))
     7       (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    88         (Expr (Ecast (Tint I8 Unsigned )
    99           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    1010           (Tint I8 Unsigned )))
    1111       (Ssequence
    12        (Sassign (Expr (Evar (succ_pos_of_nat 2)) (Tint I8 Unsigned ))
     12       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    1313         (Expr (Ecast (Tint I8 Unsigned )
    1414           (Expr (Ebinop Osub
    1515             (Expr (Ecast (Tint I32 Signed  )
    16                (Expr (Evar (succ_pos_of_nat 5)) (Tint I8 Unsigned )))
     16               (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
    1717               (Tint I32 Signed  ))
    1818             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    2222       (Swhile (Expr (Ebinop Oge
    2323                 (Expr (Ecast (Tint I32 Signed  )
    24                    (Expr (Evar (succ_pos_of_nat 2)) (Tint I8 Unsigned )))
     24                   (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    2525                   (Tint I32 Signed  ))
    2626                 (Expr (Ecast (Tint I32 Signed  )
    27                    (Expr (Evar (succ_pos_of_nat 1)) (Tint I8 Unsigned )))
     27                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    2828                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
    2929         (Ssequence
    30          (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I8 Unsigned ))
     30         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    3131           (Expr (Ecast (Tint I8 Unsigned )
    3232             (Expr (Ebinop Odiv
    3333               (Expr (Ebinop Oadd
    3434                 (Expr (Ecast (Tint I32 Signed  )
    35                    (Expr (Evar (succ_pos_of_nat 2)) (Tint I8 Unsigned )))
     35                   (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    3636                   (Tint I32 Signed  ))
    3737                 (Expr (Ecast (Tint I32 Signed  )
    38                    (Expr (Evar (succ_pos_of_nat 1)) (Tint I8 Unsigned )))
     38                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    3939                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
    4040               (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
     
    4545                          (Expr (Ederef
    4646                            (Expr (Ebinop Oadd
    47                               (Expr (Evar (succ_pos_of_nat 4))
     47                              (Expr (Evar (ident_of_nat 4))
    4848                                (Tpointer Any (Tint I8 Unsigned )))
    49                               (Expr (Evar (succ_pos_of_nat 3))
     49                              (Expr (Evar (ident_of_nat 3))
    5050                                (Tint I8 Unsigned )))
    5151                              (Tpointer Any (Tint I8 Unsigned ))))
    5252                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    5353                        (Expr (Ecast (Tint I32 Signed  )
    54                           (Expr (Evar (succ_pos_of_nat 6))
     54                          (Expr (Evar (ident_of_nat 6))
    5555                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    5656                        (Tint I32 Signed  ))
    57            (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 3))
     57           (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
    5858                                 (Tint I8 Unsigned ))))
    5959           Sskip)
     
    6363                          (Expr (Ederef
    6464                            (Expr (Ebinop Oadd
    65                               (Expr (Evar (succ_pos_of_nat 4))
     65                              (Expr (Evar (ident_of_nat 4))
    6666                                (Tpointer Any (Tint I8 Unsigned )))
    67                               (Expr (Evar (succ_pos_of_nat 3))
     67                              (Expr (Evar (ident_of_nat 3))
    6868                                (Tint I8 Unsigned )))
    6969                              (Tpointer Any (Tint I8 Unsigned ))))
    7070                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    7171                        (Expr (Ecast (Tint I32 Signed  )
    72                           (Expr (Evar (succ_pos_of_nat 6))
     72                          (Expr (Evar (ident_of_nat 6))
    7373                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    7474                        (Tint I32 Signed  ))
    75            (Sassign (Expr (Evar (succ_pos_of_nat 2)) (Tint I8 Unsigned ))
     75           (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    7676             (Expr (Ecast (Tint I8 Unsigned )
    7777               (Expr (Ebinop Osub
    7878                 (Expr (Ecast (Tint I32 Signed  )
    79                    (Expr (Evar (succ_pos_of_nat 3)) (Tint I8 Unsigned )))
     79                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    8080                   (Tint I32 Signed  ))
    8181                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    8686                          (Expr (Ederef
    8787                            (Expr (Ebinop Oadd
    88                               (Expr (Evar (succ_pos_of_nat 4))
     88                              (Expr (Evar (ident_of_nat 4))
    8989                                (Tpointer Any (Tint I8 Unsigned )))
    90                               (Expr (Evar (succ_pos_of_nat 3))
     90                              (Expr (Evar (ident_of_nat 3))
    9191                                (Tint I8 Unsigned )))
    9292                              (Tpointer Any (Tint I8 Unsigned ))))
    9393                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    9494                        (Expr (Ecast (Tint I32 Signed  )
    95                           (Expr (Evar (succ_pos_of_nat 6))
     95                          (Expr (Evar (ident_of_nat 6))
    9696                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    9797                        (Tint I32 Signed  ))
    98            (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I8 Unsigned ))
     98           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    9999             (Expr (Ecast (Tint I8 Unsigned )
    100100               (Expr (Ebinop Oadd
    101101                 (Expr (Ecast (Tint I32 Signed  )
    102                    (Expr (Evar (succ_pos_of_nat 3)) (Tint I8 Unsigned )))
     102                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    103103                   (Tint I32 Signed  ))
    104104                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    114114     
    115115   )〉;
    116   〈succ_pos_of_nat 7 (* main *), CL_Internal (
    117     mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈succ_pos_of_nat 8, (Tint I8 Unsigned )〉 ]
     116  〈ident_of_nat 7 (* main *), CL_Internal (
     117    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ]
    118118      (Ssequence
    119119      (Sassign (Expr (Ederef
    120120                 (Expr (Ebinop Oadd
    121                    (Expr (Evar (succ_pos_of_nat 4))
     121                   (Expr (Evar (ident_of_nat 4))
    122122                     (Tarray Any (Tint I8 Unsigned ) 5))
    123123                   (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     
    129129      (Sassign (Expr (Ederef
    130130                 (Expr (Ebinop Oadd
    131                    (Expr (Evar (succ_pos_of_nat 4))
     131                   (Expr (Evar (ident_of_nat 4))
    132132                     (Tarray Any (Tint I8 Unsigned ) 5))
    133133                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    139139      (Sassign (Expr (Ederef
    140140                 (Expr (Ebinop Oadd
    141                    (Expr (Evar (succ_pos_of_nat 4))
     141                   (Expr (Evar (ident_of_nat 4))
    142142                     (Tarray Any (Tint I8 Unsigned ) 5))
    143143                   (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
     
    149149      (Sassign (Expr (Ederef
    150150                 (Expr (Ebinop Oadd
    151                    (Expr (Evar (succ_pos_of_nat 4))
     151                   (Expr (Evar (ident_of_nat 4))
    152152                     (Tarray Any (Tint I8 Unsigned ) 5))
    153153                   (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
     
    159159      (Sassign (Expr (Ederef
    160160                 (Expr (Ebinop Oadd
    161                    (Expr (Evar (succ_pos_of_nat 4))
     161                   (Expr (Evar (ident_of_nat 4))
    162162                     (Tarray Any (Tint I8 Unsigned ) 5))
    163163                   (Expr (Econst_int (repr 4)) (Tint I32 Signed  )))
     
    167167          (Tint I8 Unsigned )))
    168168      (Ssequence
    169       (Scall (Some expr (Expr (Evar (succ_pos_of_nat 8)) (Tint I8 Unsigned )))
    170         (Expr (Evar (succ_pos_of_nat 0))
     169      (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned )))
     170        (Expr (Evar (ident_of_nat 0))
    171171          (Tfunction (Tcons (Tpointer Any (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned )))
    172         [(Expr (Evar (succ_pos_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
     172        [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
    173173        (Expr (Ecast (Tint I8 Unsigned )
    174174          (Expr (Econst_int (repr 5)) (Tint I32 Signed  )))
     
    178178          (Tint I8 Unsigned ))])
    179179      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    180                             (Expr (Evar (succ_pos_of_nat 8))
     180                            (Expr (Evar (ident_of_nat 8))
    181181                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))))))
    182182   
     
    184184   
    185185  )〉]
    186   (succ_pos_of_nat 7)
     186  (ident_of_nat 7)
    187187  []
    188188.
     
    190190example exec: result ? (exec_up_to myprog 1000 [EVint (repr 0)]).
    191191normalize  (* you can examine the result here *)
     192%
     193qed.
Note: See TracChangeset for help on using the changeset viewer.