Changeset 881 for src/Clight/test/io.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/io.ma

    r797 r881  
    2828@refl
    2929qed.
     30
     31
     32include "Clight/toCminor.ma".
     33include "Cminor/semantics.ma".
     34
     35example e1: (do p ← clight_to_cminor myprog;
     36             do r ← exec_up_to Cminor_fullexec p 1000 [EVint (repr 7) ];
     37             match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) =
     38 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
     39normalize
     40@refl
     41qed.
     42
     43include "Cminor/toRTLabs.ma".
     44include "RTLabs/semantics.ma".
     45
     46example e2: (do p1 ← clight_to_cminor myprog;
     47             do p2 ← cminor_to_rtlabs p1;
     48             do r ← exec_up_to RTLabs_fullexec p2 1000 [EVint (repr 7) ];
     49             match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) =
     50 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
     51normalize
     52@refl
     53qed.
Note: See TracChangeset for help on using the changeset viewer.