Taking the address of a bitfield raises not_yet.

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

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"

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"

src/plugins/e-acsl/tests/bts/bts2305.c

+/* 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

src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle

+[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).

src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c

+/* 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;
+}
+
+

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

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