Changeset 2925


Ignore:
Timestamp:
Mar 21, 2013, 3:39:16 PM (4 years ago)
Author:
tranquil
Message:

corrected bug in toggle_bool

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2918 r2925  
    743743  match destrs with
    744744  [ nil ⇒ [ ]
    745   | cons destr _ ⇒ [destr ← .Cmpl. destr]
     745  | cons destr _ ⇒ [destr ← destr .Xor. byte_of_nat 1]
    746746  ].
    747747 
     
    10931093(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
    10941094  because of CompCert heritage *)
    1095 definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
    1096  λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
     1095definition rtlabs_to_rtl: RTLabs_program → costlabel → rtl_program ≝
     1096 λp,init_cost.
     1097  mk_joint_program RTL
     1098    (transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)))
     1099    init_cost.
Note: See TracChangeset for help on using the changeset viewer.