Merge pull request diffblue#222 from diffblue/issue202-bitfields-enums

Add support for bit field and enums intervals.cpp

Author: chrisr-diffblue

regression/goto-analyzer/variable-sensitivity-bit-field-intervals/main.c

@@ -0,0 +1,14 @@
+struct bitfield_struct {
+  unsigned char byte;
+  unsigned char bitfield:1;
+};
+
+extern struct bitfield_struct bs;
+
+void main(void)
+{
+  bs.byte = 10;
+  bs.bitfield = 1;
+  __CPROVER_assert(bs.byte==10, "bs.byte==10");
+  __CPROVER_assert(bs.bitfield==1, "bs.bitfield==1");
+}

regression/goto-analyzer/variable-sensitivity-bit-field-intervals/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function main --variable --structs --interval-values --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] .* bs\.byte==10: Success
+\[main\.assertion\.2\] .* bs\.bitfield==1: Success
+--

src/util/interval.cpp

@@ -1127,17 +1127,20 @@ bool constant_interval_exprt::is_float(const constant_interval_exprt &interval)
 bool constant_interval_exprt::is_bitvector(const typet &t)
 {
   return t.id() == ID_bv || t.id() == ID_signedbv || t.id() == ID_unsignedbv
-    || t.id() == ID_c_bool;
+    || t.id() == ID_c_bool
+    || (t.id() == ID_c_bit_field && is_bitvector(t.subtype()));
 }
 
 bool constant_interval_exprt::is_signed(const typet &t)
 {
-  return t.id() == ID_signedbv;
+  return t.id() == ID_signedbv
+    || (t.id() == ID_c_bit_field && is_signed(t.subtype()));
 }
 
 bool constant_interval_exprt::is_unsigned(const typet &t)
 {
-  return t.id() == ID_bv || t.id() == ID_unsignedbv || t.id() == ID_c_bool;
+  return t.id() == ID_bv || t.id() == ID_unsignedbv || t.id() == ID_c_bool
+    || t.id() == ID_c_enum || (t.id() == ID_c_bit_field && is_unsigned(t.subtype()));
 }
 
 bool constant_interval_exprt::is_signed(const constant_interval_exprt &interval)