From eea1572c53d6c67cb6b85bdf81c9cb58120cdf79 Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Tue, 2 Oct 2018 15:39:58 +0200
Subject: [PATCH] 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 | 4 ++--
src/plugins/e-acsl/misc.ml | 8 ++++----
src/plugins/e-acsl/misc.mli | 6 +++---
src/plugins/e-acsl/tests/bts/bts2305.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle | 8 +++-----
src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c | 2 +-
src/plugins/e-acsl/translate.ml | 4 ++--
src/plugins/e-acsl/visit.ml | 2 +-
8 files changed, 17 insertions(+), 19 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 7ad73f83247..21e6f600370 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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).
###############################
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 8b00ea543fc..1b48696679d 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/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:
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index b69763676e8..1991c5afaa9 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/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:
diff --git a/src/plugins/e-acsl/tests/bts/bts2305.c b/src/plugins/e-acsl/tests/bts/bts2305.c
index 5dc705eef47..968fa232b49 100644
--- a/src/plugins/e-acsl/tests/bts/bts2305.c
+++ b/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);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle
index 430b73e16ab..d005b10c5ba 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle
@@ -1,13 +1,11 @@
[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).
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
index ab38704551e..9656f74f512 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
+++ b/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); */ ;
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index e400fe0e9b2..4510c8f3fdf 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/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
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 4b1acd83cc0..68fed778652 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/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
--
GitLab