Changeset 3006


Ignore:
Timestamp:
Mar 28, 2013, 1:50:59 PM (4 years ago)
Author:
sacerdot
Message:

New extraction, bugs fixed.

Location:
extracted
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabsToRTL.ml

    r3001 r3006  
    146146| AST.ASTptr -> Nat.S (Nat.S Nat.O)
    147147
     148(** val sign_of_sig_type : AST.typ -> AST.signedness **)
     149let sign_of_sig_type = function
     150| AST.ASTint (x, sign) -> sign
     151| AST.ASTptr -> AST.Unsigned
     152
    148153type register_type =
    149154| Register_int of Registers.register
     
    154159    -> 'a1) -> register_type -> 'a1 **)
    155160let rec register_type_rect_Type4 h_register_int h_register_ptr = function
    156 | Register_int x_7284 -> h_register_int x_7284
    157 | Register_ptr (x_7286, x_7285) -> h_register_ptr x_7286 x_7285
     161| Register_int x_8 -> h_register_int x_8
     162| Register_ptr (x_10, x_9) -> h_register_ptr x_10 x_9
    158163
    159164(** val register_type_rect_Type5 :
     
    161166    -> 'a1) -> register_type -> 'a1 **)
    162167let rec register_type_rect_Type5 h_register_int h_register_ptr = function
    163 | Register_int x_7290 -> h_register_int x_7290
    164 | Register_ptr (x_7292, x_7291) -> h_register_ptr x_7292 x_7291
     168| Register_int x_14 -> h_register_int x_14
     169| Register_ptr (x_16, x_15) -> h_register_ptr x_16 x_15
    165170
    166171(** val register_type_rect_Type3 :
     
    168173    -> 'a1) -> register_type -> 'a1 **)
    169174let rec register_type_rect_Type3 h_register_int h_register_ptr = function
    170 | Register_int x_7296 -> h_register_int x_7296
    171 | Register_ptr (x_7298, x_7297) -> h_register_ptr x_7298 x_7297
     175| Register_int x_20 -> h_register_int x_20
     176| Register_ptr (x_22, x_21) -> h_register_ptr x_22 x_21
    172177
    173178(** val register_type_rect_Type2 :
     
    175180    -> 'a1) -> register_type -> 'a1 **)
    176181let rec register_type_rect_Type2 h_register_int h_register_ptr = function
    177 | Register_int x_7302 -> h_register_int x_7302
    178 | Register_ptr (x_7304, x_7303) -> h_register_ptr x_7304 x_7303
     182| Register_int x_26 -> h_register_int x_26
     183| Register_ptr (x_28, x_27) -> h_register_ptr x_28 x_27
    179184
    180185(** val register_type_rect_Type1 :
     
    182187    -> 'a1) -> register_type -> 'a1 **)
    183188let rec register_type_rect_Type1 h_register_int h_register_ptr = function
    184 | Register_int x_7308 -> h_register_int x_7308
    185 | Register_ptr (x_7310, x_7309) -> h_register_ptr x_7310 x_7309
     189| Register_int x_32 -> h_register_int x_32
     190| Register_ptr (x_34, x_33) -> h_register_ptr x_34 x_33
    186191
    187192(** val register_type_rect_Type0 :
     
    189194    -> 'a1) -> register_type -> 'a1 **)
    190195let rec register_type_rect_Type0 h_register_int h_register_ptr = function
    191 | Register_int x_7314 -> h_register_int x_7314
    192 | Register_ptr (x_7316, x_7315) -> h_register_ptr x_7316 x_7315
     196| Register_int x_38 -> h_register_int x_38
     197| Register_ptr (x_40, x_39) -> h_register_ptr x_40 x_39
    193198
    194199(** val register_type_inv_rect_Type4 :
     
    589594    let cast_srcrs = fun srcrs tmp ->
    590595      let srcrs_l = List.length srcrs in
    591       (match Nat.leb srcrs_l l with
     596      (match Nat.leb (Nat.S srcrs_l) l with
    592597       | Bool.True ->
    593598         (match last srcrs with
  • extracted/rTLabsToRTL.mli

    r2951 r3006  
    138138
    139139val size_of_sig_type : AST.typ -> Nat.nat
     140
     141val sign_of_sig_type : AST.typ -> AST.signedness
    140142
    141143type register_type =
Note: See TracChangeset for help on using the changeset viewer.