Changeset 2107 for src/Clight


Ignore:
Timestamp:
Jun 22, 2012, 2:07:38 PM (8 years ago)
Author:
campbell
Message:

Memory initialisation and program transformations.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2105 r2107  
    10651065] qed.
    10661066
    1067 (* FIXME: to globalenvs and prove *)
    1068 axiom transform_program_init_mem : ∀A,B,V,p,f,init.
    1069   init_mem ?? init p = init_mem ?? init (transform_program A B V p f).
    1070 
    10711067
    10721068lemma initial_state_in_simulation : ∀p,s.
     
    10861082[ whd in ⊢ (??%?);
    10871083  change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?);
    1088   <transform_program_init_mem >Em in ⊢ (??%?);
     1084  >init_mem_transf >Em in ⊢ (??%?);
    10891085  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
    10901086  whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain')
Note: See TracChangeset for help on using the changeset viewer.