Changeset 1139 for src/common/AST.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/common/AST.ma

    r1064 r1139  
    282282  prog_funct: list (ident × F);
    283283  prog_main: ident;
    284   prog_vars: list (ident × (list init_data) × region × V)
     284  prog_vars: list (ident × region × V)
    285285}.
    286286
     
    290290
    291291definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
    292   map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
     292  map ?? (λx: ident × region × V. (\fst (\fst x))) (prog_vars ?? p).
    293293
    294294(* * * Generic transformations over programs *)
Note: See TracChangeset for help on using the changeset viewer.