Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (8 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/Clight/test/insertsort.c.ma

    r965 r1153  
    55   generate Init_null at the moment. *)
    66
    7 definition myprog := mk_program clight_fundef type
     7definition myprog := mk_program clight_fundef ((list init_data) × type)
    88  [〈ident_of_nat 0 (* insert *), CL_Internal (
    99     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  )〉 ]
     
    167167  )〉]
    168168  (ident_of_nat 12)
    169   [〈〈〈ident_of_nat 15 (* l6 *),
    170      [(Init_int8 (repr I8 69)) ; (Init_space 3) ; (Init_null Any) ]〉,
    171      Any〉,
    172      (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)))〉;
    173   〈〈〈ident_of_nat 16 (* l5 *),
    174     [(Init_int8 (repr I8 36)) ; (Init_space 3) ;
    175     (Init_addrof Any (ident_of_nat 15) 0)]〉, Any〉,
    176     (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)))〉;
    177   〈〈〈ident_of_nat 17 (* l4 *),
    178     [(Init_int8 (repr I8 136)) ; (Init_space 3) ;
    179     (Init_addrof Any (ident_of_nat 16) 0)]〉, Any〉,
    180     (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)))〉;
    181   〈〈〈ident_of_nat 18 (* l3 *),
    182     [(Init_int8 (repr I8 105)) ; (Init_space 3) ;
    183     (Init_addrof Any (ident_of_nat 17) 0)]〉, Any〉,
    184     (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)))〉;
    185   〈〈〈ident_of_nat 19 (* l2 *),
    186     [(Init_int8 (repr I8 234)) ; (Init_space 3) ;
    187     (Init_addrof Any (ident_of_nat 18) 0)]〉, Any〉,
    188     (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)))〉;
    189   〈〈〈ident_of_nat 20 (* l1 *),
    190     [(Init_int8 (repr I8 240)) ; (Init_space 3) ;
    191     (Init_addrof Any (ident_of_nat 19) 0)]〉, Any〉,
    192     (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)))〉;
    193   〈〈〈ident_of_nat 14 (* l0 *),
    194     [(Init_int8 (repr I8 102)) ; (Init_space 3) ;
    195     (Init_addrof Any (ident_of_nat 20) 0)]〉, Any〉,
    196     (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  [〈〈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)))〉〉]
    197196.
    198197
Note: See TracChangeset for help on using the changeset viewer.