Changeset 1698 for Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch

Timestamp:

Feb 16, 2012, 11:05:05 AM (9 years ago)

Author:

tranquil

Message:

minor modifications

Location:

Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/plugin

Files:

• compute.ml (modified) (3 diffs)
• cost_value.ml (modified) (1 diff)

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

@@ -654 +654 @@
     let body_cost = Cost_value.reduce e e e body_cost in
     let body_cost = Cost_value.amalgamation body_cost in
-    Printf.printf "%s\n" (to_string body_cost);
     mk_loop_cost_index index 0 v 1 body_cost
 
@@ -933 +932 @@
   let v1 = mk_value (Cost_value.Var counter) in
   let v2 = mk_value init_value in
-  let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in
-  mk_invariant invariant
+  if v1 == v2 then
+    let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in
+    Some (mk_invariant invariant)
+  else
+    None
 
 let mk_loop_invariant_counter_last_value
@@ -1009 +1011 @@
       increment in
   obj#push_index index;
-  add_loop_annot obj stmt invariant_counter_init_value ;
+  match invariant_counter_init_value with
+    | Some inv ->
+      add_loop_annot obj stmt inv
+    | None -> ();
   add_loop_annot obj stmt invariant_counter_last_value ;
   add_loop_annot obj stmt invariant_counter_no_change ;

Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/plugin/cost_value.ml

@@ -318 +318 @@
   | BinOp (Sub, _, _), v :: Int i :: _ when i < 0 ->
     BinOp (Add, v, Int (- i))
+  | BinOp (Sub, _, _), (BinOp (Sub, v, Int i1)) :: (Int i2) :: _ ->
+    BinOp (Sub, v, Int (i1 + i2))
   | BinOp (Add, _, _), (Int i1) :: (BinOp (Sub, v, Int i2)) :: _
   | BinOp (Add, _, _), (BinOp (Sub, v, Int i2)) :: (Int i1) :: _