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

Fix up Clight examples.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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*)
Note: See TracChangeset for help on using the changeset viewer.