Changeset 1198 for src/Clight/test


Ignore:
Timestamp:
Sep 8, 2011, 4:04:07 PM (8 years ago)
Author:
campbell
Message:

Clight cast removal (NB: quite different from the prototype).

Location:
src/Clight/test
Files:
2 added
1 edited

Legend:

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

    r1139 r1198  
    6060qed.
    6161
     62include "Clight/SimplifyCasts.ma".
     63
     64example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
     65normalize  (* you can examine the result here *)
     66@refl
     67qed.
     68
    6269include "Clight/toCminor.ma".
    6370include "Cminor/semantics.ma".
    6471
    65 example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     72example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor (simplify_program myprog); exec_up_to Cminor_fullexec p 1000 [ ]).
    6673normalize
    6774@refl
     
    7279
    7380example e2: finishes_with (repr I32 74) ? (
    74 do p1 ← clight_to_cminor myprog;
     81do p1 ← clight_to_cminor (simplify_program myprog);
    7582do p2 ← cminor_to_rtlabs p1;
    7683 exec_up_to RTLabs_fullexec p2 1000 [ ]).
Note: See TracChangeset for help on using the changeset viewer.