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

Change identifiers to Words in Clight and RTLabs semantics.

File:
1 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.
Note: See TracChangeset for help on using the changeset viewer.