Changeset 3043 for extracted/values.ml


Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/values.ml

    r2997 r3043  
    9090let rec val_rect_Type4 h_Vundef h_Vint h_Vnull h_Vptr = function
    9191| Vundef -> h_Vundef
    92 | Vint (sz, x_3980) -> h_Vint sz x_3980
     92| Vint (sz, x_5112) -> h_Vint sz x_5112
    9393| Vnull -> h_Vnull
    94 | Vptr x_3981 -> h_Vptr x_3981
     94| Vptr x_5113 -> h_Vptr x_5113
    9595
    9696(** val val_rect_Type5 :
     
    9999let rec val_rect_Type5 h_Vundef h_Vint h_Vnull h_Vptr = function
    100100| Vundef -> h_Vundef
    101 | Vint (sz, x_3987) -> h_Vint sz x_3987
     101| Vint (sz, x_5119) -> h_Vint sz x_5119
    102102| Vnull -> h_Vnull
    103 | Vptr x_3988 -> h_Vptr x_3988
     103| Vptr x_5120 -> h_Vptr x_5120
    104104
    105105(** val val_rect_Type3 :
     
    108108let rec val_rect_Type3 h_Vundef h_Vint h_Vnull h_Vptr = function
    109109| Vundef -> h_Vundef
    110 | Vint (sz, x_3994) -> h_Vint sz x_3994
     110| Vint (sz, x_5126) -> h_Vint sz x_5126
    111111| Vnull -> h_Vnull
    112 | Vptr x_3995 -> h_Vptr x_3995
     112| Vptr x_5127 -> h_Vptr x_5127
    113113
    114114(** val val_rect_Type2 :
     
    117117let rec val_rect_Type2 h_Vundef h_Vint h_Vnull h_Vptr = function
    118118| Vundef -> h_Vundef
    119 | Vint (sz, x_4001) -> h_Vint sz x_4001
     119| Vint (sz, x_5133) -> h_Vint sz x_5133
    120120| Vnull -> h_Vnull
    121 | Vptr x_4002 -> h_Vptr x_4002
     121| Vptr x_5134 -> h_Vptr x_5134
    122122
    123123(** val val_rect_Type1 :
     
    126126let rec val_rect_Type1 h_Vundef h_Vint h_Vnull h_Vptr = function
    127127| Vundef -> h_Vundef
    128 | Vint (sz, x_4008) -> h_Vint sz x_4008
     128| Vint (sz, x_5140) -> h_Vint sz x_5140
    129129| Vnull -> h_Vnull
    130 | Vptr x_4009 -> h_Vptr x_4009
     130| Vptr x_5141 -> h_Vptr x_5141
    131131
    132132(** val val_rect_Type0 :
     
    135135let rec val_rect_Type0 h_Vundef h_Vint h_Vnull h_Vptr = function
    136136| Vundef -> h_Vundef
    137 | Vint (sz, x_4015) -> h_Vint sz x_4015
     137| Vint (sz, x_5147) -> h_Vint sz x_5147
    138138| Vnull -> h_Vnull
    139 | Vptr x_4016 -> h_Vptr x_4016
     139| Vptr x_5148 -> h_Vptr x_5148
    140140
    141141(** val val_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.