Changeset 2468 for src/common/Events.ma


Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (7 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Events.ma

    r1599 r2468  
    3838
    3939inductive eventval: Type[0] ≝
    40   | EVint: ∀sz. bvint sz → eventval
    41   | EVfloat: float → eventval.
     40  | EVint: ∀sz. bvint sz → eventval.
     41(*  | EVfloat: float → eventval.*)
    4242
    4343inductive event : Type[0] ≝
     
    194194  | ev_match_int:
    195195      ∀sz,sg,i. eventval_match (EVint sz i) (ASTint sz sg) (Vint sz i)
    196   | ev_match_float:
    197       ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f).
     196(*  | ev_match_float:
     197      ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f) *).
    198198
    199199inductive eventval_list_match: list eventval -> list typ -> list val -> Prop :=
Note: See TracChangeset for help on using the changeset viewer.