Changeset 2960 for extracted/eRTLptr.ml


Ignore:
Timestamp:
Mar 26, 2013, 4:51:40 PM (7 years ago)
Author:
sacerdot
Message:

New extraction, it diverges in RTL execution now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/eRTLptr.ml

    r2951 r2960  
    130130    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    131131let rec ertlptr_seq_rect_Type4 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    132 | Ertlptr_ertl x_18654 -> h_ertlptr_ertl x_18654
    133 | LOW_ADDRESS (x_18656, x_18655) -> h_LOW_ADDRESS x_18656 x_18655
    134 | HIGH_ADDRESS (x_18658, x_18657) -> h_HIGH_ADDRESS x_18658 x_18657
     132| Ertlptr_ertl x_141 -> h_ertlptr_ertl x_141
     133| LOW_ADDRESS (x_143, x_142) -> h_LOW_ADDRESS x_143 x_142
     134| HIGH_ADDRESS (x_145, x_144) -> h_HIGH_ADDRESS x_145 x_144
    135135
    136136(** val ertlptr_seq_rect_Type5 :
     
    138138    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    139139let rec ertlptr_seq_rect_Type5 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    140 | Ertlptr_ertl x_18663 -> h_ertlptr_ertl x_18663
    141 | LOW_ADDRESS (x_18665, x_18664) -> h_LOW_ADDRESS x_18665 x_18664
    142 | HIGH_ADDRESS (x_18667, x_18666) -> h_HIGH_ADDRESS x_18667 x_18666
     140| Ertlptr_ertl x_150 -> h_ertlptr_ertl x_150
     141| LOW_ADDRESS (x_152, x_151) -> h_LOW_ADDRESS x_152 x_151
     142| HIGH_ADDRESS (x_154, x_153) -> h_HIGH_ADDRESS x_154 x_153
    143143
    144144(** val ertlptr_seq_rect_Type3 :
     
    146146    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    147147let rec ertlptr_seq_rect_Type3 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    148 | Ertlptr_ertl x_18672 -> h_ertlptr_ertl x_18672
    149 | LOW_ADDRESS (x_18674, x_18673) -> h_LOW_ADDRESS x_18674 x_18673
    150 | HIGH_ADDRESS (x_18676, x_18675) -> h_HIGH_ADDRESS x_18676 x_18675
     148| Ertlptr_ertl x_159 -> h_ertlptr_ertl x_159
     149| LOW_ADDRESS (x_161, x_160) -> h_LOW_ADDRESS x_161 x_160
     150| HIGH_ADDRESS (x_163, x_162) -> h_HIGH_ADDRESS x_163 x_162
    151151
    152152(** val ertlptr_seq_rect_Type2 :
     
    154154    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    155155let rec ertlptr_seq_rect_Type2 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    156 | Ertlptr_ertl x_18681 -> h_ertlptr_ertl x_18681
    157 | LOW_ADDRESS (x_18683, x_18682) -> h_LOW_ADDRESS x_18683 x_18682
    158 | HIGH_ADDRESS (x_18685, x_18684) -> h_HIGH_ADDRESS x_18685 x_18684
     156| Ertlptr_ertl x_168 -> h_ertlptr_ertl x_168
     157| LOW_ADDRESS (x_170, x_169) -> h_LOW_ADDRESS x_170 x_169
     158| HIGH_ADDRESS (x_172, x_171) -> h_HIGH_ADDRESS x_172 x_171
    159159
    160160(** val ertlptr_seq_rect_Type1 :
     
    162162    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    163163let rec ertlptr_seq_rect_Type1 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    164 | Ertlptr_ertl x_18690 -> h_ertlptr_ertl x_18690
    165 | LOW_ADDRESS (x_18692, x_18691) -> h_LOW_ADDRESS x_18692 x_18691
    166 | HIGH_ADDRESS (x_18694, x_18693) -> h_HIGH_ADDRESS x_18694 x_18693
     164| Ertlptr_ertl x_177 -> h_ertlptr_ertl x_177
     165| LOW_ADDRESS (x_179, x_178) -> h_LOW_ADDRESS x_179 x_178
     166| HIGH_ADDRESS (x_181, x_180) -> h_HIGH_ADDRESS x_181 x_180
    167167
    168168(** val ertlptr_seq_rect_Type0 :
     
    170170    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    171171let rec ertlptr_seq_rect_Type0 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    172 | Ertlptr_ertl x_18699 -> h_ertlptr_ertl x_18699
    173 | LOW_ADDRESS (x_18701, x_18700) -> h_LOW_ADDRESS x_18701 x_18700
    174 | HIGH_ADDRESS (x_18703, x_18702) -> h_HIGH_ADDRESS x_18703 x_18702
     172| Ertlptr_ertl x_186 -> h_ertlptr_ertl x_186
     173| LOW_ADDRESS (x_188, x_187) -> h_LOW_ADDRESS x_188 x_187
     174| HIGH_ADDRESS (x_190, x_189) -> h_HIGH_ADDRESS x_190 x_189
    175175
    176176(** val ertlptr_seq_inv_rect_Type4 :
     
    362362    Joint.add_graph eRTLptr (AST.prog_var_names p.Joint.joint_prog) l2
    363363      (Joint.Sequential ((Joint.CALL ((Types.Inl
    364       p.Joint.joint_prog.AST.prog_main),
    365       (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
     364      p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
    366365      (Obj.magic Types.It))), (Obj.magic l3))) res0
    367366  in
Note: See TracChangeset for help on using the changeset viewer.