Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (6 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/insertsort.c.ma

    r1513 r2176  
    66
    77definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
    8   [〈〈ident_of_nat 3 (* l6 *), Any〉,
     8  [〈〈ident_of_nat 3 (* l6 *), XData〉,
    99     〈[(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〉,
     10        (Init_null) ],
     11     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     12  〈〈ident_of_nat 4 (* l5 *), XData〉,
    1313    〈[(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〉,
     14       (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉;
     16  〈〈ident_of_nat 5 (* l4 *), XData〉,
    1717    〈[(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〉,
     18       (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉;
     20  〈〈ident_of_nat 6 (* l3 *), XData〉,
    2121    〈[(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〉,
     22       (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉;
     24  〈〈ident_of_nat 7 (* l2 *), XData〉,
    2525    〈[(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〉,
     26       (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉;
     28  〈〈ident_of_nat 8 (* l1 *), XData〉,
    2929    〈[(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〉,
     30       (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉;
     32  〈〈ident_of_nat 9 (* l0 *), XData〉,
    3333    〈[(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)))〉〉]
     34       (Init_addrof (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 (ident_of_nat 0)) Fnil)))〉〉]
    3636  [〈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  )〉 ]
     37     mk_function Tvoid [〈ident_of_nat 12, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 13, (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 11, (Tint I32 Signed  )〉 ]
    3838       (Ssequence
    3939       (Sifthenelse (Expr (Ebinop Oeq
    4040                      (Expr (Ederef
    4141                        (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))))
    45                         (Expr (Ecast (Tpointer Any Tvoid)
     42                          (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     43                        (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
     44                      (Expr (Ecast (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))
     45                        (Expr (Ecast (Tpointer Tvoid)
    4646                          (Expr (Econst_int I8 (repr ? 0))
    47                             (Tint I8 Unsigned ))) (Tpointer Any Tvoid)))
    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))))))
     47                            (Tint I8 Unsigned ))) (Tpointer Tvoid)))
     48                        (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    4949                      (Tint I32 Signed  ))
    5050         (Sassign (Expr (Evar (ident_of_nat 11)) (Tint I32 Signed  ))
     
    5757                                 (Expr (Ederef
    5858                                   (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))
     59                                     (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     60                                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    6262                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    6363               (Expr (Ecast (Tint I32 Signed  )
    6464                 (Expr (Efield (Expr (Ederef
    6565                                 (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))
     66                                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    6868                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    6969               (Tint I32 Signed  ))
     
    7474         (Sassign (Expr (Efield (Expr (Ederef
    7575                                  (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)))))
     76                                    (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     78                    (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    7979           (Expr (Ederef
    8080             (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))))))
     81               (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     82             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    8383         (Sassign (Expr (Ederef
    8484                    (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)))))
     85                      (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     86                    (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    8787           (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)))))))
     88             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
    8989         (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))
     90                              (Tfunction (Tcons (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
    9191           [(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)))));
     92              (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))));
    9393           (Expr (Eaddrof
    9494             (Expr (Efield (Expr (Ederef
    9595                             (Expr (Ederef
    9696                               (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))))))])))
     97                                 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     98                               (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     100               (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     101             (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))])))
    102102     
    103103     
     
    105105   )〉;
    106106  〈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))))〉 ]
     107    mk_function Tvoid [〈ident_of_nat 17, (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 15, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 2, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 16, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ]
    108108      (Ssequence
    109109      (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)))))
     110                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    111111        (Expr (Ederef
    112112          (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))))))
     113            (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     114          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    115115      (Ssequence
    116116      (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))))
     117                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
     118        (Expr (Ecast (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))
    119119          (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    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))))))
     120          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    121121      (Ssequence
    122122      (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)))))
     123                (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    124124        (Ssequence
    125125        (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)))))
     126                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    127127          (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))))))
     128            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    129129        (Ssequence
    130130        (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)))))
     131                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    132132          (Expr (Efield (Expr (Ederef
    133133                          (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))))))
     134                            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     136            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    137137        (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))
     138                             (Tfunction (Tcons (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
    139139          [(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)))));
     140             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))));
    141141          (Expr (Eaddrof
    142142            (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))))))]))))
     143              (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     144            (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))]))))
    145145      (Sassign (Expr (Ederef
    146146                 (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)))))
     147                   (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     148                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    149149        (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)))))))))
     150          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))))
    151151   
    152152   
     
    155155  〈ident_of_nat 18 (* out *), CL_External (ident_of_nat 18) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;
    156156  〈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))))〉 ]
     157    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 20, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ]
    158158      (Ssequence
    159159      (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)))))
     160                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    161161        (Expr (Eaddrof
    162162          (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))))))
     163            (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
     164          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    165165      (Ssequence
    166166      (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))
     167                           (Tfunction (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil) Tvoid))
    168168        [(Expr (Eaddrof
    169169           (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))))))])
     170             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     171           (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))])
    172172      (Ssequence
    173173      (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)))))
     174                (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    175175        (Ssequence
    176176        (Scall (None expr) (Expr (Evar (ident_of_nat 18))
     
    178178          [(Expr (Efield (Expr (Ederef
    179179                           (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))
     180                             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    182182             (Tint I8 Unsigned ))])
    183183        (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)))))
     184                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    185185          (Expr (Efield (Expr (Ederef
    186186                          (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))))))))
     187                            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (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 (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     189            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))))
    190190      (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
    191191                            (Tint I32 Signed  )))))))
Note: See TracChangeset for help on using the changeset viewer.