Changeset 2471 for src/Clight


Ignore:
Timestamp:
Nov 16, 2012, 6:41:49 PM (8 years ago)
Author:
campbell
Message:

Tame global environments a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2466 r2471  
    247247| %
    248248] qed.
     249
     250include "Clight/Cexec.ma".
     251include "Cminor/semantics.ma".
     252
     253record clight_cminor_inv : Type[0] ≝ {
     254  globals : list (ident × region × type);
     255  ge_cl : genv_t clight_fundef;
     256  ge_cm : genv_t (fundef internal_function);
     257  eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s;
     258  trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f →
     259    ∃tmp_u,f',H1,H2.
     260      translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧
     261      find_funct … ge_cm v = Some ? f'
     262}.
Note: See TracChangeset for help on using the changeset viewer.