Changeset 3019 for extracted/lINToASM.ml


Ignore:
Timestamp:
Mar 28, 2013, 5:27:46 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after ERTLptr abortion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/lINToASM.ml

    r3001 r3019  
    143143    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    144144    -> 'a1 **)
    145 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_5553 =
     145let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_263 =
    146146  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    147147    ident_map0; label_map = label_map0; address_map = address_map0;
    148     fresh_cost_label = fresh_cost_label0 } = x_5553
     148    fresh_cost_label = fresh_cost_label0 } = x_263
    149149  in
    150150  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    157157    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    158158    -> 'a1 **)
    159 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_5555 =
     159let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_265 =
    160160  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    161161    ident_map0; label_map = label_map0; address_map = address_map0;
    162     fresh_cost_label = fresh_cost_label0 } = x_5555
     162    fresh_cost_label = fresh_cost_label0 } = x_265
    163163  in
    164164  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    171171    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    172172    -> 'a1 **)
    173 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_5557 =
     173let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_267 =
    174174  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    175175    ident_map0; label_map = label_map0; address_map = address_map0;
    176     fresh_cost_label = fresh_cost_label0 } = x_5557
     176    fresh_cost_label = fresh_cost_label0 } = x_267
    177177  in
    178178  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    185185    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    186186    -> 'a1 **)
    187 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_5559 =
     187let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_269 =
    188188  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    189189    ident_map0; label_map = label_map0; address_map = address_map0;
    190     fresh_cost_label = fresh_cost_label0 } = x_5559
     190    fresh_cost_label = fresh_cost_label0 } = x_269
    191191  in
    192192  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    199199    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    200200    -> 'a1 **)
    201 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_5561 =
     201let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_271 =
    202202  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    203203    ident_map0; label_map = label_map0; address_map = address_map0;
    204     fresh_cost_label = fresh_cost_label0 } = x_5561
     204    fresh_cost_label = fresh_cost_label0 } = x_271
    205205  in
    206206  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    213213    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    214214    -> 'a1 **)
    215 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_5563 =
     215let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_273 =
    216216  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    217217    ident_map0; label_map = label_map0; address_map = address_map0;
    218     fresh_cost_label = fresh_cost_label0 } = x_5563
     218    fresh_cost_label = fresh_cost_label0 } = x_273
    219219  in
    220220  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    320320  let globals_addr_internal = fun res_offset x_size ->
    321321    let { Types.fst = res; Types.snd = offset } = res_offset in
    322     let { Types.fst = eta27394; Types.snd = data } = x_size in
    323     let { Types.fst = x; Types.snd = region } = eta27394 in
     322    let { Types.fst = eta11; Types.snd = data } = x_size in
     323    let { Types.fst = x; Types.snd = region } = eta11 in
    324324    { Types.fst =
    325325    (Identifiers.add PreIdentifiers.SymbolTag res x
     
    333333      (Identifiers.empty_map PreIdentifiers.SymbolTag); Types.snd =
    334334      (Z.zopp
    335         (Z.z_of_nat
    336           (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p))) }
     335        (Z.z_of_nat (Nat.S
     336          (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p)))) }
    337337      (AST.prog_vars p.Joint.joint_prog)
    338338  in
     
    352352        (Identifiers.empty_map PreIdentifiers.LabelTag)
    353353    in
    354     let { Types.fst = eta27395; Types.snd = lmap0 } =
     354    let { Types.fst = eta12; Types.snd = lmap0 } =
    355355      match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
    356356      | Types.None ->
     
    364364          lmap }
    365365    in
    366     let { Types.fst = id; Types.snd = univ } = eta27395 in
     366    let { Types.fst = id; Types.snd = univ } = eta12 in
    367367    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    368368    u.ident_map; label_map =
     
    377377  Obj.magic (fun u ->
    378378    let imap = u.ident_map in
    379     let { Types.fst = eta27396; Types.snd = imap0 } =
     379    let { Types.fst = eta13; Types.snd = imap0 } =
    380380      match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
    381381      | Types.None ->
     
    389389          imap }
    390390    in
    391     let { Types.fst = id; Types.snd = univ } = eta27396 in
     391    let { Types.fst = id; Types.snd = univ } = eta13 in
    392392    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    393393    ident_map = imap0; label_map = u.label_map; address_map = u.address_map;
     
    990990             (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inr { Types.fst =
    991991             ASM.CARRY; Types.snd = asm_other_bit }))))
    992          | Joint_LTL_LIN.LOW_ADDRESS (reg, lbl) ->
     992         | Joint_LTL_LIN.LOW_ADDRESS lbl ->
    993993           Monad.m_bind0 (Monad.smax_def State.state_monad)
    994994             (identifier_of_label globals lbl) (fun lbl' ->
    995995             Monad.m_return0 (Monad.smax_def State.state_monad)
    996                (ASM.MovSuccessor ((register_address reg), ASM.LOW, lbl')))
    997          | Joint_LTL_LIN.HIGH_ADDRESS (reg, lbl) ->
     996               (ASM.MovSuccessor ((register_address I8051.RegisterA),
     997               ASM.LOW, lbl')))
     998         | Joint_LTL_LIN.HIGH_ADDRESS lbl ->
    998999           Monad.m_bind0 (Monad.smax_def State.state_monad)
    9991000             (identifier_of_label globals lbl) (fun lbl' ->
    10001001             Monad.m_return0 (Monad.smax_def State.state_monad)
    1001                (ASM.MovSuccessor ((register_address reg), ASM.HIGH, lbl'))))))
     1002               (ASM.MovSuccessor ((register_address I8051.RegisterA),
     1003               ASM.HIGH, lbl'))))))
    10021004| Joint.Final instr ->
    10031005  (match instr with
     
    10761078    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    10771079    -> 'a1 **)
    1078 let rec init_mutable_rect_Type4 h_mk_init_mutable x_5580 =
     1080let rec init_mutable_rect_Type4 h_mk_init_mutable x_290 =
    10791081  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1080     built0 } = x_5580
     1082    built0 } = x_290
    10811083  in
    10821084  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    10851087    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    10861088    -> 'a1 **)
    1087 let rec init_mutable_rect_Type5 h_mk_init_mutable x_5582 =
     1089let rec init_mutable_rect_Type5 h_mk_init_mutable x_292 =
    10881090  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1089     built0 } = x_5582
     1091    built0 } = x_292
    10901092  in
    10911093  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    10941096    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    10951097    -> 'a1 **)
    1096 let rec init_mutable_rect_Type3 h_mk_init_mutable x_5584 =
     1098let rec init_mutable_rect_Type3 h_mk_init_mutable x_294 =
    10971099  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1098     built0 } = x_5584
     1100    built0 } = x_294
    10991101  in
    11001102  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    11031105    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    11041106    -> 'a1 **)
    1105 let rec init_mutable_rect_Type2 h_mk_init_mutable x_5586 =
     1107let rec init_mutable_rect_Type2 h_mk_init_mutable x_296 =
    11061108  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1107     built0 } = x_5586
     1109    built0 } = x_296
    11081110  in
    11091111  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    11121114    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    11131115    -> 'a1 **)
    1114 let rec init_mutable_rect_Type1 h_mk_init_mutable x_5588 =
     1116let rec init_mutable_rect_Type1 h_mk_init_mutable x_298 =
    11151117  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1116     built0 } = x_5588
     1118    built0 } = x_298
    11171119  in
    11181120  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    11211123    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    11221124    -> 'a1 **)
    1123 let rec init_mutable_rect_Type0 h_mk_init_mutable x_5590 =
     1125let rec init_mutable_rect_Type0 h_mk_init_mutable x_300 =
    11241126  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1125     built0 } = x_5590
     1127    built0 } = x_300
    11261128  in
    11271129  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    12951297      let start_sp =
    12961298        Z.zopp
    1297           (Z.z_of_nat
    1298             (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p))
     1299          (Z.z_of_nat (Nat.S
     1300            (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p)))
    12991301      in
    13001302      let { Types.fst = sph; Types.snd = spl } =
Note: See TracChangeset for help on using the changeset viewer.