Changeset 1513 for src/Clight/test


Ignore:
Timestamp:
Nov 17, 2011, 4:50:46 PM (10 years ago)
Author:
campbell
Message:

Fix up Clight examples.

Location:
src/Clight/test
Files:
6 added
6 edited

Legend:

Unmodified
Added
Removed

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

    r1198 r1513  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef ((list init_data) × type)
    5   [〈ident_of_nat 0 (* main *), CL_Internal (
    6      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 4, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ]
    7        (Ssequence
    8        (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    9          (Expr (Ecast (Tint I8 Unsigned )
    10            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    11            (Tint I8 Unsigned )))
    12        (Ssequence
    13        (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    14          (Expr (Ecast (Tint I8 Unsigned )
    15            (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    16            (Tint I8 Unsigned )))
    17        (Ssequence
    18        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    19          (Expr (Ecast (Tint I8 Unsigned )
    20            (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
    21            (Tint I8 Unsigned )))
    22        (Ssequence
    23        (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I8 Unsigned ))
    24          (Expr (Ecast (Tint I8 Unsigned )
    25            (Expr (Ebinop Oadd
    26              (Expr (Ecast (Tint I32 Signed  )
    27                (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    28                (Tint I32 Signed  ))
    29              (Expr (Ecast (Tint I32 Signed  )
    30                (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    31                (Tint I32 Signed  ))) (Tint I32 Signed  )))
    32            (Tint I8 Unsigned )))
    33        (Ssequence
    34        (Sassign (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned ))
    35          (Expr (Ecast (Tint I8 Unsigned )
    36            (Expr (Ebinop Oadd
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [][〈ident_of_nat 0 (* main *), CL_Internal (
     6       mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 4, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ]
     7         (Ssequence
     8         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
     9           (Expr (Ecast (Tint I8 Unsigned )
     10             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     11             (Tint I8 Unsigned )))
     12         (Ssequence
     13         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     14           (Expr (Ecast (Tint I8 Unsigned )
     15             (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     16             (Tint I8 Unsigned )))
     17         (Ssequence
     18         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
     19           (Expr (Ecast (Tint I8 Unsigned )
     20             (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
     21             (Tint I8 Unsigned )))
     22         (Ssequence
     23         (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I8 Unsigned ))
     24           (Expr (Ecast (Tint I8 Unsigned )
    3725             (Expr (Ebinop Oadd
    3826               (Expr (Ecast (Tint I32 Signed  )
    … …  
    4129               (Expr (Ecast (Tint I32 Signed  )
    4230                 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    43                  (Tint I32 Signed  ))) (Tint I32 Signed  ))
    44              (Expr (Ecast (Tint I32 Signed  )
    45                (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    46                (Tint I32 Signed  ))) (Tint I32 Signed  )))
    47            (Tint I8 Unsigned )))
    48        (Sreturn (Some expr (Expr (Ebinop Oeq
    49                              (Expr (Ecast (Tint I32 Signed  )
    50                                (Expr (Evar (ident_of_nat 5))
    51                                  (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    52                              (Expr (Ebinop Oadd
     31                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
     32             (Tint I8 Unsigned )))
     33         (Ssequence
     34         (Sassign (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned ))
     35           (Expr (Ecast (Tint I8 Unsigned )
     36             (Expr (Ebinop Oadd
     37               (Expr (Ebinop Oadd
     38                 (Expr (Ecast (Tint I32 Signed  )
     39                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
     40                   (Tint I32 Signed  ))
     41                 (Expr (Ecast (Tint I32 Signed  )
     42                   (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
     43                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
     44               (Expr (Ecast (Tint I32 Signed  )
     45                 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
     46                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
     47             (Tint I8 Unsigned )))
     48         (Sreturn (Some expr (Expr (Ebinop Oeq
    5349                               (Expr (Ecast (Tint I32 Signed  )
    54                                  (Expr (Evar (ident_of_nat 4))
     50                                 (Expr (Evar (ident_of_nat 5))
    5551                                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    56                                (Expr (Ecast (Tint I32 Signed  )
    57                                  (Expr (Evar (ident_of_nat 3))
    58                                    (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    59                                (Tint I32 Signed  ))) (Tint I32 Signed  )))))))))
    60      
    61      
    62      
    63    )〉]
     52                               (Expr (Ebinop Oadd
     53                                 (Expr (Ecast (Tint I32 Signed  )
     54                                   (Expr (Evar (ident_of_nat 4))
     55                                     (Tint I8 Unsigned )))
     56                                   (Tint I32 Signed  ))
     57                                 (Expr (Ecast (Tint I32 Signed  )
     58                                   (Expr (Evar (ident_of_nat 3))
     59                                     (Tint I8 Unsigned )))
     60                                   (Tint I32 Signed  ))) (Tint I32 Signed  )))
     61                               (Tint I32 Signed  )))))))))
     62       
     63       
     64       
     65     )〉]
    6466  (ident_of_nat 0)
    65   []
     67 
    6668.
    6769
    68 example exec: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
     70(*
     71example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    6972normalize  (* you can examine the result here *)
    70 @refl
    71 qed.
    72 
    73 include "Clight/SimplifyCasts.ma".
    74 
    75 example simplified: result ? (simplify_program myprog).
    76 normalize
    77 %
    78 qed.
    79 
    80 example exec_s: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [EVint I32 (repr I32 0)]).
    81 normalize  (* you can examine the result here *)
    82 @refl
    83 qed.
    84 
     73*)

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

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

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

    r1157 r1513  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef ((list init_data) × type)
    5   [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
    6   〈ident_of_nat 1 (* main *), CL_Internal (
    7     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  )〉 ]
    8       (Ssequence
    9       (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    10         (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
    11         [])
    12       (Ssequence
    13       (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    14         (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    15       (Ssequence
    16       (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    17               (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    18         (Expr (Ebinop Ole (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    19           (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    20           (Tint I32 Signed  ))
    21         (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    22           (Expr (Ebinop Oadd
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [][〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
     6    〈ident_of_nat 1 (* main *), CL_Internal (
     7      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  )〉 ]
     8        (Ssequence
     9        (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
     10          (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
     11          [])
     12        (Ssequence
     13        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
     14          (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     15        (Ssequence
     16        (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
     17                (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     18          (Expr (Ebinop Ole
    2319            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    24             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    25             (Tint I32 Signed  )))
    26         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    27           (Expr (Ebinop Omul
    28             (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    29             (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
    30             (Tint I32 Signed  )))
    31       )
    32       (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))))))
    33    
    34    
    35    
    36   )〉]
     20            (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
     21            (Tint I32 Signed  ))
     22          (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
     23            (Expr (Ebinop Oadd
     24              (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
     25              (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     26              (Tint I32 Signed  )))
     27          (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
     28            (Expr (Ebinop Omul
     29              (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
     30              (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
     31              (Tint I32 Signed  )))
     32        )
     33        (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
     34                              (Tint I32 Signed  )))))))
     35     
     36     
     37     
     38    )〉]
    3739  (ident_of_nat 1)
    38   []
     40 
    3941.
    4042
    41 example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
     43(*
     44example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    4245normalize  (* you can examine the result here *)
    43 @refl
    44 qed.
     46*)

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

    r1139 r1513  
    55   generate Init_null at the moment. *)
    66
    7 definition myprog := mk_program clight_fundef ((list init_data) × type)
    8   [〈ident_of_nat 0 (* insert *), CL_Internal (
    9      mk_function Tvoid [〈ident_of_nat 2, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ]
     7definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     8  [〈〈ident_of_nat 3 (* l6 *), Any〉,
     9     〈[(Init_int8 (repr I8 69)) ; (Init_space 3) ;
     10        (Init_null Any) ],
     11     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
     12  〈〈ident_of_nat 4 (* l5 *), Any〉,
     13    〈[(Init_int8 (repr I8 36)) ; (Init_space 3) ;
     14       (Init_addrof Any (ident_of_nat 3) 0)],
     15    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
     16  〈〈ident_of_nat 5 (* l4 *), Any〉,
     17    〈[(Init_int8 (repr I8 136)) ; (Init_space 3) ;
     18       (Init_addrof Any (ident_of_nat 4) 0)],
     19    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
     20  〈〈ident_of_nat 6 (* l3 *), Any〉,
     21    〈[(Init_int8 (repr I8 105)) ; (Init_space 3) ;
     22       (Init_addrof Any (ident_of_nat 5) 0)],
     23    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
     24  〈〈ident_of_nat 7 (* l2 *), Any〉,
     25    〈[(Init_int8 (repr I8 234)) ; (Init_space 3) ;
     26       (Init_addrof Any (ident_of_nat 6) 0)],
     27    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
     28  〈〈ident_of_nat 8 (* l1 *), Any〉,
     29    〈[(Init_int8 (repr I8 240)) ; (Init_space 3) ;
     30       (Init_addrof Any (ident_of_nat 7) 0)],
     31    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
     32  〈〈ident_of_nat 9 (* l0 *), Any〉,
     33    〈[(Init_int8 (repr I8 102)) ; (Init_space 3) ;
     34       (Init_addrof Any (ident_of_nat 8) 0)],
     35    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉]
     36  [〈ident_of_nat 10 (* insert *), CL_Internal (
     37     mk_function Tvoid [〈ident_of_nat 12, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 11, (Tint I32 Signed  )〉 ]
    1038       (Ssequence
    1139       (Sifthenelse (Expr (Ebinop Oeq
    1240                      (Expr (Ederef
    13                         (Expr (Evar (ident_of_nat 6))
    14                           (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))
    15                         (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
    16                       (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))
     41                        (Expr (Evar (ident_of_nat 13))
     42                          (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
     43                        (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     44                      (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))
    1745                        (Expr (Ecast (Tpointer Any Tvoid)
    1846                          (Expr (Econst_int I8 (repr ? 0))
    1947                            (Tint I8 Unsigned ))) (Tpointer Any Tvoid)))
    20                         (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
     48                        (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    2149                      (Tint I32 Signed  ))
    22          (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     50         (Sassign (Expr (Evar (ident_of_nat 11)) (Tint I32 Signed  ))
    2351           (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    24          (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     52         (Sassign (Expr (Evar (ident_of_nat 11)) (Tint I32 Signed  ))
    2553           (Expr (Ebinop One
    2654             (Expr (Ebinop Oge
    … …  
    2856                 (Expr (Efield (Expr (Ederef
    2957                                 (Expr (Ederef
    30                                    (Expr (Evar (ident_of_nat 6))
    31                                      (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))
    32                                    (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    33                                  (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
     58                                   (Expr (Evar (ident_of_nat 13))
     59                                     (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
     60                                   (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     61                                 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    3462                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    3563               (Expr (Ecast (Tint I32 Signed  )
    3664                 (Expr (Efield (Expr (Ederef
    37                                  (Expr (Evar (ident_of_nat 2))
    38                                    (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    39                                  (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
     65                                 (Expr (Evar (ident_of_nat 12))
     66                                   (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     67                                 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    4068                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    4169               (Tint I32 Signed  ))
    4270             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    4371             (Tint I32 Signed  ))))
    44        (Sifthenelse (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     72       (Sifthenelse (Expr (Evar (ident_of_nat 11)) (Tint I32 Signed  ))
    4573         (Ssequence
    4674         (Sassign (Expr (Efield (Expr (Ederef
    47                                   (Expr (Evar (ident_of_nat 2))
    48                                     (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    49                                   (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
    50                     (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
     75                                  (Expr (Evar (ident_of_nat 12))
     76                                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     77                                  (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     78                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    5179           (Expr (Ederef
    52              (Expr (Evar (ident_of_nat 6))
    53                (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))
    54              (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
     80             (Expr (Evar (ident_of_nat 13))
     81               (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
     82             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    5583         (Sassign (Expr (Ederef
    56                     (Expr (Evar (ident_of_nat 6))
    57                       (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))
    58                     (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
    59            (Expr (Evar (ident_of_nat 2))
    60              (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))
    61          (Scall (None expr) (Expr (Evar (ident_of_nat 0))
    62                               (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid))
    63            [(Expr (Evar (ident_of_nat 2))
    64               (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))));
     84                    (Expr (Evar (ident_of_nat 13))
     85                      (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
     86                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     87           (Expr (Evar (ident_of_nat 12))
     88             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
     89         (Scall (None expr) (Expr (Evar (ident_of_nat 10))
     90                              (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
     91           [(Expr (Evar (ident_of_nat 12))
     92              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))));
    6593           (Expr (Eaddrof
    6694             (Expr (Efield (Expr (Ederef
    6795                             (Expr (Ederef
    68                                (Expr (Evar (ident_of_nat 6))
    69                                  (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))
    70                                (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    71                              (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
    72                (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    73              (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))])))
     96                               (Expr (Evar (ident_of_nat 13))
     97                                 (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
     98                               (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     99                             (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     100               (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     101             (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))])))
    74102     
    75103     
    76104     
    77105   )〉;
    78   〈ident_of_nat 7 (* sort *), CL_Internal (
    79     mk_function Tvoid [〈ident_of_nat 10, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 8, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ]
    80       (Ssequence
    81       (Sassign (Expr (Evar (ident_of_nat 5))
    82                  (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
     106  〈ident_of_nat 14 (* sort *), CL_Internal (
     107    mk_function Tvoid [〈ident_of_nat 17, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 15, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 2, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ]
     108      (Ssequence
     109      (Sassign (Expr (Evar (ident_of_nat 2))
     110                 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    83111        (Expr (Ederef
    84           (Expr (Evar (ident_of_nat 10))
    85             (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))
    86           (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    87       (Ssequence
    88       (Sassign (Expr (Evar (ident_of_nat 9))
    89                  (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
    90         (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))
     112          (Expr (Evar (ident_of_nat 17))
     113            (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
     114          (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     115      (Ssequence
     116      (Sassign (Expr (Evar (ident_of_nat 16))
     117                 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     118        (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))
    91119          (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    92           (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    93       (Ssequence
    94       (Swhile (Expr (Evar (ident_of_nat 5))
    95                 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
     120          (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     121      (Ssequence
     122      (Swhile (Expr (Evar (ident_of_nat 2))
     123                (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    96124        (Ssequence
    97         (Sassign (Expr (Evar (ident_of_nat 8))
    98                    (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
    99           (Expr (Evar (ident_of_nat 5))
    100             (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
     125        (Sassign (Expr (Evar (ident_of_nat 15))
     126                   (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     127          (Expr (Evar (ident_of_nat 2))
     128            (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    101129        (Ssequence
    102         (Sassign (Expr (Evar (ident_of_nat 5))
    103                    (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
     130        (Sassign (Expr (Evar (ident_of_nat 2))
     131                   (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    104132          (Expr (Efield (Expr (Ederef
    105                           (Expr (Evar (ident_of_nat 5))
    106                             (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    107                           (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
    108             (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    109         (Scall (None expr) (Expr (Evar (ident_of_nat 0))
    110                              (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid))
    111           [(Expr (Evar (ident_of_nat 8))
    112              (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))));
     133                          (Expr (Evar (ident_of_nat 2))
     134                            (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     135                          (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     136            (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     137        (Scall (None expr) (Expr (Evar (ident_of_nat 10))
     138                             (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
     139          [(Expr (Evar (ident_of_nat 15))
     140             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))));
    113141          (Expr (Eaddrof
    114             (Expr (Evar (ident_of_nat 9))
    115               (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    116             (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))]))))
     142            (Expr (Evar (ident_of_nat 16))
     143              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     144            (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))]))))
    117145      (Sassign (Expr (Ederef
    118                  (Expr (Evar (ident_of_nat 10))
    119                    (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))
    120                  (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
    121         (Expr (Evar (ident_of_nat 9))
    122           (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))))))
     146                 (Expr (Evar (ident_of_nat 17))
     147                   (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
     148                 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     149        (Expr (Evar (ident_of_nat 16))
     150          (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))))
    123151   
    124152   
    125153   
    126154  )〉;
    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 Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))〉 ]
    130       (Ssequence
    131       (Sassign (Expr (Evar (ident_of_nat 13))
    132                  (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
     155  〈ident_of_nat 18 (* out *), CL_External (ident_of_nat 18) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;
     156  〈ident_of_nat 19 (* main *), CL_Internal (
     157    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 20, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ]
     158      (Ssequence
     159      (Sassign (Expr (Evar (ident_of_nat 20))
     160                 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    133161        (Expr (Eaddrof
    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 Any (ident_of_nat 3)) Fnil)))))
    136           (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    137       (Ssequence
    138       (Scall (None expr) (Expr (Evar (ident_of_nat 7))
    139                            (Tfunction (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))) Tnil) Tvoid))
     162          (Expr (Evar (ident_of_nat 9))
     163            (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     164          (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     165      (Ssequence
     166      (Scall (None expr) (Expr (Evar (ident_of_nat 14))
     167                           (Tfunction (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil) Tvoid))
    140168        [(Expr (Eaddrof
    141            (Expr (Evar (ident_of_nat 13))
    142              (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    143            (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))])
    144       (Ssequence
    145       (Swhile (Expr (Evar (ident_of_nat 13))
    146                 (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
     169           (Expr (Evar (ident_of_nat 20))
     170             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     171           (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))])
     172      (Ssequence
     173      (Swhile (Expr (Evar (ident_of_nat 20))
     174                (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    147175        (Ssequence
    148         (Scall (None expr) (Expr (Evar (ident_of_nat 11))
     176        (Scall (None expr) (Expr (Evar (ident_of_nat 18))
    149177                             (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) Tvoid))
    150178          [(Expr (Efield (Expr (Ederef
    151                            (Expr (Evar (ident_of_nat 13))
    152                              (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    153                            (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
     179                           (Expr (Evar (ident_of_nat 20))
     180                             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     181                           (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    154182             (Tint I8 Unsigned ))])
    155         (Sassign (Expr (Evar (ident_of_nat 13))
    156                    (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))))
     183        (Sassign (Expr (Evar (ident_of_nat 20))
     184                   (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    157185          (Expr (Efield (Expr (Ederef
    158                           (Expr (Evar (ident_of_nat 13))
    159                             (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))
    160                           (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
    161             (Tpointer Any (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil))))))))
     186                          (Expr (Evar (ident_of_nat 20))
     187                            (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     188                          (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     189            (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))))
    162190      (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
    163191                            (Tint I32 Signed  )))))))
    … …  
    166194   
    167195  )〉]
    168   (ident_of_nat 12)
    169   [〈〈ident_of_nat 15 (* l6 *), Any〉,
    170     〈[(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ],
    171      (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
    172   〈〈ident_of_nat 16 (* l5 *), Any〉,
    173     〈[(Init_int8 (repr I8 36)) ; (Init_space 3) ;
    174     (Init_addrof Any (ident_of_nat 15) 0)],
    175     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
    176   〈〈ident_of_nat 17 (* l4 *), Any〉,
    177     〈[(Init_int8 (repr I8 136)) ; (Init_space 3) ;
    178     (Init_addrof Any (ident_of_nat 16) 0)],
    179     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
    180   〈〈ident_of_nat 18 (* l3 *), Any〉,
    181     〈[(Init_int8 (repr I8 105)) ; (Init_space 3) ;
    182     (Init_addrof Any (ident_of_nat 17) 0)],
    183     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
    184   〈〈ident_of_nat 19 (* l2 *), Any〉,
    185    〈[(Init_int8 (repr I8 234)) ; (Init_space 3) ;
    186     (Init_addrof Any (ident_of_nat 18) 0)],
    187     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
    188   〈〈ident_of_nat 20 (* l1 *), Any〉,
    189    〈[(Init_int8 (repr I8 240)) ; (Init_space 3) ;
    190     (Init_addrof Any (ident_of_nat 19) 0)],
    191     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉;
    192   〈〈ident_of_nat 14 (* l0 *), Any〉,
    193     〈[(Init_int8 (repr I8 102)) ; (Init_space 3) ;
    194     (Init_addrof Any (ident_of_nat 20) 0)],
    195     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr Any (ident_of_nat 3)) Fnil)))〉〉]
     196  (ident_of_nat 19)
     197 
    196198.
    197199
    198 example exec:
    199   (do s ← exec_up_to clight_fullexec myprog 1000
    200      [EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0)];
    201    match s with [ finished t _ _ ⇒ OK ? t | _ ⇒ Error ? [ ] ]) = OK ?
    202 [EVextcall (ident_of_nat 11) [EVint I8 (repr ? 36)] (EVint I32 (repr ? 0));
    203  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 69)] (EVint I32 (repr ? 0));
    204  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 102)] (EVint I32 (repr ? 0));
    205  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 105)] (EVint I32 (repr ? 0));
    206  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 136)] (EVint I32 (repr ? 0));
    207  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 234)] (EVint I32 (repr ? 0));
    208  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 240)] (EVint I32 (repr ? 0))]
    209 .
     200(*
     201example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    210202normalize  (* you can examine the result here *)
    211 @refl
    212 qed.
    213 
    214 include "Clight/label.ma".
    215 
    216 example labelled_exec:
    217   (do p ← clight_label myprog;
    218    do s ← exec_up_to clight_fullexec p 1000
    219      [EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0)];
    220    match s with [ finished t _ _ ⇒ OK ? (remove_costs t) | _ ⇒ Error ? [ ] ]) = OK ?
    221 [EVextcall (ident_of_nat 11) [EVint I8 (repr ? 36)] (EVint I32 (repr ? 0));
    222  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 69)] (EVint I32 (repr ? 0));
    223  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 102)] (EVint I32 (repr ? 0));
    224  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 105)] (EVint I32 (repr ? 0));
    225  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 136)] (EVint I32 (repr ? 0));
    226  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 234)] (EVint I32 (repr ? 0));
    227  EVextcall (ident_of_nat 11) [EVint I8 (repr ? 240)] (EVint I32 (repr ? 0))]
    228 .
    229 normalize  (* you can examine the result here *)
    230 @refl
    231 qed.
     203*)

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

    r965 r1513  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
    5   [〈ident_of_nat 0 (* main *), CL_Internal (
    6      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I8 Unsigned ))〉 ]
    7        (Ssequence
    8        (Sassign (Expr (Evar (ident_of_nat 2))
    9                   (Tpointer Any (Tint I8 Unsigned )))
    10          (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
    11            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    12            (Tpointer Any (Tint I8 Unsigned ))))
    13        (Ssequence
    14        (Sassign (Expr (Evar (ident_of_nat 3))
    15                   (Tpointer Any (Tint I8 Unsigned )))
    16          (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    17            (Tpointer Any (Tint I8 Unsigned ))))
    18        (Ssequence
    19        (Sifthenelse (Expr (Ebinop Oeq
    20                       (Expr (Evar (ident_of_nat 2))
    21                         (Tpointer Any (Tint I8 Unsigned )))
    22                       (Expr (Evar (ident_of_nat 3))
    23                         (Tpointer Any (Tint I8 Unsigned ))))
    24                       (Tint I32 Signed  ))
    25          (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
    26                                (Tint I32 Signed  ))))
    27          Sskip)
    28        (Ssequence
    29        (Sifthenelse (Expr (Ebinop Ogt
    30                       (Expr (Ebinop Osub
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [][〈ident_of_nat 0 (* main *), CL_Internal (
     6       mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I8 Unsigned ))〉 ]
     7         (Ssequence
     8         (Sassign (Expr (Evar (ident_of_nat 2))
     9                    (Tpointer Any (Tint I8 Unsigned )))
     10           (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
     11             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     12             (Tpointer Any (Tint I8 Unsigned ))))
     13         (Ssequence
     14         (Sassign (Expr (Evar (ident_of_nat 3))
     15                    (Tpointer Any (Tint I8 Unsigned )))
     16           (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
     17             (Tpointer Any (Tint I8 Unsigned ))))
     18         (Ssequence
     19         (Sifthenelse (Expr (Ebinop Oeq
    3120                        (Expr (Evar (ident_of_nat 2))
    3221                          (Tpointer Any (Tint I8 Unsigned )))
    33                         (Expr (Evar (ident_of_nat 2))
     22                        (Expr (Evar (ident_of_nat 3))
    3423                          (Tpointer Any (Tint I8 Unsigned ))))
    3524                        (Tint I32 Signed  ))
    36                       (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    37                       (Tint I32 Signed  ))
    38          (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
    39                                (Tint I32 Signed  ))))
    40          Sskip)
    41        (Ssequence
    42        (Sassign (Expr (Evar (ident_of_nat 2))
    43                   (Tpointer Any (Tint I8 Unsigned )))
    44          (Expr (Ebinop Oadd
    45            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
    46            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    47            (Tpointer Any (Tint I8 Unsigned ))))
    48        (Ssequence
    49        (Sassign (Expr (Evar (ident_of_nat 2))
    50                   (Tpointer Any (Tint I8 Unsigned )))
    51          (Expr (Ebinop Oadd
    52            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
    53            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))))
    54            (Tpointer Any (Tint I8 Unsigned ))))
    55        (Ssequence
    56        (Sassign (Expr (Evar (ident_of_nat 2))
    57                   (Tpointer Any (Tint I8 Unsigned )))
    58          (Expr (Ebinop Osub
    59            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
    60            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    61            (Tpointer Any (Tint I8 Unsigned ))))
    62        (Sreturn (Some expr (Expr (Ebinop Oeq
    63                              (Expr (Evar (ident_of_nat 2))
    64                                (Tpointer Any (Tint I8 Unsigned )))
    65                              (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
    66                                (Expr (Ecast (Tpointer Any Tvoid)
    67                                  (Expr (Econst_int I8 (repr ? 0))
    68                                    (Tint I8 Unsigned )))
    69                                  (Tpointer Any Tvoid)))
    70                                (Tpointer Any (Tint I8 Unsigned ))))
    71                              (Tint I32 Signed  )))))))))))
    72      
    73      
    74      
    75    )〉]
     25           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
     26                                 (Tint I32 Signed  ))))
     27           Sskip)
     28         (Ssequence
     29         (Sifthenelse (Expr (Ebinop Ogt
     30                        (Expr (Ebinop Osub
     31                          (Expr (Evar (ident_of_nat 2))
     32                            (Tpointer Any (Tint I8 Unsigned )))
     33                          (Expr (Evar (ident_of_nat 2))
     34                            (Tpointer Any (Tint I8 Unsigned ))))
     35                          (Tint I32 Signed  ))
     36                        (Expr (Econst_int I32 (repr ? 0))
     37                          (Tint I32 Signed  ))) (Tint I32 Signed  ))
     38           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
     39                                 (Tint I32 Signed  ))))
     40           Sskip)
     41         (Ssequence
     42         (Sassign (Expr (Evar (ident_of_nat 2))
     43                    (Tpointer Any (Tint I8 Unsigned )))
     44           (Expr (Ebinop Oadd
     45             (Expr (Evar (ident_of_nat 2))
     46               (Tpointer Any (Tint I8 Unsigned )))
     47             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     48             (Tpointer Any (Tint I8 Unsigned ))))
     49         (Ssequence
     50         (Sassign (Expr (Evar (ident_of_nat 2))
     51                    (Tpointer Any (Tint I8 Unsigned )))
     52           (Expr (Ebinop Oadd
     53             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
     54             (Expr (Evar (ident_of_nat 2))
     55               (Tpointer Any (Tint I8 Unsigned ))))
     56             (Tpointer Any (Tint I8 Unsigned ))))
     57         (Ssequence
     58         (Sassign (Expr (Evar (ident_of_nat 2))
     59                    (Tpointer Any (Tint I8 Unsigned )))
     60           (Expr (Ebinop Osub
     61             (Expr (Evar (ident_of_nat 2))
     62               (Tpointer Any (Tint I8 Unsigned )))
     63             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     64             (Tpointer Any (Tint I8 Unsigned ))))
     65         (Sreturn (Some expr (Expr (Ebinop Oeq
     66                               (Expr (Evar (ident_of_nat 2))
     67                                 (Tpointer Any (Tint I8 Unsigned )))
     68                               (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
     69                                 (Expr (Ecast (Tpointer Any Tvoid)
     70                                   (Expr (Econst_int I8 (repr ? 0))
     71                                     (Tint I8 Unsigned )))
     72                                   (Tpointer Any Tvoid)))
     73                                 (Tpointer Any (Tint I8 Unsigned ))))
     74                               (Tint I32 Signed  )))))))))))
     75       
     76       
     77       
     78     )〉]
    7679  (ident_of_nat 0)
    77   []
     80 
    7881.
    7982
    80 example exec: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 50 [ ]).
     83(*
     84example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    8185normalize  (* you can examine the result here *)
    82 @refl
    83 qed.
     86*)

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

    r978 r1513  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
    5   [〈ident_of_nat 0 (* get *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
    6   〈ident_of_nat 1 (* main *), CL_Internal (
    7     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ]
    8       (Ssequence
    9       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    10         (Expr (Ecast (Tint I8 Unsigned )
    11           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    12           (Tint I8 Unsigned )))
    13       (Ssequence
    14       (Ssequence
    15       (Scall (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
    16         (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
    17         [])
    18       (Sswitch (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )) (
    19         (LScase I32 (repr ? 1)
    20           Sbreak
    21           (LScase I32 (repr ? 3)
    22             (Ssequence
    23             (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    24               (Expr (Ecast (Tint I8 Unsigned )
    25                 (Expr (Ebinop Oadd
    26                   (Expr (Ecast (Tint I32 Signed  )
    27                     (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    28                     (Tint I32 Signed  ))
    29                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    30                   (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    31             Sbreak)
    32             (LScase I32 (repr ? 5)
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [][〈ident_of_nat 0 (* get *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
     6    〈ident_of_nat 1 (* main *), CL_Internal (
     7      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ]
     8        (Ssequence
     9        (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     10          (Expr (Ecast (Tint I8 Unsigned )
     11            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     12            (Tint I8 Unsigned )))
     13        (Ssequence
     14        (Ssequence
     15        (Scall (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
     16          (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
     17          [])
     18        (Sswitch (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )) (
     19          (LScase I32 (repr ? 1)
     20            Sbreak
     21            (LScase I32 (repr ? 3)
     22              (Ssequence
    3323              (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    3424                (Expr (Ecast (Tint I8 Unsigned )
    … …  
    3727                      (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    3828                      (Tint I32 Signed  ))
    39                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     29                    (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    4030                    (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    41               (LScase I32 (repr ? 7)
    42                 (Ssequence
     31              Sbreak)
     32              (LScase I32 (repr ? 5)
    4333                (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    4434                  (Expr (Ecast (Tint I8 Unsigned )
    … …  
    4737                        (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    4838                        (Tint I32 Signed  ))
    49                       (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
     39                      (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    5040                      (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    51                 Sbreak)
    52                 (LSdefault
     41                (LScase I32 (repr ? 7)
     42                  (Ssequence
    5343                  (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    5444                    (Expr (Ecast (Tint I8 Unsigned )
    … …  
    5747                          (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    5848                          (Tint I32 Signed  ))
    59                         (Expr (Econst_int I32 (repr ? 16))
     49                        (Expr (Econst_int I32 (repr ? 3))
    6050                          (Tint I32 Signed  ))) (Tint I32 Signed  )))
    61                       (Tint I8 Unsigned ))))))))
    62       )))
    63       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
     51                      (Tint I8 Unsigned )))
     52                  Sbreak)
     53                  (LSdefault
     54                    (Sassign (Expr (Evar (ident_of_nat 2))
     55                               (Tint I8 Unsigned ))
     56                      (Expr (Ecast (Tint I8 Unsigned )
     57                        (Expr (Ebinop Oadd
     58                          (Expr (Ecast (Tint I32 Signed  )
    6459                            (Expr (Evar (ident_of_nat 2))
    65                               (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
    66    
    67    
    68    
    69   )〉]
     60                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
     61                          (Expr (Econst_int I32 (repr ? 16))
     62                            (Tint I32 Signed  ))) (Tint I32 Signed  )))
     63                        (Tint I8 Unsigned ))))))))
     64        )))
     65        (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
     66                              (Expr (Evar (ident_of_nat 2))
     67                                (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
     68     
     69     
     70     
     71    )〉]
    7072  (ident_of_nat 1)
    71   []
     73 
    7274.
    7375
    74 example exec0: finishes_with (repr I32 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 0)]).
     76(*
     77example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    7578normalize  (* you can examine the result here *)
    76 @refl qed.
    77 
    78 example exec1: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 1)]).
    79 normalize  (* you can examine the result here *)
    80 @refl qed.
    81 
    82 example exec3: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 3)]).
    83 normalize  (* you can examine the result here *)
    84 @refl qed.
    85 
    86 example exec5: finishes_with (repr I32 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
    87 normalize  (* you can examine the result here *)
    88 @refl qed.
    89 
    90 example exec7: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 7)]).
    91 normalize  (* you can examine the result here *)
    92 @refl qed.
     79*)
Note: See TracChangeset for help on using the changeset viewer.