Changeset 3073


Ignore:
Timestamp:
Apr 2, 2013, 6:44:34 PM (4 years ago)
Author:
sacerdot
Message:

New extraction, all tests pass.

Files:
2 edited

Legend:

Unmodified
Added
Removed
  • driver/tests/PROBLEMI

    r3071 r3073  
    555. ok
    666. ok
    7 7. LTL failure
     77. ok
    888. ok
    9 bubble_sort.c: different trace in ERTL, different result in Assembly
     9bubble_sort.c: ok
  • extracted/eRTLToLTL.ml

    r3059 r3073  
    179179    arg_decision -> 'a1 **)
    180180let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    181 | Arg_decision_colour x_19045 -> h_arg_decision_colour x_19045
    182 | Arg_decision_spill x_19046 -> h_arg_decision_spill x_19046
    183 | Arg_decision_imm x_19047 -> h_arg_decision_imm x_19047
     181| Arg_decision_colour x_9 -> h_arg_decision_colour x_9
     182| Arg_decision_spill x_10 -> h_arg_decision_spill x_10
     183| Arg_decision_imm x_11 -> h_arg_decision_imm x_11
    184184
    185185(** val arg_decision_rect_Type5 :
     
    187187    arg_decision -> 'a1 **)
    188188let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    189 | Arg_decision_colour x_19052 -> h_arg_decision_colour x_19052
    190 | Arg_decision_spill x_19053 -> h_arg_decision_spill x_19053
    191 | Arg_decision_imm x_19054 -> h_arg_decision_imm x_19054
     189| Arg_decision_colour x_16 -> h_arg_decision_colour x_16
     190| Arg_decision_spill x_17 -> h_arg_decision_spill x_17
     191| Arg_decision_imm x_18 -> h_arg_decision_imm x_18
    192192
    193193(** val arg_decision_rect_Type3 :
     
    195195    arg_decision -> 'a1 **)
    196196let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    197 | Arg_decision_colour x_19059 -> h_arg_decision_colour x_19059
    198 | Arg_decision_spill x_19060 -> h_arg_decision_spill x_19060
    199 | Arg_decision_imm x_19061 -> h_arg_decision_imm x_19061
     197| Arg_decision_colour x_23 -> h_arg_decision_colour x_23
     198| Arg_decision_spill x_24 -> h_arg_decision_spill x_24
     199| Arg_decision_imm x_25 -> h_arg_decision_imm x_25
    200200
    201201(** val arg_decision_rect_Type2 :
     
    203203    arg_decision -> 'a1 **)
    204204let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    205 | Arg_decision_colour x_19066 -> h_arg_decision_colour x_19066
    206 | Arg_decision_spill x_19067 -> h_arg_decision_spill x_19067
    207 | Arg_decision_imm x_19068 -> h_arg_decision_imm x_19068
     205| Arg_decision_colour x_30 -> h_arg_decision_colour x_30
     206| Arg_decision_spill x_31 -> h_arg_decision_spill x_31
     207| Arg_decision_imm x_32 -> h_arg_decision_imm x_32
    208208
    209209(** val arg_decision_rect_Type1 :
     
    211211    arg_decision -> 'a1 **)
    212212let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    213 | Arg_decision_colour x_19073 -> h_arg_decision_colour x_19073
    214 | Arg_decision_spill x_19074 -> h_arg_decision_spill x_19074
    215 | Arg_decision_imm x_19075 -> h_arg_decision_imm x_19075
     213| Arg_decision_colour x_37 -> h_arg_decision_colour x_37
     214| Arg_decision_spill x_38 -> h_arg_decision_spill x_38
     215| Arg_decision_imm x_39 -> h_arg_decision_imm x_39
    216216
    217217(** val arg_decision_rect_Type0 :
     
    219219    arg_decision -> 'a1 **)
    220220let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    221 | Arg_decision_colour x_19080 -> h_arg_decision_colour x_19080
    222 | Arg_decision_spill x_19081 -> h_arg_decision_spill x_19081
    223 | Arg_decision_imm x_19082 -> h_arg_decision_imm x_19082
     221| Arg_decision_colour x_44 -> h_arg_decision_colour x_44
     222| Arg_decision_spill x_45 -> h_arg_decision_spill x_45
     223| Arg_decision_imm x_46 -> h_arg_decision_imm x_46
    224224
    225225(** val arg_decision_inv_rect_Type4 :
     
    749749             (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerST0)))),
    750750             List.Nil)))
    751        | Bool.False -> move_to_dptr) (List.Cons ((Joint.STORE
     751       | Bool.False ->
     752         List.append move_to_dptr
     753           (move globals localss Bool.False (Interference.Decision_colour
     754             I8051.RegisterA) src)) (List.Cons ((Joint.STORE
    752755      ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
    753756      List.Nil)))
Note: See TracChangeset for help on using the changeset viewer.