Changeset 2468 for src/Clight/Cexec.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/Clight/Cexec.ma

    r2428 r2468  
    1919    | _ ⇒ Error ? (msg TypeMismatch)
    2020    ]
    21   | Vfloat f ⇒ match ty with
     21(*  | Vfloat f ⇒ match ty with
    2222    [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero)
    2323    | _ ⇒ Error ? (msg TypeMismatch)
    24     ]
     24    ]*)
    2525  | Vptr _ ⇒ match ty with
    2626    [ Tpointer _ ⇒ OK ? true
     
    3838  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
    3939  | #ptr #ty %{ true} % //
    40   | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
     40(*  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //; *)
    4141  | * #sg %{ false} % //
    4242  | #t %{ false} % //;
    43   | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;
     43(*  | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;*)
    4444  ]
    4545qed.
     
    110110      match ty' with
    111111      [ Tint sz2 si2 ⇒ OK ? (Vint ? (cast_int_int sz1 si1 sz2 i))
    112       | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
     112(*      | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))*)
    113113      | Tpointer _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
    114114      | Tarray _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
     
    122122  | _ ⇒ Error ? (msg TypeMismatch)
    123123  ]
    124 | Vfloat f ⇒
     124(*| Vfloat f ⇒
    125125  match ty with
    126126  [ Tfloat sz ⇒
     
    131131    ]
    132132  | _ ⇒ Error ? (msg TypeMismatch)
    133   ]
     133  ]*)
    134134| Vptr ptr ⇒
    135135(*    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
     
    179179      | _ ⇒ Error ? (msg BadlyTypedTerm)
    180180      ]
    181   | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉
     181(*  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉 *)
    182182  | Evar _ ⇒
    183183      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
Note: See TracChangeset for help on using the changeset viewer.