Merge pull request #26 from ManuelLerchner/precission

added regression test for precission usage

Author: ManuelLerchner

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

@@ -245,7 +245,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
       else 
         (top_of ik, overflow_info)
 
-  let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov t = norm ~suppress_ovwarn t
+  let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov ik x = norm ~suppress_ovwarn:(suppress_ovwarn || x = top ()) ik x
 
   let join ik b1 b2 = (norm ik @@ (BArith.join b1 b2) ) |> fst
 

src/cdomain/value/util/precisionUtil.ml

@@ -1,7 +1,7 @@
 (** Integer and floating-point option and attribute handling. *)
 
 (* We define precision by the number of IntDomains activated.
- * We currently have 5 types: DefExc, Interval, Enums, Congruence, IntervalSet, Bitfield*)
+ * We currently have 6 types: DefExc, Interval, Enums, Congruence, IntervalSet, Bitfield*)
 type int_precision = (bool * bool * bool * bool * bool * bool)
 (* Same applies for FloatDomain
  * We currently have only an interval type analysis *)
@@ -57,7 +57,8 @@ let reset_lazy () =
   enums := None;
   congruence := None;
   interval_set := None;
-  annotation_int_enabled := None
+  annotation_int_enabled := None;
+  bitfield := None
 
 (* Thus for maximum precision we activate all Domains *)
 let max_int_precision : int_precision = (true, true, true, true, true, true)

tests/regression/82-bitfield/12-precision.c

@@ -0,0 +1,47 @@
+// PARAM: --enable ana.int.bitfield --enable annotation.int.enabled
+#include <goblint.h>
+
+#define ANY_ERROR 5  // 0b0101
+void example1(void) __attribute__((goblint_precision("no-bitfield")));
+void example2(void) __attribute__((goblint_precision("bitfield")));
+
+int main() {
+    example1();
+    example2();
+}
+
+void example1(){
+    int state;
+    int r = rand() % 3;
+    switch (r) {
+        case 0:
+        state = 0; /* 0b0000 */
+         break;
+        case 1:
+        state = 8; /* 0b1000 */
+         break;
+        default:
+        state = 10; /* 0b1010 */
+         break;
+  }
+
+  __goblint_check((state & ANY_ERROR) == 0); //UNKNOWN
+}
+
+void example2(){
+    int state;
+    int r = rand() % 3;
+    switch (r) {
+        case 0:
+        state = 0; /* 0b0000 */
+         break;
+        case 1:
+        state = 8; /* 0b1000 */
+         break;
+        default:
+        state = 10; /* 0b1010 */
+         break;
+  }
+
+  __goblint_check((state & ANY_ERROR) == 0); //SUCCESS
+}