Changeset 2253 for src/Clight/test


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

Cminor to RTLabs is now a total function.

Location:
src/Clight/test
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/goto-if.test.ma

    r1914 r2253  
    3737example e2: finishes_with (repr I32 0) ? (
    3838bind ? (snapshot state) (clight_to_cminor (simplify_program myprog'))
    39 (λp1. bind ? (snapshot state) (cminor_to_rtlabs p1)
    40  (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))).
     39(λp1. let p2 ≝ cminor_to_rtlabs p1 in
     40  exec_up_to RTLabs_fullexec p2 1000 [ ])).
    4141normalize
    4242%
  • 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.