Changeset 1163 for src/ERTL/ERTLToLTL.ma
 Timestamp:
 Sep 1, 2011, 4:23:42 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1161 r1163 31 31 let 〈l, luniv〉 ≝ fresh_label globals luniv in 32 32 let graph ≝ add_graph globals l stmt graph in 33 〈l, 〈graph, luniv〉〉.33 〈l, graph, luniv〉. 34 34 35 35 definition num_locals ≝ 36 λint_fun. 37 colour_locals + (ertl_if_stacksize int_fun). 36 λglobals. 37 λint_fun. 38 colour_locals + (ertl_if_stacksize globals int_fun). 38 39 39 40 definition stacksize ≝ 40 λint_fun. 41 colour_locals + (ertl_if_stacksize int_fun). 41 λglobals. 42 λint_fun. 43 colour_locals + (ertl_if_stacksize globals int_fun). 42 44 43 45 definition adjust_off ≝ 46 λglobals. 44 47 λint_fun. 45 48 λoff. 46 49 let 〈ignore, int_off〉 ≝ half_add ? int_size off in 47 let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals int_fun)) int_off false in50 let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in 48 51 sub. 49 52 53 check 54 50 55 definition get_stack ≝ 51 λ int_fun.52 λ globals.56 λglobals. 57 λint_fun. 53 58 λgraph: graph (ltl_statement (globals)). 54 59 λr. 55 60 λoff. 56 61 λl. 57 let off ≝ adjust_off int_fun off in 58 let luniv ≝ ertl_if_luniverse int_fun in 59 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in 62 let off ≝ adjust_off globals int_fun off in 63 let luniv ≝ ertl_if_luniverse globals int_fun in 64 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_hdw_to_hdw globals … 〈RegisterA, r〉) l) in 65 ?. 66 60 67 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in 61 68 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
Note: See TracChangeset
for help on using the changeset viewer.