Ignore:
Timestamp:
Apr 4, 2012, 6:48:26 PM (8 years ago)
Author:
campbell
Message:

Update Cexec soundness proof.
Change finishes_with predicate to inductive form so that qed no longer
spends huge amounts of time typechecking.

File:
1 edited

Legend:

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

    r1618 r1876  
    186186example exec: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
    187187normalize  (* you can examine the result here *)
    188 @refl
     188%
    189189qed.
    190190
     
    197197*)
    198198normalize
    199 @refl
     199%
    200200qed.
    201201
     
    213213 exec_up_to RTLabs_fullexec p2 1000 [ ]).*)
    214214normalize
    215 @refl
     215%
    216216qed.
    217217(*
Note: See TracChangeset for help on using the changeset viewer.