Changeset 1238 for src/Clight


Ignore:
Timestamp:
Sep 21, 2011, 4:25:36 PM (9 years ago)
Author:
campbell
Message:

Update Cminor and RTLabs to fit SmallstepExec? changes.

File:
1 edited

Legend:

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

    r1224 r1238  
    192192include "Cminor/semantics.ma".
    193193
     194example e1: finishes_with (repr I32 3) ? (bind ? (snapshot state) (clight_to_cminor myprog) (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
     195(*
    194196example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     197*)
    195198normalize
    196199@refl
     
    202205example e2: finishes_with (repr 3) ? (
    203206do p1 ← clight_to_cminor myprog;
     207bind ? (snapshot state) (cminor_to_rtlabs p1) (λp2.
     208 exec_up_to RTLabs_fullexec p2 1000 [ ])).
     209(*
     210example e2: finishes_with (repr 3) ? (
     211do p1 ← clight_to_cminor myprog;
    204212do p2 ← cminor_to_rtlabs p1;
    205  exec_up_to RTLabs_fullexec p2 1000 [ ]).
     213 exec_up_to RTLabs_fullexec p2 1000 [ ]).*)
    206214normalize
    207215@refl
Note: See TracChangeset for help on using the changeset viewer.