Changeset 1224 for src/Cminor


Ignore:
Timestamp:
Sep 16, 2011, 6:39:05 PM (9 years ago)
Author:
sacerdot
Message:

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

Location:
src/Cminor
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r1139 r1224  
    7272λp.
    7373  mk_program ??
     74    (empty_vars (prog_vars ?? p))
    7475    (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
    75     (prog_main ?? p)
    76     (empty_vars (prog_vars ?? p)).
    77    
     76    (prog_main ?? p).
  • src/Cminor/syntax.ma

    r1147 r1224  
    4545   responsible for initialisation and we only give the size of each variable. *)
    4646
    47 definition Cminor_program ≝ program (fundef internal_function) (list init_data).
     47definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data).
    4848
    49 definition Cminor_noinit_program ≝ program (fundef internal_function) nat.
     49definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat.
  • src/Cminor/toRTLabs.ma

    r1139 r1224  
    296296
    297297definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
    298 transform_partial_program ???
    299   (transf_partial_fundef ?? c2ra_function).
     298λp.transform_partial_program … p (transf_partial_fundef … c2ra_function).
    300299
    301300include "Cminor/initialisation.ma".
Note: See TracChangeset for help on using the changeset viewer.