[eacsl:tests] Add tests for bitwise operators

src/plugins/e-acsl/tests/arith/bitwise.c

+/* run.config_ci, run.config_dev
+   COMMENT: Support of bitwise operations
+   STDOPT: #"-warn-right-shift-negative -warn-left-shift-negative"
+*/
+
+#include <limits.h>
+
+// Operations on signed C integers
+void f_signed(int a, int b) {
+    int c = a << 2;
+    /*@ assert c == (a<<2); */
+    int d = b >> 2;
+    /*@ assert d == (b>>2); */
+    int e = a | b;
+    /*@ assert e == (a | b); */
+    int f = a & b;
+    /*@ assert f == (a & b); */
+    int g = a ^ b;
+    /*@ assert g == (a ^ b); */
+}
+
+// Operations on unsigned C integers
+void f_unsigned(unsigned int a, unsigned int b) {
+    unsigned int c = a << 2u;
+    /*@ assert c == (a<<2); */
+    unsigned int d = b >> 2u;
+    /*@ assert d == (b>>2); */
+    unsigned int e = a | b;
+    /*@ assert e == (a | b); */
+    unsigned int f = a & b;
+    /*@ assert f == (a & b); */
+    unsigned int g = a ^ b;
+    /*@ assert g == (a ^ b); */
+}
+
+// Operations on arbitrary precision signed integers
+void g_signed(int a, int b) {
+    int c = a << b;
+    /*@ assert c == (a<<b); */
+    int d = a >> b;
+    /*@ assert d == (a>>b); */
+
+    /*@ assert ((ULLONG_MAX + 1) << 1) != 0; */
+    /*@ assert ((ULLONG_MAX + 1) >> 1) != 0; */
+    /*@ assert ((LLONG_MIN - 1) << 1) != 0; */
+    /*@ assert ((LLONG_MIN - 1) >> 1) != 0; */
+    /*@ assert (1 << 65) != 0; */
+    /*@ assert ((ULLONG_MAX + 1) | (LLONG_MIN - 1)) != 0; */
+    /*@ assert ((ULLONG_MAX + 1) & (LLONG_MIN - 1)) !=
+               ((ULLONG_MAX + 1) ^ (LLONG_MIN - 1)); */
+}
+
+// Operations on arbitrary precision unsigned integers
+void g_unsigned(unsigned int a, unsigned int b) {
+    unsigned int c = a << b;
+    /*@ assert c == (a<<b); */
+    unsigned int d = a >> b;
+    /*@ assert d == (a>>b); */
+
+    /*@ assert ((ULLONG_MAX + 1u) << 1u) != 0; */
+    /*@ assert ((ULLONG_MAX + 1u) >> 1u) != 0; */
+    /*@ assert (1u << 65u) != 0; */
+    /*@ assert ((ULLONG_MAX + 1u) | 1u) != 0; */
+    /*@ assert ((ULLONG_MAX + 1u) & 1u) !=
+               ((ULLONG_MAX + 1u) ^ 1u); */
+}
+
+int main() {
+    int a = 4;
+    int b = 8;
+    f_signed(a,b);
+    f_unsigned(a,b);
+    g_signed(a,b);
+    g_unsigned(a,b);
+    return 0;
+}

src/plugins/e-acsl/tests/arith/oracle_ci/bitwise.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] tests/arith/bitwise.c:39: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:41: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:43: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:44: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:45: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:46: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:47: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:48: Warning: 
+  E-ACSL construct `bitwise operator on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:49: Warning: 
+  E-ACSL construct `bitwise operator on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:56: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:58: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:60: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:61: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:62: Warning: 
+  E-ACSL construct `left/right shift on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:63: Warning: 
+  E-ACSL construct `bitwise operator on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/arith/bitwise.c:64: Warning: 
+  E-ACSL construct `bitwise operator on arbitrary precision'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/arith/oracle_ci/gen_bitwise.c

+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+void f_signed(int a, int b)
+{
+  int c = a << 2;
+  __e_acsl_assert(0 <= a,"RTE","f_signed","shift: 0 <= a",
+                  "tests/arith/bitwise.c",11);
+  __e_acsl_assert((long)c == a << 2L,"Assertion","f_signed","c == a << 2",
+                  "tests/arith/bitwise.c",11);
+  /*@ assert c ≡ a << 2; */ ;
+  int d = b >> 2;
+  __e_acsl_assert(0 <= b,"RTE","f_signed","shift: 0 <= b",
+                  "tests/arith/bitwise.c",13);
+  __e_acsl_assert(d == b >> 2,"Assertion","f_signed","d == b >> 2",
+                  "tests/arith/bitwise.c",13);
+  /*@ assert d ≡ b >> 2; */ ;
+  int e = a | b;
+  __e_acsl_assert((long)e == (a | (long)b),"Assertion","f_signed",
+                  "e == (a | b)","tests/arith/bitwise.c",15);
+  /*@ assert e ≡ (a | b); */ ;
+  int f = a & b;
+  __e_acsl_assert((long)f == (a & (long)b),"Assertion","f_signed",
+                  "f == (a & b)","tests/arith/bitwise.c",17);
+  /*@ assert f ≡ (a & b); */ ;
+  int g = a ^ b;
+  __e_acsl_assert((long)g == (a ^ (long)b),"Assertion","f_signed",
+                  "g == (a ^ b)","tests/arith/bitwise.c",19);
+  /*@ assert g ≡ (a ^ b); */ ;
+  return;
+}
+
+void f_unsigned(unsigned int a, unsigned int b)
+{
+  unsigned int c = a << 2u;
+  __e_acsl_assert((unsigned long)c == a << 2UL,"Assertion","f_unsigned",
+                  "c == a << 2","tests/arith/bitwise.c",25);
+  /*@ assert c ≡ a << 2; */ ;
+  unsigned int d = b >> 2u;
+  __e_acsl_assert(d == b >> 2U,"Assertion","f_unsigned","d == b >> 2",
+                  "tests/arith/bitwise.c",27);
+  /*@ assert d ≡ b >> 2; */ ;
+  unsigned int e = a | b;
+  __e_acsl_assert(e == (a | b),"Assertion","f_unsigned","e == (a | b)",
+                  "tests/arith/bitwise.c",29);
+  /*@ assert e ≡ (a | b); */ ;
+  unsigned int f = a & b;
+  __e_acsl_assert(f == (a & b),"Assertion","f_unsigned","f == (a & b)",
+                  "tests/arith/bitwise.c",31);
+  /*@ assert f ≡ (a & b); */ ;
+  unsigned int g = a ^ b;
+  __e_acsl_assert(g == (a ^ b),"Assertion","f_unsigned","g == (a ^ b)",
+                  "tests/arith/bitwise.c",33);
+  /*@ assert g ≡ (a ^ b); */ ;
+  return;
+}
+
+void g_signed(int a, int b)
+{
+  int c = a << b;
+  /*@ assert c ≡ a << b; */ ;
+  int d = a >> b;
+  /*@ assert d ≡ a >> b; */ ;
+  /*@ assert (18446744073709551615ULL + 1) << 1 ≢ 0; */ ;
+  /*@ assert (18446744073709551615ULL + 1) >> 1 ≢ 0; */ ;
+  /*@ assert ((-9223372036854775807LL - 1LL) - 1) << 1 ≢ 0; */ ;
+  /*@ assert ((-9223372036854775807LL - 1LL) - 1) >> 1 ≢ 0; */ ;
+  /*@ assert 1 << 65 ≢ 0; */ ;
+  /*@
+  assert
+  ((18446744073709551615ULL + 1) | ((-9223372036854775807LL - 1LL) - 1)) ≢
+  0; */
+  ;
+  /*@
+  assert
+  ((18446744073709551615ULL + 1) & ((-9223372036854775807LL - 1LL) - 1)) ≢
+  ((18446744073709551615ULL + 1) ^ ((-9223372036854775807LL - 1LL) - 1)); */
+  ;
+  return;
+}
+
+void g_unsigned(unsigned int a, unsigned int b)
+{
+  unsigned int c = a << b;
+  /*@ assert c ≡ a << b; */ ;
+  unsigned int d = a >> b;
+  /*@ assert d ≡ a >> b; */ ;
+  /*@ assert (18446744073709551615ULL + 1u) << 1u ≢ 0; */ ;
+  /*@ assert (18446744073709551615ULL + 1u) >> 1u ≢ 0; */ ;
+  /*@ assert 1u << 65u ≢ 0; */ ;
+  /*@ assert ((18446744073709551615ULL + 1u) | 1u) ≢ 0; */ ;
+  /*@
+  assert
+  ((18446744073709551615ULL + 1u) & 1u) ≢
+  ((18446744073709551615ULL + 1u) ^ 1u); */
+  ;
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  int a = 4;
+  int b = 8;
+  f_signed(a,b);
+  f_unsigned((unsigned int)a,(unsigned int)b);
+  g_signed(a,b);
+  g_unsigned((unsigned int)a,(unsigned int)b);
+  __retres = 0;
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle

+[kernel] Parsing tests/arith/bitwise.c (with preprocessing)