From 0cc16dc5abc2d4498c9c0724fd2756db14db551d Mon Sep 17 00:00:00 2001 From: leon Date: Thu, 19 Dec 2024 15:51:42 +0100 Subject: [PATCH 1/2] added regression test --- src/cdomain/value/util/precisionUtil.ml | 5 ++- tests/regression/82-bitfield/12-precision.c | 47 +++++++++++++++++++++ 2 files changed, 50 insertions(+), 2 deletions(-) create mode 100644 tests/regression/82-bitfield/12-precision.c diff --git a/src/cdomain/value/util/precisionUtil.ml b/src/cdomain/value/util/precisionUtil.ml index 9f27f810c7..b226931be9 100644 --- a/src/cdomain/value/util/precisionUtil.ml +++ b/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) diff --git a/tests/regression/82-bitfield/12-precision.c b/tests/regression/82-bitfield/12-precision.c new file mode 100644 index 0000000000..8e97a4dd7e --- /dev/null +++ b/tests/regression/82-bitfield/12-precision.c @@ -0,0 +1,47 @@ +// PARAM: --enable ana.int.bitfield --enable annotation.int.enabled +#include + +#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 +} \ No newline at end of file From 65237fdea577306033e3260822783d4075c82810 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Adrian=20Krau=C3=9F?= Date: Thu, 19 Dec 2024 22:26:41 +0100 Subject: [PATCH 2/2] fixed overflow handling --- src/cdomain/value/cdomains/int/bitfieldDomain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/int/bitfieldDomain.ml b/src/cdomain/value/cdomains/int/bitfieldDomain.ml index d0c65284fd..bf4529b74e 100644 --- a/src/cdomain/value/cdomains/int/bitfieldDomain.ml +++ b/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