Changeset 2385


Ignore:
Timestamp:
Oct 3, 2012, 11:33:45 AM (8 years ago)
Author:
campbell
Message:

Minor housekeeping.

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/memoryInjections.ma

    r2332 r2385  
    11include "Clight/Cexec.ma".
    2 include "frontend_misc.ma".
     2include "Clight/frontend_misc.ma".
    33
    44(* This file contains some definitions and lemmas related to memory injections.
  • src/Clight/test/insertsort.test.ma

    r1515 r2385  
    2626
    2727example labelled_exec:
    28   (let p ≝ clight_label myprog in
     28  (let 〈p,init〉 ≝ clight_label myprog in
    2929   do s ← exec_up_to clight_fullexec p 1000
    3030     [EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0);EVint I32 (repr ? 0)];
  • src/Clight/test/search.test.ma

    r2106 r2385  
    2222
    2323example e2: finishes_with (repr 3) ? (
    24 do p1 ← clight_to_cminor myprog;
    25 bind ? (snapshot state) (cminor_to_rtlabs p1) (λp2.
     24let 〈p0,init〉 ≝ clight_label myprog in
     25bind ? (snapshot state) (clight_to_cminor p0) (λp1.
     26let p2 ≝ cminor_to_rtlabs init p1 in
    2627 exec_up_to RTLabs_fullexec p2 1000 [ ])).
    2728(*
Note: See TracChangeset for help on using the changeset viewer.