Addresses Julien's review no.1:

 - Date format in Changelog
 - No code generation in the original project
 - \valid_read(&(t.j) + (1..3)) is valid
 - addresses -> pointers

src/plugins/e-acsl/doc/Changelog

@@ -19,9 +19,9 @@
 #   configure	configure
 ###############################################################################
 
-*  E-ACSL       [2018/02/10] Fix bug #2305 about taking the address of a
+*  E-ACSL       [2018/10/02] Fix bug #2305 about taking the address of a
                 bitfield.
--  E-ACSL       [2018/18/09] Support for ranges in memory builtins
+-  E-ACSL       [2018/09/18] Support for ranges in memory builtins
                 (\valid, \initialized, etc).
 
 ###############################

src/plugins/e-acsl/misc.ml

@@ -272,8 +272,8 @@ let is_range_free t =
   with Range_found_exception ->
     false
 
-let is_bitfield_address_or_set lty =
-  let is_bitfield_address = function
+let is_bitfield_pointers lty =
+  let is_bitfield_pointer = function
     | Ctype typ ->
       begin match Cil.unrollType typ with
         | TPtr(typ, _) ->
@@ -286,9 +286,9 @@ let is_bitfield_address_or_set lty =
       false
   in
   if Logic_const.is_set_type lty then
-    is_bitfield_address (Logic_const.type_of_element lty)
+    is_bitfield_pointer (Logic_const.type_of_element lty)
   else
-    is_bitfield_address lty
+    is_bitfield_pointer lty
 
 (*
 Local Variables:

src/plugins/e-acsl/misc.mli

@@ -110,9 +110,9 @@ 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. *)
+val is_bitfield_pointers: logic_type -> bool
+(* Returns [true] iff the given logic type is a bitfield pointer or a
+   set of bitfield pointer. *)
 
 (*
 Local Variables:

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

@@ -17,7 +17,7 @@ int test(struct bitfields *a)
 int main(int argc, char **argv)
 {
   //@ assert \valid_read(&(t.j));
-  //@ assert !\valid_read(&(t.j) + (1..3));
+  //@ assert \valid_read(&(t.j) + (1..3));
   t.j = 1;
   //@ assert \initialized(&(t.j));
   return test(&t);

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.
+  E-ACSL construct `bitfield pointer' 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.
+  E-ACSL construct `bitfield pointer' 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.
+  E-ACSL construct `bitfield pointer' 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

@@ -26,7 +26,7 @@ int main(int argc, char **argv)
   __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)); */ ;
+  /*@ assert \valid_read(&t.j + (1 .. 3)); */ ;
   ;
   t.j = (_Bool)1;
   /*@ assert \initialized(&t.j); */ ;

src/plugins/e-acsl/translate.ml

@@ -725,8 +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";
+  if Misc.is_bitfield_pointers t.term_type then
+    not_yet env "bitfield pointer";
   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

@@ -747,7 +747,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
         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 ()
+          if Cil.isBitfield lv then Project.on prj Cil.mkEmptyStmt ()
           else Project.on prj (Misc.mk_initialize ~loc) lv
         in
         let env = Env.add_stmt ~post ~before env new_stmt in