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

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File:
1 edited

Legend:

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

    r965 r1139  
    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.