Changeset 881 for src/Clight/test/sum.ma


Ignore:
Timestamp:
Jun 3, 2011, 5:35:31 PM (10 years ago)
Author:
campbell
Message:

Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/sum.ma

    r758 r881  
    6060@refl
    6161qed.
     62
     63include "Clight/toCminor.ma".
     64include "Cminor/semantics.ma".
     65
     66example e1: finishes_with (repr 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     67normalize
     68@refl
     69qed.
     70
     71include "Cminor/toRTLabs.ma".
     72include "RTLabs/semantics.ma".
     73
     74example e2: finishes_with (repr 74) ? (
     75do p1 ← clight_to_cminor myprog;
     76do p2 ← cminor_to_rtlabs p1;
     77 exec_up_to RTLabs_fullexec p2 1000 [ ]).
     78normalize
     79@refl
     80qed.
Note: See TracChangeset for help on using the changeset viewer.