diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 3a70cdfe5a9d5994c6106887b1ed4a8f3109199b..7ad73f832471302aaa5429da83ded1e6e548f3a1 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,8 +19,10 @@
# configure configure
###############################################################################
+* E-ACSL [2018/02/10] Fix bug #2305 about taking the address of a
+ bitfield.
- E-ACSL [2018/18/09] Support for ranges in memory builtins
- (\valid, \initialized, etc).
+ (\valid, \initialized, etc).
###############################
Plugin E-ACSL Chlorine-20180501
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 02077223ffe4f9dac32cb37080ef121c0530f1dd..8b00ea543fc8c1c30d0d304f6b79756a044e1993 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -272,6 +272,24 @@ let is_range_free t =
with Range_found_exception ->
false
+let is_bitfield_address_or_set lty =
+ let is_bitfield_address = function
+ | Ctype typ ->
+ begin match Cil.unrollType typ with
+ | TPtr(typ, _) ->
+ let attrs = Cil.typeAttrs typ in
+ Cil.hasAttribute Cil.bitfield_attribute_name attrs
+ | _ ->
+ false
+ end
+ | Ltype _ | Lvar _ | Linteger | Lreal | Larrow _ ->
+ false
+ in
+ if Logic_const.is_set_type lty then
+ is_bitfield_address (Logic_const.type_of_element lty)
+ else
+ is_bitfield_address lty
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 55a5619f2e3499b44587f05a992cc5dc00abf5fc..b69763676e8660adca8c117b157b377bd7137d31 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -110,6 +110,10 @@ val is_set_of_ptr_or_array: logic_type -> bool
val is_range_free: term -> bool
(* Returns [true] iff the given term does not contain any range. *)
+val is_bitfield_address_or_set: logic_type -> bool
+(* Returns [true] iff the given logic type is a bitfield address or a
+ set of bitfield addresses. *)
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/tests/bts/bts2305.c b/src/plugins/e-acsl/tests/bts/bts2305.c
new file mode 100644
index 0000000000000000000000000000000000000000..5dc705eef4732938fe4c2d3e301b37346a2f0481
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/bts2305.c
@@ -0,0 +1,24 @@
+/* run.config
+ COMMENT: bts #2252, taking the address of a bitfield
+*/
+
+#include <stdbool.h>
+
+struct bitfields {
+ int i : 2;
+ bool j : 1;
+} t;
+
+int test(struct bitfields *a)
+{
+ return a->i;
+}
+
+int main(int argc, char **argv)
+{
+ //@ assert \valid_read(&(t.j));
+ //@ assert !\valid_read(&(t.j) + (1..3));
+ t.j = 1;
+ //@ assert \initialized(&(t.j));
+ return test(&t);
+}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..430b73e16abddab92c651cc2f24fddfaba318200
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle
@@ -0,0 +1,13 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/bts/bts2305.c:19: Warning:
+ E-ACSL construct `taking the address of a bitfield' is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/bts/bts2305.c:20: Warning:
+ E-ACSL construct `taking the address of a bitfield' is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/bts/bts2305.c:22: Warning:
+ E-ACSL construct `taking the address of a bitfield' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/bts2305.c:20: Warning:
+ assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
new file mode 100644
index 0000000000000000000000000000000000000000..ab38704551e45937180f4095e829b61ac28e61ff
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
@@ -0,0 +1,39 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+struct bitfields {
+ int i : 2 ;
+ _Bool j : 1 ;
+};
+struct bitfields t;
+int test(struct bitfields *a)
+{
+ int __retres;
+ __retres = (int)a->i;
+ return __retres;
+}
+
+void __e_acsl_globals_init(void)
+{
+ __e_acsl_store_block((void *)(& t),(size_t)4);
+ __e_acsl_full_init((void *)(& t));
+ return;
+}
+
+int main(int argc, char **argv)
+{
+ int tmp;
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
+ __e_acsl_globals_init();
+ /*@ assert \valid_read(&t.j); */ ;
+ /*@ assert ¬\valid_read(&t.j + (1 .. 3)); */ ;
+ ;
+ t.j = (_Bool)1;
+ /*@ assert \initialized(&t.j); */ ;
+ tmp = test(& t);
+ __e_acsl_delete_block((void *)(& t));
+ __e_acsl_memory_clean();
+ return tmp;
+}
+
+
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index fa284c4c66fbc83453c2aacf961038ee015f27fd..e400fe0e9b20872756e256be0c1fdcf755171989 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -725,6 +725,8 @@ and mmodel_call_valid ~loc kf name ctx env t =
B: [\valid(&t[4][3..5][2])]
NON-contiguous locations -> multiple calls (3) to [__e_acsl_valid] *)
and mmodel_call_with_ranges ~loc kf name ctx env t mmodel_call_default =
+ if Misc.is_bitfield_address_or_set t.term_type then
+ not_yet env "taking the address of a bitfield";
match t.term_node with
| TBinOp((PlusPI | IndexPI), p, ({ term_node = Trange _ } as r)) ->
if Misc.is_set_of_ptr_or_array p.term_type then
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 4152ed586ac940c1681f9742677887ded54225f9..4b1acd83cc070ef19d4e687659dd4b4cb97b37d6 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -744,7 +744,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let must_model = Mmodel_analysis.must_model_lval ~stmt ~kf lv in
if not (may_safely_ignore lv) && must_model then
let before = Cil.mkStmt stmt.skind in
- let new_stmt = Project.on prj (Misc.mk_initialize ~loc) lv in
+ let new_stmt =
+ (* Bitfields are not yet supported ==> no initializer.
+ A not_yet will be raised in [Translate]. *)
+ if Cil.isBitfield lv then Cil.mkEmptyStmt ()
+ else Project.on prj (Misc.mk_initialize ~loc) lv
+ in
let env = Env.add_stmt ~post ~before env new_stmt in
let env = match vi with
| None -> env