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/rTL_semantics.ml

    r2951 r2960  
    157157    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    158158    'a1) -> reg_sp -> 'a1 **)
    159 let rec reg_sp_rect_Type4 h_mk_reg_sp x_6032 =
    160   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6032 in
     159let rec reg_sp_rect_Type4 h_mk_reg_sp x_3 =
     160  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_3 in
    161161  h_mk_reg_sp reg_sp_env0 stackp0
    162162
     
    164164    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    165165    'a1) -> reg_sp -> 'a1 **)
    166 let rec reg_sp_rect_Type5 h_mk_reg_sp x_6034 =
    167   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6034 in
     166let rec reg_sp_rect_Type5 h_mk_reg_sp x_5 =
     167  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_5 in
    168168  h_mk_reg_sp reg_sp_env0 stackp0
    169169
     
    171171    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    172172    'a1) -> reg_sp -> 'a1 **)
    173 let rec reg_sp_rect_Type3 h_mk_reg_sp x_6036 =
    174   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6036 in
     173let rec reg_sp_rect_Type3 h_mk_reg_sp x_7 =
     174  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_7 in
    175175  h_mk_reg_sp reg_sp_env0 stackp0
    176176
     
    178178    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    179179    'a1) -> reg_sp -> 'a1 **)
    180 let rec reg_sp_rect_Type2 h_mk_reg_sp x_6038 =
    181   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6038 in
     180let rec reg_sp_rect_Type2 h_mk_reg_sp x_9 =
     181  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_9 in
    182182  h_mk_reg_sp reg_sp_env0 stackp0
    183183
     
    185185    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    186186    'a1) -> reg_sp -> 'a1 **)
    187 let rec reg_sp_rect_Type1 h_mk_reg_sp x_6040 =
    188   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6040 in
     187let rec reg_sp_rect_Type1 h_mk_reg_sp x_11 =
     188  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_11 in
    189189  h_mk_reg_sp reg_sp_env0 stackp0
    190190
     
    192192    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    193193    'a1) -> reg_sp -> 'a1 **)
    194 let rec reg_sp_rect_Type0 h_mk_reg_sp x_6042 =
    195   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6042 in
     194let rec reg_sp_rect_Type0 h_mk_reg_sp x_13 =
     195  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_13 in
    196196  h_mk_reg_sp reg_sp_env0 stackp0
    197197
     
    297297    (Registers.register List.list -> ByteValues.program_counter ->
    298298    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    299 let rec frame_rect_Type4 h_mk_frame x_6058 =
     299let rec frame_rect_Type4 h_mk_frame x_29 =
    300300  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    301     fr_regs = fr_regs0 } = x_6058
     301    fr_regs = fr_regs0 } = x_29
    302302  in
    303303  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    306306    (Registers.register List.list -> ByteValues.program_counter ->
    307307    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    308 let rec frame_rect_Type5 h_mk_frame x_6060 =
     308let rec frame_rect_Type5 h_mk_frame x_31 =
    309309  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    310     fr_regs = fr_regs0 } = x_6060
     310    fr_regs = fr_regs0 } = x_31
    311311  in
    312312  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    315315    (Registers.register List.list -> ByteValues.program_counter ->
    316316    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    317 let rec frame_rect_Type3 h_mk_frame x_6062 =
     317let rec frame_rect_Type3 h_mk_frame x_33 =
    318318  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    319     fr_regs = fr_regs0 } = x_6062
     319    fr_regs = fr_regs0 } = x_33
    320320  in
    321321  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    324324    (Registers.register List.list -> ByteValues.program_counter ->
    325325    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    326 let rec frame_rect_Type2 h_mk_frame x_6064 =
     326let rec frame_rect_Type2 h_mk_frame x_35 =
    327327  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    328     fr_regs = fr_regs0 } = x_6064
     328    fr_regs = fr_regs0 } = x_35
    329329  in
    330330  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    333333    (Registers.register List.list -> ByteValues.program_counter ->
    334334    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    335 let rec frame_rect_Type1 h_mk_frame x_6066 =
     335let rec frame_rect_Type1 h_mk_frame x_37 =
    336336  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    337     fr_regs = fr_regs0 } = x_6066
     337    fr_regs = fr_regs0 } = x_37
    338338  in
    339339  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    342342    (Registers.register List.list -> ByteValues.program_counter ->
    343343    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    344 let rec frame_rect_Type0 h_mk_frame x_6068 =
     344let rec frame_rect_Type0 h_mk_frame x_39 =
    345345  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    346     fr_regs = fr_regs0 } = x_6068
     346    fr_regs = fr_regs0 } = x_39
    347347  in
    348348  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    471471          (Joint_semantics.set_m rTL_state_params mem st))))))) __
    472472
    473 (** val stackOverflow : ErrorMessages.errorMessage **)
    474 let stackOverflow = ErrorMessages.MISSING
    475 
    476473(** val rtl_setup_call_separate_overflow :
    477474    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
     
    485482    rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
    486483  | Bool.False ->
    487     Errors.Error (List.Cons ((Errors.MSG stackOverflow), List.Nil))
     484    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.StackOverflow), List.Nil))
    488485
    489486(** val rtl_setup_call_unique :
     
    535532    AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
    536533    Values.val0 List.list Errors.res **)
    537 let rtl_fetch_external_args _ = assert false
     534let rtl_fetch_external_args _ =
     535  failwith "AXIOM TO BE REALIZED"
    538536
    539537(** val rtl_set_result :
    540538    Values.val0 List.list -> Registers.register List.list -> rTL_state ->
    541539    rTL_state Errors.res **)
    542 let rtl_set_result _ = assert false
     540let rtl_set_result _ =
     541  failwith "AXIOM TO BE REALIZED"
    543542
    544543(** val rtl_reg_store :
Note: See TracChangeset for help on using the changeset viewer.