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/sum.c.ma

    r965 r1139  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
     4definition myprog := mk_program clight_fundef (list init_data × type)
    55  [〈ident_of_nat 0 (* main *), CL_Internal (
    66     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ]
     
    4848   )〉]
    4949  (ident_of_nat 0)
    50   [〈〈〈ident_of_nat 3 (* src *),
    51      [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
     50  [〈〈ident_of_nat 3 (* src *), Any〉,
     51     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
    5252     (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
    53      (Init_int8 (repr I8 4)) ]〉, Any〉,
    54      (Tarray Any (Tint I8 Unsigned ) 5)〉]
     53     (Init_int8 (repr I8 4)) ],
     54     (Tarray Any (Tint I8 Unsigned ) 5)〉]
    5555.
    5656
Note: See TracChangeset for help on using the changeset viewer.