Changeset 1698
 Timestamp:
 Feb 16, 2012, 11:05:05 AM (6 years ago)
 Location:
 Deliverables/D5.15.3/costpluginindexedlabelsbranch/plugin
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D5.15.3/costpluginindexedlabelsbranch/plugin/compute.ml
r1689 r1698 654 654 let body_cost = Cost_value.reduce e e e body_cost in 655 655 let body_cost = Cost_value.amalgamation body_cost in 656 Printf.printf "%s\n" (to_string body_cost);657 656 mk_loop_cost_index index 0 v 1 body_cost 658 657 … … 933 932 let v1 = mk_value (Cost_value.Var counter) in 934 933 let v2 = mk_value init_value in 935 let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in 936 mk_invariant invariant 934 if v1 == v2 then 935 let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in 936 Some (mk_invariant invariant) 937 else 938 None 937 939 938 940 let mk_loop_invariant_counter_last_value … … 1009 1011 increment in 1010 1012 obj#push_index index; 1011 add_loop_annot obj stmt invariant_counter_init_value ; 1013 match invariant_counter_init_value with 1014  Some inv > 1015 add_loop_annot obj stmt inv 1016  None > (); 1012 1017 add_loop_annot obj stmt invariant_counter_last_value ; 1013 1018 add_loop_annot obj stmt invariant_counter_no_change ; 
Deliverables/D5.15.3/costpluginindexedlabelsbranch/plugin/cost_value.ml
r1508 r1698 318 318  BinOp (Sub, _, _), v :: Int i :: _ when i < 0 > 319 319 BinOp (Add, v, Int ( i)) 320  BinOp (Sub, _, _), (BinOp (Sub, v, Int i1)) :: (Int i2) :: _ > 321 BinOp (Sub, v, Int (i1 + i2)) 320 322  BinOp (Add, _, _), (Int i1) :: (BinOp (Sub, v, Int i2)) :: _ 321 323  BinOp (Add, _, _), (BinOp (Sub, v, Int i2)) :: (Int i1) :: _
Note: See TracChangeset
for help on using the changeset viewer.