From 1374b94f71db4cbfe1c55c649682cb1dab29fd37 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 21 Jun 2013 13:20:45 +0000
Subject: [PATCH] [E-ACSL] still fewer unknown locations
---
src/plugins/e-acsl/mpz.ml | 3 +--
.../tests/e-acsl-runtime/oracle/bts1324.1.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/bts1324.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/bts1390.1.res.oracle | 3 ++-
.../tests/e-acsl-runtime/oracle/bts1390.res.oracle | 3 ++-
.../e-acsl-runtime/oracle/linear_search.1.res.oracle | 3 ++-
.../tests/e-acsl-runtime/oracle/linear_search.res.oracle | 3 ++-
src/plugins/e-acsl/translate.ml | 9 ++++++---
8 files changed, 17 insertions(+), 11 deletions(-)
diff --git a/src/plugins/e-acsl/mpz.ml b/src/plugins/e-acsl/mpz.ml
index c55a6d9d97e..a9c5a530c7e 100644
--- a/src/plugins/e-acsl/mpz.ml
+++ b/src/plugins/e-acsl/mpz.ml
@@ -21,7 +21,6 @@
(**************************************************************************)
open Cil_types
-open Cil_datatype
let t_torig_ref =
ref
@@ -59,7 +58,7 @@ let get_set_suffix_and_arg e =
| TPtr(TInt(IChar, _), _) ->
"_str",
(* decimal base for the number given as string *)
- [ e; Cil.integer ~loc:Location.unknown 10 ]
+ [ e; Cil.integer ~loc:e.eloc 10 ]
| _ -> assert false
let generic_affect ~loc fname lv ev e =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
index 31bf99c6e3c..dd3522b0651 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
@@ -34,7 +34,7 @@ share/e-acsl/e_acsl_gmp.h:91:[value] Function __gmpz_set: precondition got statu
share/e-acsl/e_acsl_gmp.h:92:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_clear
share/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/bts1324.i:8:[value] entering loop for the first time
[value] using specification for function __gmpz_cmp
share/e-acsl/e_acsl_gmp.h:124:[value] Function __gmpz_cmp: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
index 7315d054464..243cae07889 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
@@ -16,7 +16,7 @@
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __initialize
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/bts1324.i:8:[value] entering loop for the first time
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
index 95b2d0a49d8..633eebb1b80 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
@@ -18,10 +18,11 @@
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __literal_string
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/bts1390.c:15:[value] entering loop for the first time
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/bts1390.c:11:[value] entering loop for the first time
tests/e-acsl-runtime/bts1390.c:20:[value] entering loop for the first time
[value] using specification for function __delete_block
tests/e-acsl-runtime/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
index 7fbf952e57a..121482b5954 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
@@ -33,7 +33,7 @@ share/e-acsl/e_acsl_gmp.h:91:[value] Function __gmpz_set: precondition got statu
share/e-acsl/e_acsl_gmp.h:92:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_clear
share/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/bts1390.c:15:[value] entering loop for the first time
[value] using specification for function __gmpz_init_set_ui
share/e-acsl/e_acsl_gmp.h:53:[value] Function __gmpz_init_set_ui: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: postcondition got status valid.
@@ -48,6 +48,7 @@ tests/e-acsl-runtime/bts1390.c:15:[kernel] warning: out of bounds read. assert \
share/e-acsl/e_acsl_gmp.h:140:[value] Function __gmpz_add: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:141:[value] Function __gmpz_add: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:142:[value] Function __gmpz_add: precondition got status valid.
+tests/e-acsl-runtime/bts1390.c:11:[value] entering loop for the first time
tests/e-acsl-runtime/bts1390.c:11:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_i_2);
tests/e-acsl-runtime/bts1390.c:20:[value] entering loop for the first time
[value] using specification for function __delete_block
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index 8a4630fea36..28ec7679cbd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -48,8 +48,9 @@ share/e-acsl/e_acsl_gmp.h:142:[value] Function __gmpz_add: precondition got stat
tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_3 < 10;
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/linear_search.i:14:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:14:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_j_4 < 10;
+tests/e-acsl-runtime/linear_search.i:11:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:11:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_j_2 < 10;
tests/e-acsl-runtime/linear_search.i:9:[value] Function search: precondition got status unknown.
tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
index a3216aea63e..94d7fda7d4d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
@@ -22,7 +22,8 @@ tests/e-acsl-runtime/linear_search.i:9:[value] entering loop for the first time
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/linear_search.i:14:[value] entering loop for the first time
+tests/e-acsl-runtime/linear_search.i:11:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:9:[value] Function search: precondition got status unknown.
tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index c7f6447d64a..78d76d732ac 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -581,9 +581,9 @@ and named_predicate_content_to_exp ?name kf env p =
| Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p
| Pat(p, LogicLabel(_, label)) when label = "Here" ->
named_predicate_to_exp kf env p
- | Pat(p, label) ->
+ | Pat(p', label) ->
(* convert [t'] to [e] in a separated local env *)
- let e, env = named_predicate_to_exp kf (Env.push env) p in
+ let e, env = named_predicate_to_exp kf (Env.push env) p' in
let e, env, is_string = at_to_exp env None label e in
assert (not is_string);
e, env
@@ -693,7 +693,10 @@ let predicate_to_exp kf p =
let assumes_predicate bhv =
List.fold_left
- (fun acc p -> Logic_const.pand (acc, Logic_const.unamed p.ip_content))
+ (fun acc p ->
+ Logic_const.pand
+ ~loc:p.ip_loc
+ (acc, Logic_const.unamed ~loc:p.ip_loc p.ip_content))
Logic_const.ptrue
bhv.b_assumes
--
GitLab