Changeset 2972


Ignore:
Timestamp:
Mar 27, 2013, 11:42:03 AM (4 years ago)
Author:
campbell
Message:

Remove init from a testcase.

File:
1 edited

Legend:

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

    r2645 r2972  
    3030let 〈p0,init〉 ≝ clight_label myprog in
    3131bind ? (snapshot state) (clight_to_cminor (simplify_program p0))
    32 (λp1. let p2 ≝ cminor_to_rtlabs init p1 in
     32(λp1. let p2 ≝ cminor_to_rtlabs p1 in
    3333  exec_up_to RTLabs_fullexec p2 1000 [ ])).
    3434normalize
     
    6060  let 〈p0,init〉 ≝ clight_label myprog in
    6161  ! p1 ← clight_to_cminor (simplify_program p0);
    62   let p2 ≝ cminor_to_rtlabs init p1 in
     62  let p2 ≝ cminor_to_rtlabs p1 in
    6363  return (check_cost_program p2)) = OK bool true.
    6464normalize
Note: See TracChangeset for help on using the changeset viewer.