Merge pull request #25 from ManuelLerchner/indent-fixes

fixed all current ocp-indent failures

Author: ManuelLerchner

src/cdomain/value/cdomains/int/bitfieldDomain.ml

@@ -78,7 +78,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
   let bitmask_up_to pos =
     let top_bit = Ints_t.one <<: pos in
     if top_bit =: Ints_t.zero
-      then Ints_t.zero
+    then Ints_t.zero
     else
       Ints_t.sub top_bit Ints_t.one
 
@@ -122,27 +122,27 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let shift_right ik (z1, o1) (z2, o2) = 
     if is_const (z2, o2) 
-      then 
-        shift_right ik (z1, o1) (Ints_t.to_int o2)
+    then 
+      shift_right ik (z1, o1) (Ints_t.to_int o2)
     else
       let shift_counts = concretize (z2, o2) in
       List.fold_left (fun acc c ->
-        let next = shift_right ik (z1, o1) c in join acc next
-      ) (zero_mask, zero_mask) shift_counts
+          let next = shift_right ik (z1, o1) c in join acc next
+        ) (zero_mask, zero_mask) shift_counts
 
   let shift_left _ (z,o) c =
     let zero_mask = bitmask_up_to c in
     ((z <<: c) |: zero_mask, o <<: c)
 
   let shift_left ik (z1, o1) (z2, o2) = 
     if is_const (z2, o2) 
-      then 
-        shift_left ik (z1, o1) (Ints_t.to_int o2)
+    then 
+      shift_left ik (z1, o1) (Ints_t.to_int o2)
     else
       let shift_counts = concretize (z2, o2) in
       List.fold_left (fun acc c ->
-        let next = shift_left ik (z1, o1) c in join acc next
-      ) (zero_mask, zero_mask) shift_counts
+          let next = shift_left ik (z1, o1) c in join acc next
+        ) (zero_mask, zero_mask) shift_counts
 end
 
 module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) = struct
@@ -161,7 +161,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
   let top_of ik = 
     if isSigned ik then top () 
     else (BArith.one_mask, Ints_t.of_bigint (snd (Size.range ik)))
-    
+
   let bot_of ik = bot ()
 
   let to_pretty_bits (z,o) = 
@@ -171,38 +171,38 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     let z_mask = ref z in
 
     let rec to_pretty_bits' acc =
-        let current_bit_known = (!known_bitmask &: Ints_t.one) = Ints_t.one in
-        let current_bit_impossible = (!invalid_bitmask &: Ints_t.one) = Ints_t.one in
-
-        let bit_value = !o_mask &: Ints_t.one in
-        let bit =
-          if current_bit_impossible then "⊥"
-          else if not current_bit_known then "⊤"
-          else Ints_t.to_string bit_value 
-        in
+      let current_bit_known = (!known_bitmask &: Ints_t.one) = Ints_t.one in
+      let current_bit_impossible = (!invalid_bitmask &: Ints_t.one) = Ints_t.one in
+
+      let bit_value = !o_mask &: Ints_t.one in
+      let bit =
+        if current_bit_impossible then "⊥"
+        else if not current_bit_known then "⊤"
+        else Ints_t.to_string bit_value 
+      in
 
-        if (!o_mask = Ints_t.of_int (-1) || !o_mask = Ints_t.zero ) && (!z_mask = Ints_t.of_int (-1) || !z_mask = Ints_t.zero) then
-          let prefix = bit ^ "..." ^ bit in
-          prefix ^ acc
-        else
-          (known_bitmask := !known_bitmask >>: 1;
-          invalid_bitmask := !invalid_bitmask >>: 1;
-          o_mask := !o_mask >>: 1;
-          z_mask := !z_mask >>: 1;
-          to_pretty_bits' (bit ^ acc))
+      if (!o_mask = Ints_t.of_int (-1) || !o_mask = Ints_t.zero ) && (!z_mask = Ints_t.of_int (-1) || !z_mask = Ints_t.zero) then
+        let prefix = bit ^ "..." ^ bit in
+        prefix ^ acc
+      else
+        (known_bitmask := !known_bitmask >>: 1;
+         invalid_bitmask := !invalid_bitmask >>: 1;
+         o_mask := !o_mask >>: 1;
+         z_mask := !z_mask >>: 1;
+         to_pretty_bits' (bit ^ acc))
     in
     "0b" ^ to_pretty_bits' ""
 
   let show t = 
     if t = bot () then "bot" else
     if t = top () then "top" else
       let (z,o) = t in
-        Format.sprintf "{%s, (zs:%s, os:%s)}" (to_pretty_bits t) (Ints_t.to_string z) (Ints_t.to_string o) 
+      Format.sprintf "{%s, (zs:%s, os:%s)}" (to_pretty_bits t) (Ints_t.to_string z) (Ints_t.to_string o) 
 
   include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
 
   let range ik bf = (BArith.min ik bf, BArith.max ik bf)
-  
+
   let maximal (z,o) =     
     if (z < Ints_t.zero) <> (o < Ints_t.zero) then Some o
     else None
@@ -240,8 +240,8 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
         (new_bitfield, overflow_info)
       else if should_ignore_overflow ik then 
         (M.warn ~category:M.Category.Integer.overflow "Bitfield: Value was outside of range, indicating overflow, but 'sem.int.signed_overflow' is 'assume_none' -> Returned Top";
-        (* (bot (), overflow_info)) *)
-        (top_of ik, overflow_info))
+         (* (bot (), overflow_info)) *)
+         (top_of ik, overflow_info))
       else 
         (top_of ik, overflow_info)
 
@@ -274,7 +274,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     let (min_ik, max_ik) = Size.range ik in
     let startv = Ints_t.max x (Ints_t.of_bigint min_ik) in
     let endv= Ints_t.min y (Ints_t.of_bigint max_ik) in
-    
+
     let rec analyze_bits pos (acc_z, acc_o) =
       if pos < 0 then (acc_z, acc_o)
       else
@@ -284,15 +284,15 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
 
         let without_remainder = Ints_t.sub startv remainder in
         let bigger_number = Ints_t.add without_remainder position in
-        
+
         let bit_status =
           if Ints_t.compare bigger_number endv <= 0 then
             `top
           else 
-            if Ints_t.equal (Ints_t.logand (Ints_t.shift_right startv pos) Ints_t.one) Ints_t.one then
-              `one
-            else
-              `zero
+          if Ints_t.equal (Ints_t.logand (Ints_t.shift_right startv pos) Ints_t.one) Ints_t.one then
+            `one
+          else
+            `zero
         in
 
         let new_acc = 
@@ -365,7 +365,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     (z |: !:mask, o &: mask)
 
   let is_invalid_shift_operation ik a b = BArith.is_invalid b
-    || BArith.is_invalid a
+                                          || BArith.is_invalid a
 
   let is_undefined_shift_operation ik a b =
     let some_negatives = BArith.min ik b < Z.zero in
@@ -375,23 +375,23 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
   let shift_right ik a b = 
     if M.tracing then M.trace "bitfield" "%a >> %a" pretty a pretty b; 
     if is_invalid_shift_operation ik a b
-      then
-        (bot (), {underflow=false; overflow=false})
+    then
+      (bot (), {underflow=false; overflow=false})
     else if is_undefined_shift_operation ik a b
-      then
-        (top_of ik, {underflow=false; overflow=false})
+    then
+      (top_of ik, {underflow=false; overflow=false})
     else
       let defined_shifts = cap_bitshifts_to_precision ik b in
       norm ik @@ BArith.shift_right ik a defined_shifts
 
   let shift_left ik a b =
     if M.tracing then M.trace "bitfield" "%a << %a" pretty a pretty b;
     if is_invalid_shift_operation ik a b
-      then
-        (bot (), {underflow=false; overflow=false})
+    then
+      (bot (), {underflow=false; overflow=false})
     else if is_undefined_shift_operation ik a b
-      then
-        (top_of ik, {underflow=false; overflow=false})
+    then
+      (top_of ik, {underflow=false; overflow=false})
     else
       let defined_shifts = cap_bitshifts_to_precision ik b in
       norm ik @@ BArith.shift_left ik a defined_shifts
@@ -461,10 +461,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     let signBitDefZ = !:(o1 ^: o2) &: bitmask in
     for _ = size downto 0 do 
       (if !pm &: Ints_t.one == Ints_t.one then 
-        accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (!qv |: !qm))
-      else if !pv &: Ints_t.one == Ints_t.one then
-        accv := fst(add_paper !accv Ints_t.zero !qv Ints_t.zero);
-        accm := snd(add_paper Ints_t.zero !accm Ints_t.zero !qm));
+         accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (!qv |: !qm))
+       else if !pv &: Ints_t.one == Ints_t.one then
+         accv := fst(add_paper !accv Ints_t.zero !qv Ints_t.zero);
+       accm := snd(add_paper Ints_t.zero !accm Ints_t.zero !qm));
 
       pv := !pv >>: 1;
       pm := !pm >>: 1;
@@ -586,7 +586,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     QCheck.(set_shrink shrink @@ set_print show @@ map (fun (i1,i2) -> norm ik (i1,i2) |> fst ) pair_arb)
 
   let project ik p t = t
-  
+
 end
 
 module Bitfield = BitfieldFunctor (IntOps.BigIntOps)

src/cdomain/value/cdomains/int/congruenceDomain.ml

@@ -142,13 +142,13 @@ struct
   let to_bitfield ik x = 
     let is_power_of_two x = (Z.logand x (x -: Z.one) = Z.zero) in
     match x with None -> (Z.zero, Z.zero) | Some (c,m) ->
-    if m = Z.zero then (Z.lognot c, c)
-    else if is_power_of_two m then 
-      let mod_mask = m -: Z.one in 
-      let z = Z.lognot c in 
-      let o = Z.logor (Z.lognot mod_mask) c in 
-      (z,o)
-    else (Z.lognot Z.zero, Z.lognot Z.zero)
+      if m = Z.zero then (Z.lognot c, c)
+      else if is_power_of_two m then 
+        let mod_mask = m -: Z.one in 
+        let z = Z.lognot c in 
+        let o = Z.logor (Z.lognot mod_mask) c in 
+        (z,o)
+      else (Z.lognot Z.zero, Z.lognot Z.zero)
 
   let maximal t = match t with
     | Some (x, y) when y =: Z.zero -> Some x

src/cdomain/value/cdomains/int/defExcDomain.ml

@@ -299,11 +299,11 @@ struct
       let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else  S.empty () in
       norm ik @@ (`Excluded (ex, r))
 
-    let to_bitfield ik x = 
-      match x with 
+  let to_bitfield ik x = 
+    match x with 
       `Definite c -> (Z.lognot c, c) |
       _ -> let one_mask = Z.lognot Z.zero 
-           in (one_mask, one_mask)
+      in (one_mask, one_mask)
 
   let starting ?(suppress_ovwarn=false) ikind x =
     let _,u_ik = Size.range ikind in

src/cdomain/value/cdomains/int/enumsDomain.ml

@@ -252,13 +252,13 @@ module Enums : S with type int_t = Z.t = struct
 
   let to_bitfield ik x = 
     match x with 
-    Inc i when BISet.is_empty i -> (Z.zero, Z.zero) |
-    Inc i when BISet.is_singleton i -> 
+      Inc i when BISet.is_empty i -> (Z.zero, Z.zero) |
+      Inc i when BISet.is_singleton i -> 
       let o = BISet.choose i 
       in (Z.lognot o, o) |
-    Inc i -> BISet.fold (fun o (az, ao) -> (Z.logor (Z.lognot o) az, Z.logor o ao)) i (Z.zero, Z.zero) |
-    _ -> let one_mask = Z.lognot Z.zero     
-    in (one_mask, one_mask)
+      Inc i -> BISet.fold (fun o (az, ao) -> (Z.logor (Z.lognot o) az, Z.logor o ao)) i (Z.zero, Z.zero) |
+      _ -> let one_mask = Z.lognot Z.zero     
+      in (one_mask, one_mask)
 
   let starting ?(suppress_ovwarn=false) ikind x =
     let _,u_ik = Size.range ikind in

src/cdomain/value/cdomains/int/intervalDomain.ml

@@ -89,11 +89,11 @@ struct
       if isSigned ik && isNegative then Ints_t.logor signMask (Ints_t.lognot z)
       else Ints_t.lognot z
     in let max ik (z,o) =
-      let signBit = Ints_t.shift_left Ints_t.one ((Size.bit ik) - 1) in 
-      let signMask = Ints_t.of_bigint (snd (Size.range ik)) in
-      let isPositive = Ints_t.logand signBit z <> Ints_t.zero in
-      if isSigned ik && isPositive then Ints_t.logand signMask o
-      else o 
+         let signBit = Ints_t.shift_left Ints_t.one ((Size.bit ik) - 1) in 
+         let signMask = Ints_t.of_bigint (snd (Size.range ik)) in
+         let isPositive = Ints_t.logand signBit z <> Ints_t.zero in
+         if isSigned ik && isPositive then Ints_t.logand signMask o
+         else o 
     in fst (norm ik (Some (min ik x, max ik x)))
 
   let of_int ik (x: int_t) = of_interval ik (x,x)
@@ -103,53 +103,53 @@ struct
 
   let to_bitfield ik z = 
     match z with None -> (Ints_t.lognot Ints_t.zero, Ints_t.lognot Ints_t.zero) | Some (x,y) ->
-    let (min_ik, max_ik) = Size.range ik in
-    let startv = Ints_t.max x (Ints_t.of_bigint min_ik) in
-    let endv= Ints_t.min y (Ints_t.of_bigint max_ik) in
-
-    let wrap ik (z,o) = 
       let (min_ik, max_ik) = Size.range ik in
-      if isSigned ik then
-        let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (Ints_t.logand Ints_t.one (Ints_t.shift_right z (Size.bit ik - 1)))) in
-        let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (Ints_t.logand Ints_t.one (Ints_t.shift_right o (Size.bit ik - 1)))) in
-        (newz,newo)
-      else
-        let newz = Ints_t.logor z (Ints_t.lognot (Ints_t.of_bigint max_ik)) in
-        let newo = Ints_t.logand o (Ints_t.of_bigint max_ik) in
-        (newz,newo)
+      let startv = Ints_t.max x (Ints_t.of_bigint min_ik) in
+      let endv= Ints_t.min y (Ints_t.of_bigint max_ik) in
+
+      let wrap ik (z,o) = 
+        let (min_ik, max_ik) = Size.range ik in
+        if isSigned ik then
+          let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (Ints_t.logand Ints_t.one (Ints_t.shift_right z (Size.bit ik - 1)))) in
+          let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (Ints_t.logand Ints_t.one (Ints_t.shift_right o (Size.bit ik - 1)))) in
+          (newz,newo)
+        else
+          let newz = Ints_t.logor z (Ints_t.lognot (Ints_t.of_bigint max_ik)) in
+          let newo = Ints_t.logand o (Ints_t.of_bigint max_ik) in
+          (newz,newo)
       in    
-    let rec analyze_bits pos (acc_z, acc_o) =
-      if pos < 0 then (acc_z, acc_o)
-      else
-        let position = Ints_t.shift_left Ints_t.one pos in
-        let mask = Ints_t.sub position Ints_t.one in
-        let remainder = Ints_t.logand startv mask in
-
-        let without_remainder = Ints_t.sub startv remainder in
-        let bigger_number = Ints_t.add without_remainder position in
-        
-        let bit_status =
-          if Ints_t.compare bigger_number endv <= 0 then
-            `top
-          else 
+      let rec analyze_bits pos (acc_z, acc_o) =
+        if pos < 0 then (acc_z, acc_o)
+        else
+          let position = Ints_t.shift_left Ints_t.one pos in
+          let mask = Ints_t.sub position Ints_t.one in
+          let remainder = Ints_t.logand startv mask in
+
+          let without_remainder = Ints_t.sub startv remainder in
+          let bigger_number = Ints_t.add without_remainder position in
+
+          let bit_status =
+            if Ints_t.compare bigger_number endv <= 0 then
+              `top
+            else 
             if Ints_t.equal (Ints_t.logand (Ints_t.shift_right startv pos) Ints_t.one) Ints_t.one then
               `one
             else
               `zero
-        in
+          in
 
-        let new_acc = 
-          match bit_status with
-          | `top -> (Ints_t.logor position acc_z, Ints_t.logor position acc_o)
-          | `one -> (Ints_t.logand (Ints_t.lognot position) acc_z, Ints_t.logor position acc_o)
-          | `zero -> (Ints_t.logor position acc_z, Ints_t.logand (Ints_t.lognot position) acc_o)
+          let new_acc = 
+            match bit_status with
+            | `top -> (Ints_t.logor position acc_z, Ints_t.logor position acc_o)
+            | `one -> (Ints_t.logand (Ints_t.lognot position) acc_z, Ints_t.logor position acc_o)
+            | `zero -> (Ints_t.logor position acc_z, Ints_t.logand (Ints_t.lognot position) acc_o)
 
-        in 
-        analyze_bits (pos - 1) new_acc
-    in      
-    let result = analyze_bits (Size.bit ik - 1) (Ints_t.zero, Ints_t.zero) in
-    let casted = (Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (fst result)))), Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (snd result))))) 
-    in wrap ik casted
+          in 
+          analyze_bits (pos - 1) new_acc
+      in      
+      let result = analyze_bits (Size.bit ik - 1) (Ints_t.zero, Ints_t.zero) in
+      let casted = (Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (fst result)))), Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (snd result))))) 
+      in wrap ik casted
 
   let of_bool _ik = function true -> one | false -> zero
   let to_bool (a: t) = match a with
@@ -447,7 +447,7 @@ struct
     let refn = refine_with_congruence ik x y in
     if M.tracing then M.trace "refine" "int_refine_with_congruence %a %a -> %a" pretty x pretty y pretty refn;
     refn
-    
+
   let refine_with_bitfield ik a b = 
     let interv = of_bitfield ik b in 
     meet ik a interv