diff --git a/src/plugins/e-acsl/tests/arith/bitwise.c b/src/plugins/e-acsl/tests/arith/bitwise.c
new file mode 100644
index 0000000000000000000000000000000000000000..a47aba968c95d5816444f76c1500b325194a644c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/bitwise.c
@@ -0,0 +1,76 @@
+/* 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;
+}
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/bitwise.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/bitwise.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d3656a3e7da8fdc8710c080e25eee4cc81f9efe2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/bitwise.res.oracle
@@ -0,0 +1,66 @@
+[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".
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_bitwise.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_bitwise.c
new file mode 100644
index 0000000000000000000000000000000000000000..7e230971466517b86b4844888116d3dd4359a0ba
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_bitwise.c
@@ -0,0 +1,113 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7a5cede891e1d7fc3175c8f0839ee423771fa84a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/bitwise.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/arith/bitwise.c (with preprocessing)