Ignore:
Timestamp:
Mar 21, 2013, 8:11:50 PM (6 years ago)
Author:
sacerdot
Message:

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/byteValues.mli

    r2773 r2933  
    390390val word_of_list_beval : beval List.list -> Integers.int Errors.res
    391391
     392type add_or_sub =
     393| Do_add
     394| Do_sub
     395
     396val add_or_sub_rect_Type4 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     397
     398val add_or_sub_rect_Type5 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     399
     400val add_or_sub_rect_Type3 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     401
     402val add_or_sub_rect_Type2 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     403
     404val add_or_sub_rect_Type1 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     405
     406val add_or_sub_rect_Type0 : 'a1 -> 'a1 -> add_or_sub -> 'a1
     407
     408val add_or_sub_inv_rect_Type4 :
     409  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     410
     411val add_or_sub_inv_rect_Type3 :
     412  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     413
     414val add_or_sub_inv_rect_Type2 :
     415  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     416
     417val add_or_sub_inv_rect_Type1 :
     418  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     419
     420val add_or_sub_inv_rect_Type0 :
     421  add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     422
     423val add_or_sub_discr : add_or_sub -> add_or_sub -> __
     424
     425val add_or_sub_jmdiscr : add_or_sub -> add_or_sub -> __
     426
     427val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool
     428
    392429type bebit =
    393430| BBbit of Bool.bool
    394431| BBundef
    395 | BBptrcarry of Bool.bool * Pointers.pointer * part * BitVector.bitVector
     432| BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector
    396433
    397434val bebit_rect_Type4 :
    398   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     435  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    399436  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    400437
    401438val bebit_rect_Type5 :
    402   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     439  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    403440  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    404441
    405442val bebit_rect_Type3 :
    406   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     443  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    407444  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    408445
    409446val bebit_rect_Type2 :
    410   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     447  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    411448  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    412449
    413450val bebit_rect_Type1 :
    414   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     451  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    415452  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    416453
    417454val bebit_rect_Type0 :
    418   (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     455  (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    419456  BitVector.bitVector -> 'a1) -> bebit -> 'a1
    420457
    421458val bebit_inv_rect_Type4 :
    422   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     459  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    423460  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
    424461
    425462val bebit_inv_rect_Type3 :
    426   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     463  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    427464  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
    428465
    429466val bebit_inv_rect_Type2 :
    430   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     467  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    431468  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
    432469
    433470val bebit_inv_rect_Type1 :
    434   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     471  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    435472  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
    436473
    437474val bebit_inv_rect_Type0 :
    438   bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     475  bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    439476  Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1
    440477
Note: See TracChangeset for help on using the changeset viewer.