Changeset 2597 for src/Clight


Ignore:
Timestamp:
Jan 31, 2013, 12:07:02 PM (8 years ago)
Author:
campbell
Message:

Some work in progress on measurable subtrace preservation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2591 r2597  
    338338  ).
    339339
     340axiom clight_cminor_init : ∀cl_program,cm_program,s,s'.
     341  clight_to_cminor cl_program = OK ? cm_program →
     342  make_initial_state ?? clight_fullexec cl_program = OK ? s →
     343  make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
     344  ∃INV. clight_cminor_rel INV s s'.
Note: See TracChangeset for help on using the changeset viewer.