Changeset 1139 for src/RTLabs


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.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1123 r1139  
    209209definition make_initial_state : RTLabs_program → res (genv × state) ≝
    210210λp.
    211   do ge ← globalenv Genv ?? p;
    212   do m ← init_mem Genv ?? p;
     211  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     212  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    213213  let main ≝ prog_main ?? p in
    214214  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
  • src/RTLabs/syntax.ma

    r1116 r1139  
    4040
    4141(* Note that the global variables will be initialised by the code in main
    42    by this stage.  All initialisation data should only reserve space. *)
     42   by this stage, so the only initialisation data is the amount of space to
     43   allocate. *)
    4344
    44 definition RTLabs_program ≝ program (fundef internal_function) unit.
     45definition RTLabs_program ≝ program (fundef internal_function) nat.
    4546
    4647(* TO CONSIDER:
Note: See TracChangeset for help on using the changeset viewer.