Ignore:
Timestamp:
Mar 29, 2011, 5:54:36 PM (9 years ago)
Author:
campbell
Message:

Clean up Clight examples; better temporary definition of multiply.

File:
1 edited

Legend:

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

    r415 r717  
    1 include "Animation.ma".
     1include "Clight/Animation.ma".
    22
    3 (* This definition takes a long time to be accepted. *)
    4 
    5 ndefinition myprog := mk_program fundef type
    6   [mk_pair ?? (succ_pos_of_nat 132 (* copy *)) (Internal (
    7     mk_function Tvoid [mk_pair ?? (succ_pos_of_nat 151) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 152) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 153) (Tint I32 Signed  )] [mk_pair ?? (succ_pos_of_nat 133) (Tint I32 Signed  ); mk_pair ?? (succ_pos_of_nat 134) (Tint I32 Signed  ); mk_pair ?? (succ_pos_of_nat 135) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 136) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 137) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 138) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 139) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 140) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 141) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 142) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 143) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 144) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 145) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 146) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 147) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 148) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 149) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 150) (Tpointer Any (Tint I16 Signed  ))]
    8       (Ssequence
    9       (Sassign (Expr (Evar (succ_pos_of_nat 133)) (Tint I32 Signed  ))
    10         (Expr (Ebinop Odiv
    11           (Expr (Ebinop Oadd
    12             (Expr (Evar (succ_pos_of_nat 153)) (Tint I32 Signed  ))
    13             (Expr (Econst_int (repr 7)) (Tint I32 Signed  )))
    14             (Tint I32 Signed  ))
    15           (Expr (Econst_int (repr 8)) (Tint I32 Signed  )))
    16           (Tint I32 Signed  )))
    17       (Sswitch (Expr (Ebinop Omod
    18                  (Expr (Evar (succ_pos_of_nat 153)) (Tint I32 Signed  ))
    19                  (Expr (Econst_int (repr 8)) (Tint I32 Signed  )))
    20                  (Tint I32 Signed  )) (
    21         (LScase (repr 0)
    22           (Slabel (succ_pos_of_nat 154)
    23           (Ssequence
    24           (Ssequence
    25           (Sassign (Expr (Evar (succ_pos_of_nat 149))
     3definition myprog := mk_program fundef type
     4  [〈succ_pos_of_nat 0 (* copy *), 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  ))〉 ]
     6       (Ssequence
     7       (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I32 Signed  ))
     8         (Expr (Ebinop Odiv
     9           (Expr (Ebinop Oadd
     10             (Expr (Evar (succ_pos_of_nat 21)) (Tint I32 Signed  ))
     11             (Expr (Econst_int (repr 7)) (Tint I32 Signed  )))
     12             (Tint I32 Signed  ))
     13           (Expr (Econst_int (repr 8)) (Tint I32 Signed  )))
     14           (Tint I32 Signed  )))
     15       (Sswitch (Expr (Ebinop Omod
     16                  (Expr (Evar (succ_pos_of_nat 21)) (Tint I32 Signed  ))
     17                  (Expr (Econst_int (repr 8)) (Tint I32 Signed  )))
     18                  (Tint I32 Signed  )) (
     19         (LScase (repr 0)
     20           (Slabel (succ_pos_of_nat 22)
     21           (Ssequence
     22           (Ssequence
     23           (Sassign (Expr (Evar (succ_pos_of_nat 17))
     24                      (Tpointer Any (Tint I16 Signed  )))
     25             (Expr (Evar (succ_pos_of_nat 19))
     26               (Tpointer Any (Tint I16 Signed  ))))
     27           (Sassign (Expr (Evar (succ_pos_of_nat 19))
     28                      (Tpointer Any (Tint I16 Signed  )))
     29             (Expr (Ebinop Oadd
     30               (Expr (Evar (succ_pos_of_nat 17))
     31                 (Tpointer Any (Tint I16 Signed  )))
     32               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     33               (Tpointer Any (Tint I16 Signed  )))))
     34           (Ssequence
     35           (Ssequence
     36           (Sassign (Expr (Evar (succ_pos_of_nat 18))
     37                      (Tpointer Any (Tint I16 Signed  )))
     38             (Expr (Evar (succ_pos_of_nat 20))
     39               (Tpointer Any (Tint I16 Signed  ))))
     40           (Sassign (Expr (Evar (succ_pos_of_nat 20))
     41                      (Tpointer Any (Tint I16 Signed  )))
     42             (Expr (Ebinop Oadd
     43               (Expr (Evar (succ_pos_of_nat 18))
     44                 (Tpointer Any (Tint I16 Signed  )))
     45               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     46               (Tpointer Any (Tint I16 Signed  )))))
     47           (Sassign (Expr (Ederef
     48                      (Expr (Evar (succ_pos_of_nat 17))
     49                        (Tpointer Any (Tint I16 Signed  ))))
     50                      (Tint I16 Signed  ))
     51             (Expr (Ederef
     52               (Expr (Evar (succ_pos_of_nat 18))
     53                 (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
     54           (LScase (repr 7)
     55             (Ssequence
     56             (Sassign (Expr (Evar (succ_pos_of_nat 15))
     57                        (Tpointer Any (Tint I16 Signed  )))
     58               (Expr (Evar (succ_pos_of_nat 19))
     59                 (Tpointer Any (Tint I16 Signed  ))))
     60             (Ssequence
     61             (Sassign (Expr (Evar (succ_pos_of_nat 19))
     62                        (Tpointer Any (Tint I16 Signed  )))
     63               (Expr (Ebinop Oadd
     64                 (Expr (Evar (succ_pos_of_nat 15))
     65                   (Tpointer Any (Tint I16 Signed  )))
     66                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     67                 (Tpointer Any (Tint I16 Signed  ))))
     68             (Ssequence
     69             (Sassign (Expr (Evar (succ_pos_of_nat 16))
     70                        (Tpointer Any (Tint I16 Signed  )))
     71               (Expr (Evar (succ_pos_of_nat 20))
     72                 (Tpointer Any (Tint I16 Signed  ))))
     73             (Ssequence
     74             (Sassign (Expr (Evar (succ_pos_of_nat 20))
     75                        (Tpointer Any (Tint I16 Signed  )))
     76               (Expr (Ebinop Oadd
     77                 (Expr (Evar (succ_pos_of_nat 16))
     78                   (Tpointer Any (Tint I16 Signed  )))
     79                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     80                 (Tpointer Any (Tint I16 Signed  ))))
     81             (Sassign (Expr (Ederef
     82                        (Expr (Evar (succ_pos_of_nat 15))
     83                          (Tpointer Any (Tint I16 Signed  ))))
     84                        (Tint I16 Signed  ))
     85               (Expr (Ederef
     86                 (Expr (Evar (succ_pos_of_nat 16))
     87                   (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
     88             (LScase (repr 6)
     89               (Ssequence
     90               (Sassign (Expr (Evar (succ_pos_of_nat 13))
     91                          (Tpointer Any (Tint I16 Signed  )))
     92                 (Expr (Evar (succ_pos_of_nat 19))
     93                   (Tpointer Any (Tint I16 Signed  ))))
     94               (Ssequence
     95               (Sassign (Expr (Evar (succ_pos_of_nat 19))
     96                          (Tpointer Any (Tint I16 Signed  )))
     97                 (Expr (Ebinop Oadd
     98                   (Expr (Evar (succ_pos_of_nat 13))
    2699                     (Tpointer Any (Tint I16 Signed  )))
    27             (Expr (Evar (succ_pos_of_nat 151))
    28               (Tpointer Any (Tint I16 Signed  ))))
    29           (Sassign (Expr (Evar (succ_pos_of_nat 151))
     100                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     101                   (Tpointer Any (Tint I16 Signed  ))))
     102               (Ssequence
     103               (Sassign (Expr (Evar (succ_pos_of_nat 14))
     104                          (Tpointer Any (Tint I16 Signed  )))
     105                 (Expr (Evar (succ_pos_of_nat 20))
     106                   (Tpointer Any (Tint I16 Signed  ))))
     107               (Ssequence
     108               (Sassign (Expr (Evar (succ_pos_of_nat 20))
     109                          (Tpointer Any (Tint I16 Signed  )))
     110                 (Expr (Ebinop Oadd
     111                   (Expr (Evar (succ_pos_of_nat 14))
    30112                     (Tpointer Any (Tint I16 Signed  )))
    31             (Expr (Ebinop Oadd
    32               (Expr (Evar (succ_pos_of_nat 149))
    33                 (Tpointer Any (Tint I16 Signed  )))
    34               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    35               (Tpointer Any (Tint I16 Signed  )))))
    36           (Ssequence
    37           (Ssequence
    38           (Sassign (Expr (Evar (succ_pos_of_nat 150))
    39                      (Tpointer Any (Tint I16 Signed  )))
    40             (Expr (Evar (succ_pos_of_nat 152))
    41               (Tpointer Any (Tint I16 Signed  ))))
    42           (Sassign (Expr (Evar (succ_pos_of_nat 152))
    43                      (Tpointer Any (Tint I16 Signed  )))
    44             (Expr (Ebinop Oadd
    45               (Expr (Evar (succ_pos_of_nat 150))
    46                 (Tpointer Any (Tint I16 Signed  )))
    47               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    48               (Tpointer Any (Tint I16 Signed  )))))
    49           (Sassign (Expr (Ederef
    50                      (Expr (Evar (succ_pos_of_nat 149))
     113                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     114                   (Tpointer Any (Tint I16 Signed  ))))
     115               (Sassign (Expr (Ederef
     116                          (Expr (Evar (succ_pos_of_nat 13))
     117                            (Tpointer Any (Tint I16 Signed  ))))
     118                          (Tint I16 Signed  ))
     119                 (Expr (Ederef
     120                   (Expr (Evar (succ_pos_of_nat 14))
     121                     (Tpointer Any (Tint I16 Signed  ))))
     122                   (Tint I16 Signed  )))))))
     123               (LScase (repr 5)
     124                 (Ssequence
     125                 (Sassign (Expr (Evar (succ_pos_of_nat 11))
     126                            (Tpointer Any (Tint I16 Signed  )))
     127                   (Expr (Evar (succ_pos_of_nat 19))
     128                     (Tpointer Any (Tint I16 Signed  ))))
     129                 (Ssequence
     130                 (Sassign (Expr (Evar (succ_pos_of_nat 19))
     131                            (Tpointer Any (Tint I16 Signed  )))
     132                   (Expr (Ebinop Oadd
     133                     (Expr (Evar (succ_pos_of_nat 11))
     134                       (Tpointer Any (Tint I16 Signed  )))
     135                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     136                     (Tpointer Any (Tint I16 Signed  ))))
     137                 (Ssequence
     138                 (Sassign (Expr (Evar (succ_pos_of_nat 12))
     139                            (Tpointer Any (Tint I16 Signed  )))
     140                   (Expr (Evar (succ_pos_of_nat 20))
     141                     (Tpointer Any (Tint I16 Signed  ))))
     142                 (Ssequence
     143                 (Sassign (Expr (Evar (succ_pos_of_nat 20))
     144                            (Tpointer Any (Tint I16 Signed  )))
     145                   (Expr (Ebinop Oadd
     146                     (Expr (Evar (succ_pos_of_nat 12))
     147                       (Tpointer Any (Tint I16 Signed  )))
     148                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     149                     (Tpointer Any (Tint I16 Signed  ))))
     150                 (Sassign (Expr (Ederef
     151                            (Expr (Evar (succ_pos_of_nat 11))
     152                              (Tpointer Any (Tint I16 Signed  ))))
     153                            (Tint I16 Signed  ))
     154                   (Expr (Ederef
     155                     (Expr (Evar (succ_pos_of_nat 12))
    51156                       (Tpointer Any (Tint I16 Signed  ))))
    52                      (Tint I16 Signed  ))
    53             (Expr (Ederef
    54               (Expr (Evar (succ_pos_of_nat 150))
    55                 (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
    56           (LScase (repr 7)
    57             (Ssequence
    58             (Sassign (Expr (Evar (succ_pos_of_nat 147))
    59                        (Tpointer Any (Tint I16 Signed  )))
    60               (Expr (Evar (succ_pos_of_nat 151))
    61                 (Tpointer Any (Tint I16 Signed  ))))
    62             (Ssequence
    63             (Sassign (Expr (Evar (succ_pos_of_nat 151))
    64                        (Tpointer Any (Tint I16 Signed  )))
    65               (Expr (Ebinop Oadd
    66                 (Expr (Evar (succ_pos_of_nat 147))
    67                   (Tpointer Any (Tint I16 Signed  )))
    68                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    69                 (Tpointer Any (Tint I16 Signed  ))))
    70             (Ssequence
    71             (Sassign (Expr (Evar (succ_pos_of_nat 148))
    72                        (Tpointer Any (Tint I16 Signed  )))
    73               (Expr (Evar (succ_pos_of_nat 152))
    74                 (Tpointer Any (Tint I16 Signed  ))))
    75             (Ssequence
    76             (Sassign (Expr (Evar (succ_pos_of_nat 152))
    77                        (Tpointer Any (Tint I16 Signed  )))
    78               (Expr (Ebinop Oadd
    79                 (Expr (Evar (succ_pos_of_nat 148))
    80                   (Tpointer Any (Tint I16 Signed  )))
    81                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    82                 (Tpointer Any (Tint I16 Signed  ))))
    83             (Sassign (Expr (Ederef
    84                        (Expr (Evar (succ_pos_of_nat 147))
     157                     (Tint I16 Signed  )))))))
     158                 (LScase (repr 4)
     159                   (Ssequence
     160                   (Sassign (Expr (Evar (succ_pos_of_nat 9))
     161                              (Tpointer Any (Tint I16 Signed  )))
     162                     (Expr (Evar (succ_pos_of_nat 19))
     163                       (Tpointer Any (Tint I16 Signed  ))))
     164                   (Ssequence
     165                   (Sassign (Expr (Evar (succ_pos_of_nat 19))
     166                              (Tpointer Any (Tint I16 Signed  )))
     167                     (Expr (Ebinop Oadd
     168                       (Expr (Evar (succ_pos_of_nat 9))
     169                         (Tpointer Any (Tint I16 Signed  )))
     170                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     171                       (Tpointer Any (Tint I16 Signed  ))))
     172                   (Ssequence
     173                   (Sassign (Expr (Evar (succ_pos_of_nat 10))
     174                              (Tpointer Any (Tint I16 Signed  )))
     175                     (Expr (Evar (succ_pos_of_nat 20))
     176                       (Tpointer Any (Tint I16 Signed  ))))
     177                   (Ssequence
     178                   (Sassign (Expr (Evar (succ_pos_of_nat 20))
     179                              (Tpointer Any (Tint I16 Signed  )))
     180                     (Expr (Ebinop Oadd
     181                       (Expr (Evar (succ_pos_of_nat 10))
     182                         (Tpointer Any (Tint I16 Signed  )))
     183                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     184                       (Tpointer Any (Tint I16 Signed  ))))
     185                   (Sassign (Expr (Ederef
     186                              (Expr (Evar (succ_pos_of_nat 9))
     187                                (Tpointer Any (Tint I16 Signed  ))))
     188                              (Tint I16 Signed  ))
     189                     (Expr (Ederef
     190                       (Expr (Evar (succ_pos_of_nat 10))
    85191                         (Tpointer Any (Tint I16 Signed  ))))
    86                        (Tint I16 Signed  ))
    87               (Expr (Ederef
    88                 (Expr (Evar (succ_pos_of_nat 148))
    89                   (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
    90             (LScase (repr 6)
    91               (Ssequence
    92               (Sassign (Expr (Evar (succ_pos_of_nat 145))
    93                          (Tpointer Any (Tint I16 Signed  )))
    94                 (Expr (Evar (succ_pos_of_nat 151))
    95                   (Tpointer Any (Tint I16 Signed  ))))
    96               (Ssequence
    97               (Sassign (Expr (Evar (succ_pos_of_nat 151))
    98                          (Tpointer Any (Tint I16 Signed  )))
    99                 (Expr (Ebinop Oadd
    100                   (Expr (Evar (succ_pos_of_nat 145))
    101                     (Tpointer Any (Tint I16 Signed  )))
    102                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    103                   (Tpointer Any (Tint I16 Signed  ))))
    104               (Ssequence
    105               (Sassign (Expr (Evar (succ_pos_of_nat 146))
    106                          (Tpointer Any (Tint I16 Signed  )))
    107                 (Expr (Evar (succ_pos_of_nat 152))
    108                   (Tpointer Any (Tint I16 Signed  ))))
    109               (Ssequence
    110               (Sassign (Expr (Evar (succ_pos_of_nat 152))
    111                          (Tpointer Any (Tint I16 Signed  )))
    112                 (Expr (Ebinop Oadd
    113                   (Expr (Evar (succ_pos_of_nat 146))
    114                     (Tpointer Any (Tint I16 Signed  )))
    115                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    116                   (Tpointer Any (Tint I16 Signed  ))))
    117               (Sassign (Expr (Ederef
    118                          (Expr (Evar (succ_pos_of_nat 145))
     192                       (Tint I16 Signed  )))))))
     193                   (LScase (repr 3)
     194                     (Ssequence
     195                     (Sassign (Expr (Evar (succ_pos_of_nat 7))
     196                                (Tpointer Any (Tint I16 Signed  )))
     197                       (Expr (Evar (succ_pos_of_nat 19))
     198                         (Tpointer Any (Tint I16 Signed  ))))
     199                     (Ssequence
     200                     (Sassign (Expr (Evar (succ_pos_of_nat 19))
     201                                (Tpointer Any (Tint I16 Signed  )))
     202                       (Expr (Ebinop Oadd
     203                         (Expr (Evar (succ_pos_of_nat 7))
     204                           (Tpointer Any (Tint I16 Signed  )))
     205                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     206                         (Tpointer Any (Tint I16 Signed  ))))
     207                     (Ssequence
     208                     (Sassign (Expr (Evar (succ_pos_of_nat 8))
     209                                (Tpointer Any (Tint I16 Signed  )))
     210                       (Expr (Evar (succ_pos_of_nat 20))
     211                         (Tpointer Any (Tint I16 Signed  ))))
     212                     (Ssequence
     213                     (Sassign (Expr (Evar (succ_pos_of_nat 20))
     214                                (Tpointer Any (Tint I16 Signed  )))
     215                       (Expr (Ebinop Oadd
     216                         (Expr (Evar (succ_pos_of_nat 8))
     217                           (Tpointer Any (Tint I16 Signed  )))
     218                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     219                         (Tpointer Any (Tint I16 Signed  ))))
     220                     (Sassign (Expr (Ederef
     221                                (Expr (Evar (succ_pos_of_nat 7))
     222                                  (Tpointer Any (Tint I16 Signed  ))))
     223                                (Tint I16 Signed  ))
     224                       (Expr (Ederef
     225                         (Expr (Evar (succ_pos_of_nat 8))
    119226                           (Tpointer Any (Tint I16 Signed  ))))
    120                          (Tint I16 Signed  ))
    121                 (Expr (Ederef
    122                   (Expr (Evar (succ_pos_of_nat 146))
    123                     (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
    124               (LScase (repr 5)
    125                 (Ssequence
    126                 (Sassign (Expr (Evar (succ_pos_of_nat 143))
    127                            (Tpointer Any (Tint I16 Signed  )))
    128                   (Expr (Evar (succ_pos_of_nat 151))
    129                     (Tpointer Any (Tint I16 Signed  ))))
    130                 (Ssequence
    131                 (Sassign (Expr (Evar (succ_pos_of_nat 151))
    132                            (Tpointer Any (Tint I16 Signed  )))
    133                   (Expr (Ebinop Oadd
    134                     (Expr (Evar (succ_pos_of_nat 143))
    135                       (Tpointer Any (Tint I16 Signed  )))
    136                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    137                     (Tpointer Any (Tint I16 Signed  ))))
    138                 (Ssequence
    139                 (Sassign (Expr (Evar (succ_pos_of_nat 144))
    140                            (Tpointer Any (Tint I16 Signed  )))
    141                   (Expr (Evar (succ_pos_of_nat 152))
    142                     (Tpointer Any (Tint I16 Signed  ))))
    143                 (Ssequence
    144                 (Sassign (Expr (Evar (succ_pos_of_nat 152))
    145                            (Tpointer Any (Tint I16 Signed  )))
    146                   (Expr (Ebinop Oadd
    147                     (Expr (Evar (succ_pos_of_nat 144))
    148                       (Tpointer Any (Tint I16 Signed  )))
    149                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    150                     (Tpointer Any (Tint I16 Signed  ))))
    151                 (Sassign (Expr (Ederef
    152                            (Expr (Evar (succ_pos_of_nat 143))
     227                         (Tint I16 Signed  )))))))
     228                     (LScase (repr 2)
     229                       (Ssequence
     230                       (Sassign (Expr (Evar (succ_pos_of_nat 5))
     231                                  (Tpointer Any (Tint I16 Signed  )))
     232                         (Expr (Evar (succ_pos_of_nat 19))
     233                           (Tpointer Any (Tint I16 Signed  ))))
     234                       (Ssequence
     235                       (Sassign (Expr (Evar (succ_pos_of_nat 19))
     236                                  (Tpointer Any (Tint I16 Signed  )))
     237                         (Expr (Ebinop Oadd
     238                           (Expr (Evar (succ_pos_of_nat 5))
     239                             (Tpointer Any (Tint I16 Signed  )))
     240                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     241                           (Tpointer Any (Tint I16 Signed  ))))
     242                       (Ssequence
     243                       (Sassign (Expr (Evar (succ_pos_of_nat 6))
     244                                  (Tpointer Any (Tint I16 Signed  )))
     245                         (Expr (Evar (succ_pos_of_nat 20))
     246                           (Tpointer Any (Tint I16 Signed  ))))
     247                       (Ssequence
     248                       (Sassign (Expr (Evar (succ_pos_of_nat 20))
     249                                  (Tpointer Any (Tint I16 Signed  )))
     250                         (Expr (Ebinop Oadd
     251                           (Expr (Evar (succ_pos_of_nat 6))
     252                             (Tpointer Any (Tint I16 Signed  )))
     253                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     254                           (Tpointer Any (Tint I16 Signed  ))))
     255                       (Sassign (Expr (Ederef
     256                                  (Expr (Evar (succ_pos_of_nat 5))
     257                                    (Tpointer Any (Tint I16 Signed  ))))
     258                                  (Tint I16 Signed  ))
     259                         (Expr (Ederef
     260                           (Expr (Evar (succ_pos_of_nat 6))
    153261                             (Tpointer Any (Tint I16 Signed  ))))
    154                            (Tint I16 Signed  ))
    155                   (Expr (Ederef
    156                     (Expr (Evar (succ_pos_of_nat 144))
    157                       (Tpointer Any (Tint I16 Signed  ))))
    158                     (Tint I16 Signed  )))))))
    159                 (LScase (repr 4)
    160                   (Ssequence
    161                   (Sassign (Expr (Evar (succ_pos_of_nat 141))
    162                              (Tpointer Any (Tint I16 Signed  )))
    163                     (Expr (Evar (succ_pos_of_nat 151))
    164                       (Tpointer Any (Tint I16 Signed  ))))
    165                   (Ssequence
    166                   (Sassign (Expr (Evar (succ_pos_of_nat 151))
    167                              (Tpointer Any (Tint I16 Signed  )))
    168                     (Expr (Ebinop Oadd
    169                       (Expr (Evar (succ_pos_of_nat 141))
    170                         (Tpointer Any (Tint I16 Signed  )))
    171                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    172                       (Tpointer Any (Tint I16 Signed  ))))
    173                   (Ssequence
    174                   (Sassign (Expr (Evar (succ_pos_of_nat 142))
    175                              (Tpointer Any (Tint I16 Signed  )))
    176                     (Expr (Evar (succ_pos_of_nat 152))
    177                       (Tpointer Any (Tint I16 Signed  ))))
    178                   (Ssequence
    179                   (Sassign (Expr (Evar (succ_pos_of_nat 152))
    180                              (Tpointer Any (Tint I16 Signed  )))
    181                     (Expr (Ebinop Oadd
    182                       (Expr (Evar (succ_pos_of_nat 142))
    183                         (Tpointer Any (Tint I16 Signed  )))
    184                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    185                       (Tpointer Any (Tint I16 Signed  ))))
    186                   (Sassign (Expr (Ederef
    187                              (Expr (Evar (succ_pos_of_nat 141))
     262                           (Tint I16 Signed  )))))))
     263                       (LScase (repr 1)
     264                         (Ssequence
     265                         (Sassign (Expr (Evar (succ_pos_of_nat 3))
     266                                    (Tpointer Any (Tint I16 Signed  )))
     267                           (Expr (Evar (succ_pos_of_nat 19))
     268                             (Tpointer Any (Tint I16 Signed  ))))
     269                         (Ssequence
     270                         (Sassign (Expr (Evar (succ_pos_of_nat 19))
     271                                    (Tpointer Any (Tint I16 Signed  )))
     272                           (Expr (Ebinop Oadd
     273                             (Expr (Evar (succ_pos_of_nat 3))
     274                               (Tpointer Any (Tint I16 Signed  )))
     275                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     276                             (Tpointer Any (Tint I16 Signed  ))))
     277                         (Ssequence
     278                         (Sassign (Expr (Evar (succ_pos_of_nat 4))
     279                                    (Tpointer Any (Tint I16 Signed  )))
     280                           (Expr (Evar (succ_pos_of_nat 20))
     281                             (Tpointer Any (Tint I16 Signed  ))))
     282                         (Ssequence
     283                         (Sassign (Expr (Evar (succ_pos_of_nat 20))
     284                                    (Tpointer Any (Tint I16 Signed  )))
     285                           (Expr (Ebinop Oadd
     286                             (Expr (Evar (succ_pos_of_nat 4))
     287                               (Tpointer Any (Tint I16 Signed  )))
     288                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     289                             (Tpointer Any (Tint I16 Signed  ))))
     290                         (Ssequence
     291                         (Sassign (Expr (Ederef
     292                                    (Expr (Evar (succ_pos_of_nat 3))
     293                                      (Tpointer Any (Tint I16 Signed  ))))
     294                                    (Tint I16 Signed  ))
     295                           (Expr (Ederef
     296                             (Expr (Evar (succ_pos_of_nat 4))
    188297                               (Tpointer Any (Tint I16 Signed  ))))
    189                              (Tint I16 Signed  ))
    190                     (Expr (Ederef
    191                       (Expr (Evar (succ_pos_of_nat 142))
    192                         (Tpointer Any (Tint I16 Signed  ))))
    193                       (Tint I16 Signed  )))))))
    194                   (LScase (repr 3)
    195                     (Ssequence
    196                     (Sassign (Expr (Evar (succ_pos_of_nat 139))
    197                                (Tpointer Any (Tint I16 Signed  )))
    198                       (Expr (Evar (succ_pos_of_nat 151))
    199                         (Tpointer Any (Tint I16 Signed  ))))
    200                     (Ssequence
    201                     (Sassign (Expr (Evar (succ_pos_of_nat 151))
    202                                (Tpointer Any (Tint I16 Signed  )))
    203                       (Expr (Ebinop Oadd
    204                         (Expr (Evar (succ_pos_of_nat 139))
    205                           (Tpointer Any (Tint I16 Signed  )))
    206                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    207                         (Tpointer Any (Tint I16 Signed  ))))
    208                     (Ssequence
    209                     (Sassign (Expr (Evar (succ_pos_of_nat 140))
    210                                (Tpointer Any (Tint I16 Signed  )))
    211                       (Expr (Evar (succ_pos_of_nat 152))
    212                         (Tpointer Any (Tint I16 Signed  ))))
    213                     (Ssequence
    214                     (Sassign (Expr (Evar (succ_pos_of_nat 152))
    215                                (Tpointer Any (Tint I16 Signed  )))
    216                       (Expr (Ebinop Oadd
    217                         (Expr (Evar (succ_pos_of_nat 140))
    218                           (Tpointer Any (Tint I16 Signed  )))
    219                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    220                         (Tpointer Any (Tint I16 Signed  ))))
    221                     (Sassign (Expr (Ederef
    222                                (Expr (Evar (succ_pos_of_nat 139))
    223                                  (Tpointer Any (Tint I16 Signed  ))))
    224                                (Tint I16 Signed  ))
    225                       (Expr (Ederef
    226                         (Expr (Evar (succ_pos_of_nat 140))
    227                           (Tpointer Any (Tint I16 Signed  ))))
    228                         (Tint I16 Signed  )))))))
    229                     (LScase (repr 2)
    230                       (Ssequence
    231                       (Sassign (Expr (Evar (succ_pos_of_nat 137))
    232                                  (Tpointer Any (Tint I16 Signed  )))
    233                         (Expr (Evar (succ_pos_of_nat 151))
    234                           (Tpointer Any (Tint I16 Signed  ))))
    235                       (Ssequence
    236                       (Sassign (Expr (Evar (succ_pos_of_nat 151))
    237                                  (Tpointer Any (Tint I16 Signed  )))
    238                         (Expr (Ebinop Oadd
    239                           (Expr (Evar (succ_pos_of_nat 137))
    240                             (Tpointer Any (Tint I16 Signed  )))
    241                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    242                           (Tpointer Any (Tint I16 Signed  ))))
    243                       (Ssequence
    244                       (Sassign (Expr (Evar (succ_pos_of_nat 138))
    245                                  (Tpointer Any (Tint I16 Signed  )))
    246                         (Expr (Evar (succ_pos_of_nat 152))
    247                           (Tpointer Any (Tint I16 Signed  ))))
    248                       (Ssequence
    249                       (Sassign (Expr (Evar (succ_pos_of_nat 152))
    250                                  (Tpointer Any (Tint I16 Signed  )))
    251                         (Expr (Ebinop Oadd
    252                           (Expr (Evar (succ_pos_of_nat 138))
    253                             (Tpointer Any (Tint I16 Signed  )))
    254                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    255                           (Tpointer Any (Tint I16 Signed  ))))
    256                       (Sassign (Expr (Ederef
    257                                  (Expr (Evar (succ_pos_of_nat 137))
    258                                    (Tpointer Any (Tint I16 Signed  ))))
    259                                  (Tint I16 Signed  ))
    260                         (Expr (Ederef
    261                           (Expr (Evar (succ_pos_of_nat 138))
    262                             (Tpointer Any (Tint I16 Signed  ))))
    263                           (Tint I16 Signed  )))))))
    264                       (LScase (repr 1)
    265                         (Ssequence
    266                         (Sassign (Expr (Evar (succ_pos_of_nat 135))
    267                                    (Tpointer Any (Tint I16 Signed  )))
    268                           (Expr (Evar (succ_pos_of_nat 151))
    269                             (Tpointer Any (Tint I16 Signed  ))))
    270                         (Ssequence
    271                         (Sassign (Expr (Evar (succ_pos_of_nat 151))
    272                                    (Tpointer Any (Tint I16 Signed  )))
    273                           (Expr (Ebinop Oadd
    274                             (Expr (Evar (succ_pos_of_nat 135))
    275                               (Tpointer Any (Tint I16 Signed  )))
    276                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    277                             (Tpointer Any (Tint I16 Signed  ))))
    278                         (Ssequence
    279                         (Sassign (Expr (Evar (succ_pos_of_nat 136))
    280                                    (Tpointer Any (Tint I16 Signed  )))
    281                           (Expr (Evar (succ_pos_of_nat 152))
    282                             (Tpointer Any (Tint I16 Signed  ))))
    283                         (Ssequence
    284                         (Sassign (Expr (Evar (succ_pos_of_nat 152))
    285                                    (Tpointer Any (Tint I16 Signed  )))
    286                           (Expr (Ebinop Oadd
    287                             (Expr (Evar (succ_pos_of_nat 136))
    288                               (Tpointer Any (Tint I16 Signed  )))
    289                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    290                             (Tpointer Any (Tint I16 Signed  ))))
    291                         (Ssequence
    292                         (Sassign (Expr (Ederef
    293                                    (Expr (Evar (succ_pos_of_nat 135))
    294                                      (Tpointer Any (Tint I16 Signed  ))))
    295                                    (Tint I16 Signed  ))
    296                           (Expr (Ederef
    297                             (Expr (Evar (succ_pos_of_nat 136))
    298                               (Tpointer Any (Tint I16 Signed  ))))
    299                             (Tint I16 Signed  )))
    300                         (Ssequence
    301                         (Sassign (Expr (Evar (succ_pos_of_nat 134))
    302                                    (Tint I32 Signed  ))
    303                           (Expr (Ebinop Osub
    304                             (Expr (Evar (succ_pos_of_nat 133))
    305                               (Tint I32 Signed  ))
    306                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    307                             (Tint I32 Signed  )))
    308                         (Ssequence
    309                         (Sassign (Expr (Evar (succ_pos_of_nat 133))
    310                                    (Tint I32 Signed  ))
    311                           (Expr (Evar (succ_pos_of_nat 134))
    312                             (Tint I32 Signed  )))
    313                         (Sifthenelse (Expr (Ebinop Ogt
    314                                        (Expr (Evar (succ_pos_of_nat 134))
    315                                          (Tint I32 Signed  ))
    316                                        (Expr (Econst_int (repr 0))
    317                                          (Tint I32 Signed  )))
    318                                        (Tint I32 Signed  ))
    319                           (Sgoto (succ_pos_of_nat 154))
    320                           Sskip))))))))
    321                         (LSdefault
    322                           Sskip)))))))))
    323       )))
    324    
    325    
    326    
    327   ));
    328   mk_pair ?? (succ_pos_of_nat 155 (* main *)) (Internal (
    329     mk_function (Tint I32 Signed  ) [] [mk_pair ?? (succ_pos_of_nat 156) (Tarray Any (Tint I16 Signed  ) 3); mk_pair ?? (succ_pos_of_nat 157) (Tarray Any (Tint I16 Signed  ) 3)]
     298                             (Tint I16 Signed  )))
     299                         (Ssequence
     300                         (Sassign (Expr (Evar (succ_pos_of_nat 2))
     301                                    (Tint I32 Signed  ))
     302                           (Expr (Ebinop Osub
     303                             (Expr (Evar (succ_pos_of_nat 1))
     304                               (Tint I32 Signed  ))
     305                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     306                             (Tint I32 Signed  )))
     307                         (Ssequence
     308                         (Sassign (Expr (Evar (succ_pos_of_nat 1))
     309                                    (Tint I32 Signed  ))
     310                           (Expr (Evar (succ_pos_of_nat 2))
     311                             (Tint I32 Signed  )))
     312                         (Sifthenelse (Expr (Ebinop Ogt
     313                                        (Expr (Evar (succ_pos_of_nat 2))
     314                                          (Tint I32 Signed  ))
     315                                        (Expr (Econst_int (repr 0))
     316                                          (Tint I32 Signed  )))
     317                                        (Tint I32 Signed  ))
     318                           (Sgoto (succ_pos_of_nat 22))
     319                           Sskip))))))))
     320                         (LSdefault
     321                           Sskip)))))))))
     322       )))
     323     
     324     
     325     
     326   )〉;
     327  〈succ_pos_of_nat 23 (* main *), 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)〉 ]
    330329      (Ssequence
    331330      (Sassign (Expr (Ederef
    332331                 (Expr (Ebinop Oadd
    333                    (Expr (Evar (succ_pos_of_nat 156))
     332                   (Expr (Evar (succ_pos_of_nat 24))
    334333                     (Tarray Any (Tint I16 Signed  ) 3))
    335334                   (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     
    341340      (Sassign (Expr (Ederef
    342341                 (Expr (Ebinop Oadd
    343                    (Expr (Evar (succ_pos_of_nat 156))
     342                   (Expr (Evar (succ_pos_of_nat 24))
    344343                     (Tarray Any (Tint I16 Signed  ) 3))
    345344                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    351350      (Sassign (Expr (Ederef
    352351                 (Expr (Ebinop Oadd
    353                    (Expr (Evar (succ_pos_of_nat 156))
     352                   (Expr (Evar (succ_pos_of_nat 24))
    354353                     (Tarray Any (Tint I16 Signed  ) 3))
    355354                   (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
     
    359358          (Tint I16 Signed  )))
    360359      (Ssequence
    361       (Scall (None ?) (Expr (Evar (succ_pos_of_nat 132))
    362                         (Tfunction (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid))
    363         [(Expr (Evar (succ_pos_of_nat 157))
     360      (Scall (None expr) (Expr (Evar (succ_pos_of_nat 0))
     361                           (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))
    364363           (Tarray Any (Tint I16 Signed  ) 3));
    365         (Expr (Evar (succ_pos_of_nat 156))
    366           (Tarray Any (Tint I16 Signed  ) 3));
     364        (Expr (Evar (succ_pos_of_nat 24)) (Tarray Any (Tint I16 Signed  ) 3));
    367365        (Expr (Econst_int (repr 3)) (Tint I32 Signed  ))])
    368       (Sreturn (Some ? (Expr (Ebinop Oadd
    369                          (Expr (Ebinop Oadd
    370                            (Expr (Ecast (Tint I32 Signed  )
    371                              (Expr (Ederef
    372                                (Expr (Ebinop Oadd
    373                                  (Expr (Evar (succ_pos_of_nat 157))
    374                                    (Tarray Any (Tint I16 Signed  ) 3))
    375                                  (Expr (Econst_int (repr 0))
    376                                    (Tint I32 Signed  )))
    377                                  (Tarray Any (Tint I16 Signed  ) 3)))
    378                                (Tint I16 Signed  ))) (Tint I32 Signed  ))
    379                            (Expr (Ecast (Tint I32 Signed  )
    380                              (Expr (Ederef
    381                                (Expr (Ebinop Oadd
    382                                  (Expr (Evar (succ_pos_of_nat 157))
    383                                    (Tarray Any (Tint I16 Signed  ) 3))
    384                                  (Expr (Econst_int (repr 1))
    385                                    (Tint I32 Signed  )))
    386                                  (Tarray Any (Tint I16 Signed  ) 3)))
    387                                (Tint I16 Signed  ))) (Tint I32 Signed  )))
    388                            (Tint I32 Signed  ))
    389                          (Expr (Ecast (Tint I32 Signed  )
    390                            (Expr (Ederef
    391                              (Expr (Ebinop Oadd
    392                                (Expr (Evar (succ_pos_of_nat 157))
    393                                  (Tarray Any (Tint I16 Signed  ) 3))
    394                                (Expr (Econst_int (repr 2))
    395                                  (Tint I32 Signed  )))
    396                                (Tarray Any (Tint I16 Signed  ) 3)))
    397                              (Tint I16 Signed  ))) (Tint I32 Signed  )))
    398                          (Tint I32 Signed  ))))))))
     366      (Sreturn (Some expr (Expr (Ebinop Oadd
     367                            (Expr (Ebinop Oadd
     368                              (Expr (Ecast (Tint I32 Signed  )
     369                                (Expr (Ederef
     370                                  (Expr (Ebinop Oadd
     371                                    (Expr (Evar (succ_pos_of_nat 25))
     372                                      (Tarray Any (Tint I16 Signed  ) 3))
     373                                    (Expr (Econst_int (repr 0))
     374                                      (Tint I32 Signed  )))
     375                                    (Tarray Any (Tint I16 Signed  ) 3)))
     376                                  (Tint I16 Signed  ))) (Tint I32 Signed  ))
     377                              (Expr (Ecast (Tint I32 Signed  )
     378                                (Expr (Ederef
     379                                  (Expr (Ebinop Oadd
     380                                    (Expr (Evar (succ_pos_of_nat 25))
     381                                      (Tarray Any (Tint I16 Signed  ) 3))
     382                                    (Expr (Econst_int (repr 1))
     383                                      (Tint I32 Signed  )))
     384                                    (Tarray Any (Tint I16 Signed  ) 3)))
     385                                  (Tint I16 Signed  ))) (Tint I32 Signed  )))
     386                              (Tint I32 Signed  ))
     387                            (Expr (Ecast (Tint I32 Signed  )
     388                              (Expr (Ederef
     389                                (Expr (Ebinop Oadd
     390                                  (Expr (Evar (succ_pos_of_nat 25))
     391                                    (Tarray Any (Tint I16 Signed  ) 3))
     392                                  (Expr (Econst_int (repr 2))
     393                                    (Tint I32 Signed  )))
     394                                  (Tarray Any (Tint I16 Signed  ) 3)))
     395                                (Tint I16 Signed  ))) (Tint I32 Signed  )))
     396                            (Tint I32 Signed  ))))))))
    399397   
    400398   
    401399   
    402   ))]
    403   (succ_pos_of_nat 155)
     400  )]
     401  (succ_pos_of_nat 23)
    404402  []
    405403.
    406404
    407 nremark exec: result ? (exec_up_to myprog 80 []).
    408 nnormalize;  (* you can examine the result here *)
    409 @; nqed.
     405example exec:
     406  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 0)]; OK ? (is_final s)) = OK ? (Some ? (repr 6)).
     407normalize @refl
     408qed.
Note: See TracChangeset for help on using the changeset viewer.