Ignore:
Timestamp:
Aug 30, 2011, 12:47:18 PM (9 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/toCminor.ma

    r1078 r1139  
    779779λp.
    780780  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
    781   let var_globals ≝ map … (λv. 〈\fst (\fst (\fst v)), \snd (\fst v)〉) (prog_vars ?? p) in
     781  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
    782782  let globals ≝ fun_globals @ var_globals in
    783   transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p.
     783  transform_partial_program2 ???? (translate_fundef globals) (λi. OK ? (\fst i)) p.
Note: See TracChangeset for help on using the changeset viewer.