Ignore:
Timestamp:
Jul 24, 2012, 7:40:22 PM (9 years ago)
Author:
campbell
Message:

Cminor to RTLabs is now a total function.

File:
1 edited

Legend:

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

    r1876 r2253  
    2828example e2: finishes_with (repr I32 74) ? (
    2929bind ? (snapshot state) (clight_to_cminor (simplify_program myprog))
    30 (λp1. bind ? (snapshot state) (cminor_to_rtlabs p1)
    31  (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))).
     30(λp1. let p2 ≝ cminor_to_rtlabs p1 in
     31  exec_up_to RTLabs_fullexec p2 1000 [ ])).
    3232normalize
    3333%
Note: See TracChangeset for help on using the changeset viewer.