Changeset 1698


Ignore:
Timestamp:
Feb 16, 2012, 11:05:05 AM (6 years ago)
Author:
tranquil
Message:

minor modifications

Location:
Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/plugin
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/plugin/compute.ml

    r1689 r1698  
    654654    let body_cost = Cost_value.reduce e e e body_cost in
    655655    let body_cost = Cost_value.amalgamation body_cost in
    656     Printf.printf "%s\n" (to_string body_cost);
    657656    mk_loop_cost_index index 0 v 1 body_cost
    658657
     
    933932  let v1 = mk_value (Cost_value.Var counter) in
    934933  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
    937939
    938940let mk_loop_invariant_counter_last_value
     
    10091011      increment in
    10101012  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 -> ();
    10121017  add_loop_annot obj stmt invariant_counter_last_value ;
    10131018  add_loop_annot obj stmt invariant_counter_no_change ;
  • Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/plugin/cost_value.ml

    r1508 r1698  
    318318  | BinOp (Sub, _, _), v :: Int i :: _ when i < 0 ->
    319319    BinOp (Add, v, Int (- i))
     320  | BinOp (Sub, _, _), (BinOp (Sub, v, Int i1)) :: (Int i2) :: _ ->
     321    BinOp (Sub, v, Int (i1 + i2))
    320322  | BinOp (Add, _, _), (Int i1) :: (BinOp (Sub, v, Int i2)) :: _
    321323  | BinOp (Add, _, _), (BinOp (Sub, v, Int i2)) :: (Int i1) :: _
Note: See TracChangeset for help on using the changeset viewer.