Changeset 1139 for src/Clight/Cexec.ma


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/Cexec.ma

    r1058 r1139  
    534534
    535535let rec make_initial_state (p:clight_program) : res (genv × state) ≝
    536   do ge ← globalenv Genv ?? p;
    537   do m0 ← init_mem Genv ?? p;
     536  do ge ← globalenv Genv ?? (fst ??) p;
     537  do m0 ← init_mem Genv ?? (fst ??) p;
    538538  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    539539  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
Note: See TracChangeset for help on using the changeset viewer.