diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index e2d8c8d10031e1f2762a5aef1149971d4482c6e2..f162204e1a697ad93d70da5260ab185da4fa0d77 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -71,13 +71,9 @@ let is_empty env = env.var_cpt = 0 && is_empty_block env
let add_stmt env s =
{ env with beginning_of_block = s :: env.beginning_of_block }
-let add_assert s p =
+let add_assert kf s p =
Queue.add
- (fun () ->
- (* Don't work since the kernel_function does not yet exist in the new
- project. Virgile said he was implementing the missing stuff in the
- visitor. Wait and see... *)
- let kf = Kernel_function.find_englobing_kf s in
+ (fun () ->
Annotations.add_assert kf s [ !self ] p)
!queue
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index c48dc52acef0cfedc125a61bcde2ddca0aaa2a4f..e67bdad8e3d69fd4e7ee99efa10ee87ab45e929b 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -60,9 +60,9 @@ val merge_block_vars: from:t -> t -> t
val add_stmt: t -> stmt -> t
(** [add_stmt env s] extends [env] with the new statement [s] *)
-val add_assert: stmt -> predicate named -> unit
- (** [add_assert s p] extends the global environment with an assertion [p]
- associated to the statement [s]. *)
+val add_assert: kernel_function -> stmt -> predicate named -> unit
+ (** [add_assert kf s p] extends the global environment with an assertion [p]
+ associated to the statement [s] in function [kf]. *)
val register_actions_queue: (unit -> unit) Queue.t -> unit
(** To be called once at initialization time: the queue of event of the
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index e1823cd42647abb82fd31b77339c8aa95b8870e3..8c3d2b5d938bfe388b6fe2039b9751ddbf7d51f5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -6,24 +6,24 @@
PROJECT_FILE.i:134:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:136.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
Called from PROJECT_FILE.i:136.
-PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown
+PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status valid.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
Called from PROJECT_FILE.i:137.
-PROJECT_FILE.i:55:[value] Function mpz_neg: precondition got status valid
-PROJECT_FILE.i:56:[value] Function mpz_neg: precondition got status valid
+PROJECT_FILE.i:55:[value] Function mpz_neg: precondition got status valid.
+PROJECT_FILE.i:56:[value] Function mpz_neg: precondition got status valid.
[value] Done for function mpz_neg
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:137.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
Called from PROJECT_FILE.i:138.
-PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
-PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
+PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:139.
@@ -32,13 +32,13 @@ PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:140.
-PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
+PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:140.
@@ -129,9 +129,9 @@ PROJECT_FILE.i:161:[value] Assertion got status valid.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
Called from PROJECT_FILE.i:165.
-PROJECT_FILE.i:60:[value] Function mpz_add: precondition got status valid
-PROJECT_FILE.i:61:[value] Function mpz_add: precondition got status valid
-PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
+PROJECT_FILE.i:60:[value] Function mpz_add: precondition got status valid.
+PROJECT_FILE.i:61:[value] Function mpz_add: precondition got status valid.
+PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid.
[value] Done for function mpz_add
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:165.
@@ -182,9 +182,9 @@ PROJECT_FILE.i:173:[value] Assertion got status valid.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
Called from PROJECT_FILE.i:177.
-PROJECT_FILE.i:66:[value] Function mpz_sub: precondition got status valid
-PROJECT_FILE.i:67:[value] Function mpz_sub: precondition got status valid
-PROJECT_FILE.i:68:[value] Function mpz_sub: precondition got status valid
+PROJECT_FILE.i:66:[value] Function mpz_sub: precondition got status valid.
+PROJECT_FILE.i:67:[value] Function mpz_sub: precondition got status valid.
+PROJECT_FILE.i:68:[value] Function mpz_sub: precondition got status valid.
[value] Done for function mpz_sub
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:177.
@@ -235,9 +235,9 @@ PROJECT_FILE.i:185:[value] Assertion got status valid.
[value] Done for function mpz_init
[value] computing for function mpz_mul <- main.
Called from PROJECT_FILE.i:189.
-PROJECT_FILE.i:72:[value] Function mpz_mul: precondition got status valid
-PROJECT_FILE.i:73:[value] Function mpz_mul: precondition got status valid
-PROJECT_FILE.i:74:[value] Function mpz_mul: precondition got status valid
+PROJECT_FILE.i:72:[value] Function mpz_mul: precondition got status valid.
+PROJECT_FILE.i:73:[value] Function mpz_mul: precondition got status valid.
+PROJECT_FILE.i:74:[value] Function mpz_mul: precondition got status valid.
[value] Done for function mpz_mul
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:189.
@@ -285,7 +285,7 @@ PROJECT_FILE.i:197:[value] Assertion got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_get_si <- main.
Called from PROJECT_FILE.i:201.
-PROJECT_FILE.i:92:[value] Function mpz_get_si: precondition got status valid
+PROJECT_FILE.i:92:[value] Function mpz_get_si: precondition got status valid.
[value] Done for function mpz_get_si
[value] computing for function mpz_init <- main.
Called from PROJECT_FILE.i:201.
@@ -303,9 +303,9 @@ PROJECT_FILE.i:202:[value] Assertion got status valid.
[value] Done for function e_acsl_fail
[value] computing for function mpz_cdiv_q <- main.
Called from PROJECT_FILE.i:204.
-PROJECT_FILE.i:78:[value] Function mpz_cdiv_q: precondition got status valid
-PROJECT_FILE.i:79:[value] Function mpz_cdiv_q: precondition got status valid
-PROJECT_FILE.i:80:[value] Function mpz_cdiv_q: precondition got status valid
+PROJECT_FILE.i:78:[value] Function mpz_cdiv_q: precondition got status valid.
+PROJECT_FILE.i:79:[value] Function mpz_cdiv_q: precondition got status valid.
+PROJECT_FILE.i:80:[value] Function mpz_cdiv_q: precondition got status valid.
[value] Done for function mpz_cdiv_q
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:204.
@@ -347,7 +347,7 @@ PROJECT_FILE.i:80:[value] Function mpz_cdiv_q: precondition got status valid
PROJECT_FILE.i:212:[value] Assertion got status valid.
[value] computing for function mpz_init_set_str <- main.
Called from PROJECT_FILE.i:215.
-PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status unknown
+PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status valid.
[value] Done for function mpz_init_set_str
[value] computing for function mpz_init_set_str <- main.
Called from PROJECT_FILE.i:216.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index d1c35002514a4f04b1feadb5087dc34273b7f029..bc71784ef73faada91cb1de204c3208bf07cbca1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -7,7 +7,7 @@ tests/e-acsl-runtime/cast.i:18:[e-acsl] warning: missing guard for ensuring that
PROJECT_FILE.i:134:[value] Assertion got status valid.
[value] computing for function mpz_init_set_str <- main.
Called from PROJECT_FILE.i:136.
-PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status unknown.
+PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status valid.
[value] Done for function mpz_init_set_str
[value] computing for function mpz_get_si <- main.
Called from PROJECT_FILE.i:137.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index ba903d11580edd9956268f70a40b96e092b4401a..6351bee0d37da771b214486544895fbe4697a9d4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -7,7 +7,7 @@ PROJECT_FILE.i:138:[value] Assertion got status valid.
PROJECT_FILE.i:141:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:143.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown.
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:143.
@@ -62,7 +62,7 @@ PROJECT_FILE.i:149:[value] Assertion got status valid.
Called from PROJECT_FILE.i:154.
[value] Done for function mpz_clear
PROJECT_FILE.i:158:[value] Assertion got status valid.
-PROJECT_FILE.i:161:[value] Assertion got status valid.
+PROJECT_FILE.i:161:[value] Assertion got status unknown.
PROJECT_FILE.i:164:[value] Assertion got status valid.
PROJECT_FILE.i:167:[value] Assertion got status valid.
PROJECT_FILE.i:170:[value] Assertion got status valid.
@@ -75,7 +75,7 @@ PROJECT_FILE.i:182:[value] Assertion got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
Called from PROJECT_FILE.i:184.
-PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown.
+PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status valid.
[value] Done for function mpz_init
[value] computing for function mpz_neg <- main.
Called from PROJECT_FILE.i:185.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index 81ba3e72ab9b4915c53af9910c13d288d78d5692..c1bb930a271214543a3423a69849a928ab21de91 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -20,7 +20,7 @@ PROJECT_FILE.i:144:[value] Function g: postcondition got status valid.
PROJECT_FILE.i:162:[value] Function h: precondition got status valid.
[value] computing for function mpz_init_set_si <- h <- main.
Called from PROJECT_FILE.i:166.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown.
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- h <- main.
Called from PROJECT_FILE.i:166.
@@ -141,7 +141,7 @@ PROJECT_FILE.i:201:[value] Function j, behavior b2: precondition got status vali
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- j <- main.
Called from PROJECT_FILE.i:215.
-PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown.
+PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status valid.
[value] Done for function mpz_init
[value] computing for function mpz_add <- j <- main.
Called from PROJECT_FILE.i:216.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index 4fc2d516e8e7d8b0dd00033bc5e9347e4c5c291a..f9a3f1a52e33456969a998beb17db5e998efce62 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -604,7 +604,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
extern void exit(int status);
void e_acsl_fail(char *msg)
{
- printf((char const *)"%s\n",msg);
+ printf("%s\n",msg);
exit(1);
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
index bee9302fe0a0e28120c3cc646c1d918dba974917..8a2ae8bb12df129df00433026f710476cf409745 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
@@ -559,7 +559,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
extern void exit(int status);
void e_acsl_fail(char *msg)
{
- printf((char const *)"%s\n",msg);
+ printf("%s\n",msg);
exit(1);
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index 3fa5e559ff282dc250e91bfed85c0c33d52c09e6..53a8b0b13bff6474fd5b89ccfbd361635eed5c3f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -598,7 +598,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
extern void exit(int status);
void e_acsl_fail(char *msg)
{
- printf((char const *)"%s\n",msg);
+ printf("%s\n",msg);
exit(1);
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index dd65f0697655184082c19b01fc680d3124de58e1..f6e48bcfecdbc15fafcbc10a995724afe0256218 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -7,7 +7,7 @@ PROJECT_FILE.i:135:[value] Assertion got status valid.
PROJECT_FILE.i:138:[value] Assertion got status valid.
[value] computing for function mpz_init_set_str <- main.
Called from PROJECT_FILE.i:140.
-PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status unknown.
+PROJECT_FILE.i:33:[value] Function mpz_init_set_str: postcondition got status valid.
[value] Done for function mpz_init_set_str
[value] computing for function mpz_init_set_str <- main.
Called from PROJECT_FILE.i:141.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
index c8428bb3abe96cba28552c70023b9074e3d08387..1d54dc22a3546873d78163ce7c5a1b886c3ea9d7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -5,15 +5,15 @@
PROJECT_FILE.i:134:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:136.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:137.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
Called from PROJECT_FILE.i:137.
-PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
-PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
+PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:142.
@@ -27,7 +27,7 @@ PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
PROJECT_FILE.i:145:[value] assigning non deterministic value for the first time
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:146.
-PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
+PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:147.
@@ -39,7 +39,7 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
@@ -62,7 +62,7 @@ PROJECT_FILE.i:153:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:163.
[value] Done for function mpz_init_set_si
-PROJECT_FILE.i:164:[value] Assertion got status invalid (stopping propagation)..
+PROJECT_FILE.i:164:[value] Assertion got status invalid (stopping propagation).
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:174.
[value] Done for function mpz_clear
@@ -123,7 +123,7 @@ PROJECT_FILE.i:196:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:207.
[value] Done for function mpz_init_set_si
-PROJECT_FILE.i:208:[value] Assertion got status invalid (stopping propagation)..
+PROJECT_FILE.i:208:[value] Assertion got status invalid (stopping propagation).
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:217.
[value] Done for function mpz_clear
@@ -184,7 +184,7 @@ PROJECT_FILE.i:239:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:250.
[value] Done for function mpz_init_set_si
-PROJECT_FILE.i:251:[value] Assertion got status invalid (stopping propagation)..
+PROJECT_FILE.i:251:[value] Assertion got status invalid (stopping propagation).
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:260.
[value] Done for function mpz_clear
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
index f0693c50a44cfca3ee84058434500a1c2ed63a79..6f6d95e3edbf2f076fbf00ccb7500f42f4025be4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
@@ -6,7 +6,7 @@ tests/e-acsl-runtime/nested_code_annot.i:12:[kernel] warning: Body of function m
PROJECT_FILE.i:134:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:141.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown.
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:141.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index f0c78ccd69af31f45afce818ac8d934b261df275..e2d48d0b40d8aba6a621513cbd3b67a6473ea780 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -2,11 +2,11 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
-PROJECT_FILE.i:134:[value] Assertion got status valid.
-PROJECT_FILE.i:137:[value] Assertion got status valid.
+PROJECT_FILE.i:134:[value] Assertion got status unknown.
+PROJECT_FILE.i:137:[value] Assertion got status unknown.
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:139.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown.
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:139.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index 612d89375bd59c3ad62cc63a57d674c151abaaf7..7a43b69b087ed77c2b5d1fe10dfff1ad76e9c161 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -17,15 +17,15 @@ tests/e-acsl-runtime/ptr.i:26:[e-acsl] warning: missing guard for ensuring that
PROJECT_FILE.i:138:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:140.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:140.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
Called from PROJECT_FILE.i:141.
-PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid
-PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
+PROJECT_FILE.i:45:[value] Function mpz_cmp: precondition got status valid.
+PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
Called from PROJECT_FILE.i:142.
@@ -34,13 +34,13 @@ PROJECT_FILE.i:46:[value] Function mpz_cmp: precondition got status valid
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:125.
-PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid
+PROJECT_FILE.i:115:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:143.
-PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
+PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:143.
@@ -106,13 +106,13 @@ PROJECT_FILE.i:162:[value] Assertion got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
Called from PROJECT_FILE.i:167.
-PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown
+PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status valid.
[value] Done for function mpz_init
[value] computing for function mpz_mul <- main.
Called from PROJECT_FILE.i:167.
-PROJECT_FILE.i:72:[value] Function mpz_mul: precondition got status valid
-PROJECT_FILE.i:73:[value] Function mpz_mul: precondition got status valid
-PROJECT_FILE.i:74:[value] Function mpz_mul: precondition got status valid
+PROJECT_FILE.i:72:[value] Function mpz_mul: precondition got status valid.
+PROJECT_FILE.i:73:[value] Function mpz_mul: precondition got status valid.
+PROJECT_FILE.i:74:[value] Function mpz_mul: precondition got status valid.
[value] Done for function mpz_mul
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:168.
@@ -139,13 +139,13 @@ PROJECT_FILE.i:170:[value] Assertion got status valid.
[value] Done for function e_acsl_fail
[value] computing for function mpz_cdiv_q <- main.
Called from PROJECT_FILE.i:172.
-PROJECT_FILE.i:78:[value] Function mpz_cdiv_q: precondition got status valid
-PROJECT_FILE.i:79:[value] Function mpz_cdiv_q: precondition got status valid
-PROJECT_FILE.i:80:[value] Function mpz_cdiv_q: precondition got status valid
+PROJECT_FILE.i:78:[value] Function mpz_cdiv_q: precondition got status valid.
+PROJECT_FILE.i:79:[value] Function mpz_cdiv_q: precondition got status valid.
+PROJECT_FILE.i:80:[value] Function mpz_cdiv_q: precondition got status valid.
[value] Done for function mpz_cdiv_q
[value] computing for function mpz_get_si <- main.
Called from PROJECT_FILE.i:173.
-PROJECT_FILE.i:92:[value] Function mpz_get_si: precondition got status valid
+PROJECT_FILE.i:92:[value] Function mpz_get_si: precondition got status valid.
[value] Done for function mpz_get_si
PROJECT_FILE.i:174:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
assert 0 ≤ e_acsl_17 ∧ e_acsl_17 < 3;
@@ -208,9 +208,9 @@ PROJECT_FILE.i:186:[value] Assertion got status valid.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
Called from PROJECT_FILE.i:190.
-PROJECT_FILE.i:60:[value] Function mpz_add: precondition got status valid
-PROJECT_FILE.i:61:[value] Function mpz_add: precondition got status valid
-PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
+PROJECT_FILE.i:60:[value] Function mpz_add: precondition got status valid.
+PROJECT_FILE.i:61:[value] Function mpz_add: precondition got status valid.
+PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid.
[value] Done for function mpz_add
[value] computing for function mpz_cmp <- main.
Called from PROJECT_FILE.i:191.
@@ -249,9 +249,9 @@ PROJECT_FILE.i:197:[value] Assertion got status valid.
[value] Done for function mpz_init
[value] computing for function mpz_sub <- main.
Called from PROJECT_FILE.i:202.
-PROJECT_FILE.i:66:[value] Function mpz_sub: precondition got status valid
-PROJECT_FILE.i:67:[value] Function mpz_sub: precondition got status valid
-PROJECT_FILE.i:68:[value] Function mpz_sub: precondition got status valid
+PROJECT_FILE.i:66:[value] Function mpz_sub: precondition got status valid.
+PROJECT_FILE.i:67:[value] Function mpz_sub: precondition got status valid.
+PROJECT_FILE.i:68:[value] Function mpz_sub: precondition got status valid.
[value] Done for function mpz_sub
[value] computing for function mpz_get_si <- main.
Called from PROJECT_FILE.i:203.
@@ -405,6 +405,7 @@ PROJECT_FILE.i:197:[value] Assertion got status unknown.
[value] computing for function mpz_get_si <- main.
Called from PROJECT_FILE.i:203.
[value] Done for function mpz_get_si
+PROJECT_FILE.i:204:[value] Assertion got status unknown.
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:204.
[value] Done for function mpz_init_set_si
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index e0448b250d0a9f46ad7aceb731ad9df34efa8752..723f3b5095d64432f85d58b609dc1175c2430e2b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -5,7 +5,7 @@
PROJECT_FILE.i:131:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:133.
-PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status unknown.
+PROJECT_FILE.i:29:[value] Function mpz_init_set_si: postcondition got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
Called from PROJECT_FILE.i:133.
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 52fc32115d6ad793cfb20112a5affc7278b3d765..2fc97d1856d4b509d72a7283e4fdf0139bbe50b0 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -141,60 +141,60 @@ let constant_to_exp ?(loc=Location.unknown) = function
| CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _ as c ->
new_exp ?loc (Const c), false
-let rec thost_to_host env = function
+let rec thost_to_host kf env = function
| TVar { lv_origin = Some v } -> Var v, env
| TVar { lv_origin = None } -> Misc.not_yet "logic variable"
| TResult _typ -> Misc.not_yet "\\result"
| TMem t ->
- let e, env = term_to_exp env (Ctype intType) t in
+ let e, env = term_to_exp kf env (Ctype intType) t in
Options.warning ~source:(fst e.eloc) ~once:true
"missing guard for ensuring that %a is a valid memory access"
d_term t;
Mem e, env
-and toffset_to_offset ?loc env = function
+and toffset_to_offset ?loc kf env = function
| TNoOffset -> NoOffset, env
| TField(f, offset) ->
(* TODO: still untested *)
- let offset, env = toffset_to_offset ?loc env offset in
+ let offset, env = toffset_to_offset ?loc kf env offset in
Field(f, offset), env
| TIndex(t, offset) ->
- let e, env = term_to_exp env (Ctype intType) t in
+ let e, env = term_to_exp kf env (Ctype intType) t in
Options.warning ~source:(fst e.eloc) ~once:true
"missing guard for ensuring that %a is a valid array index"
d_term t;
- let offset, env = toffset_to_offset env offset in
+ let offset, env = toffset_to_offset kf env offset in
Index(e, offset), env
-and tlval_to_lval env (host, offset) =
- let host, env = thost_to_host env host in
- let offset, env = toffset_to_offset env offset in
+and tlval_to_lval kf env (host, offset) =
+ let host, env = thost_to_host kf env host in
+ let offset, env = toffset_to_offset kf env offset in
(host, offset), env
-and context_insensitive_term_to_exp env t =
+and context_insensitive_term_to_exp kf env t =
let loc = t.term_loc in
match t.term_node with
| TConst c ->
let c, is_mpz_string = constant_to_exp ~loc c in
c, env, is_mpz_string
| TLval lv ->
- let lv, env = tlval_to_lval env lv in
+ let lv, env = tlval_to_lval kf env lv in
new_exp ~loc (Lval lv), env, false
| TSizeOf ty -> sizeOf ~loc ty, env, false
| TSizeOfE t ->
let ty = t.term_type in
assert (match ty with Ctype _ -> true | _ -> false);
- let e, env = term_to_exp env ty t in
+ let e, env = term_to_exp kf env ty t in
sizeOf ~loc (typeOf e), env, false
| TSizeOfStr s -> new_exp ~loc (SizeOfStr s), env, false
| TAlignOf ty -> new_exp ~loc (AlignOf ty), env, false
| TAlignOfE t ->
let ty = t.term_type in
assert (match ty with Ctype _ -> true | _ -> false);
- let e, env = term_to_exp env ty t in
+ let e, env = term_to_exp kf env ty t in
new_exp ~loc (AlignOfE e), env, false
| TUnOp(Neg | BNot as op, t) ->
- let e, env = term_to_exp env Linteger t in
+ let e, env = term_to_exp kf env Linteger t in
let name = match op with
| Neg -> "mpz_neg"
| BNot -> "mpz_com"
@@ -208,7 +208,7 @@ and context_insensitive_term_to_exp env t =
e, env, false
| TUnOp(LNot, t) ->
let ty = t.term_type in
- let e, env = term_to_exp env ty t in
+ let e, env = term_to_exp kf env ty t in
(* TODO: preserve the old behavior. But that is incorrect if [t] is an
integer since we have to implement a ! over mpz values.
Such a case is actually possible. *)
@@ -216,8 +216,8 @@ and context_insensitive_term_to_exp env t =
new_exp ~loc (UnOp(LNot, e, intType)), env, false
| TBinOp(PlusA | MinusA | Mult as bop, t1, t2) ->
(* arithmetic binary operator not safely convertible into C *)
- let e1, env = term_to_exp env Linteger t1 in
- let e2, env = term_to_exp env Linteger t2 in
+ let e1, env = term_to_exp kf env Linteger t1 in
+ let e2, env = term_to_exp kf env Linteger t2 in
assert (Typ.equal (typeOf e1) (typeOf e2));
let name = name_of_mpz_arith_bop bop in
let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
@@ -226,18 +226,18 @@ and context_insensitive_term_to_exp env t =
| TBinOp(Div | Mod as bop, t1, t2) ->
(* arithmetic binary operator potentially convertible into C *)
let ctx = principal_type_from_term t1 t2 in
- let e1, env = term_to_exp env ctx t1 in
- let e2, env = term_to_exp env ctx t2 in
+ let e1, env = term_to_exp kf env ctx t1 in
+ let e2, env = term_to_exp kf env ctx t2 in
(* guarding divisions and modulos *)
let zero = Logic_const.tinteger ~ikind:IInt 0 in
(* do not generate [e2] from [t2] twice *)
- let guard, env = comparison_to_exp env ~e1:(e2, ctx) Eq t2 zero in
+ let guard, env = comparison_to_exp kf env ~e1:(e2, ctx) Eq t2 zero in
let mk_stmts v e =
let name = name_of_mpz_arith_bop bop in
let cond =
Misc.mk_e_acsl_guard guard (Logic_const.prel (Req, t2, zero))
in
- Env.add_assert cond (Logic_const.prel (Rneq, t2, zero));
+ Env.add_assert kf cond (Logic_const.prel (Rneq, t2, zero));
let instr = match ctx with
| Ctype ty when isIntegralType ty ->
let e = new_exp ~loc (BinOp(bop, e1, e2, ty)) in
@@ -255,7 +255,7 @@ and context_insensitive_term_to_exp env t =
e, env, false
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
- let e, env = comparison_to_exp ~loc env bop t1 t2 in
+ let e, env = comparison_to_exp ~loc kf env bop t1 t2 in
e, env, false
| TBinOp((Shiftlt | Shiftrt), _, _) ->
(* left/right shift *)
@@ -272,8 +272,8 @@ and context_insensitive_term_to_exp env t =
Ctype intType
| ty -> ty
in
- let e1, env = term_to_exp env (ctx_type t1) t1 in
- let e2, env = term_to_exp env (ctx_type t2) t2 in
+ let e1, env = term_to_exp kf env (ctx_type t1) t1 in
+ let e2, env = term_to_exp kf env (ctx_type t2) t2 in
Options.warning ~source:(fst loc) ~once:true
"missing guard for ensuring that %a is a valid pointer"
d_term t;
@@ -281,13 +281,13 @@ and context_insensitive_term_to_exp env t =
whatever is [e2] *)
new_exp ~loc (BinOp(bop, e1, e2, typeOf e1)), env, false
| TCastE(ty, t) ->
- let e, env = term_to_exp env (Ctype ty) t in
+ let e, env = term_to_exp kf env (Ctype ty) t in
mkCast e ty, env, false
| TAddrOf lv ->
- let lv, env = tlval_to_lval env lv in
+ let lv, env = tlval_to_lval kf env lv in
mkAddrOf ~loc lv, env, false
| TStartOf lv ->
- let lv, env = tlval_to_lval env lv in
+ let lv, env = tlval_to_lval kf env lv in
mkAddrOrStartOf ~loc lv, env, false
| Tapp _ -> Misc.not_yet "applying logic function"
| Tlambda _ -> Misc.not_yet "functional"
@@ -312,12 +312,12 @@ and context_insensitive_term_to_exp env t =
(* Convert an ACSL term into a corresponding C expression (if any) in the given
environment. Also extend this environment which includes the generating
constructs. *)
-and term_to_exp env ctx t =
- let e, env, is_mpz_string = context_insensitive_term_to_exp env t in
+and term_to_exp kf env ctx t =
+ let e, env, is_mpz_string = context_insensitive_term_to_exp kf env t in
context_sensitive ~loc:t.term_loc env ctx is_mpz_string e
(* generate the C code equivalent to [t1 bop t2]. *)
-and comparison_to_exp ?(loc=Location.unknown) ?e1 env bop t1 t2 =
+and comparison_to_exp ?(loc=Location.unknown) kf ?e1 env bop t1 t2 =
let ctx = match e1 with
| None -> principal_type_from_term t1 t2
| Some(_, ctx) ->
@@ -327,11 +327,11 @@ and comparison_to_exp ?(loc=Location.unknown) ?e1 env bop t1 t2 =
(* Options.feedback "principal type of %a and %a is %a"
d_term t1 d_term t2 d_logic_type ctx;*)
let e1, env = match e1 with
- | None -> term_to_exp env ctx t1
+ | None -> term_to_exp kf env ctx t1
| Some(e1, ctx1) when Cil_datatype.Logic_type.equal ctx ctx1 -> e1, env
| Some(e1, _) -> context_sensitive ~loc:e1.eloc env ctx false e1
in
- let e2, env = term_to_exp env ctx t2 in
+ let e2, env = term_to_exp kf env ctx t2 in
match ctx with
| Linteger ->
let e, env =
@@ -347,7 +347,7 @@ and comparison_to_exp ?(loc=Location.unknown) ?e1 env bop t1 t2 =
(* Convert an ACSL named predicate into a corresponding C expression (if
any) in the given environment. Also extend this environment which includes
the generating constructs. *)
-let rec named_predicate_to_exp env p =
+let rec named_predicate_to_exp kf env p =
let loc = p.loc in
match p.content with
| Pfalse -> zero ~loc, env
@@ -355,13 +355,13 @@ let rec named_predicate_to_exp env p =
| Papp _ -> Misc.not_yet "logic function application"
| Pseparated _ -> Misc.not_yet "separated"
| Prel(rel, t1, t2) ->
- let e, env = comparison_to_exp ~loc env (relation_to_binop rel) t1 t2 in
+ let e, env = comparison_to_exp ~loc kf env (relation_to_binop rel) t1 t2 in
context_sensitive ~loc env (Ctype intType) false e
| Pand(p1, p2) ->
(* p1 && p2 <==> if p1 then p2 else false *)
- let e1, env1 = named_predicate_to_exp env p1 in
+ let e1, env1 = named_predicate_to_exp kf env p1 in
let e2, env2 =
- named_predicate_to_exp (Env.no_overlap ~from:env1 Env.empty) p2
+ named_predicate_to_exp kf (Env.no_overlap ~from:env1 Env.empty) p2
in
let env = Env.merge_block_vars ~from:env2 env1 in
Env.new_var
@@ -379,9 +379,9 @@ let rec named_predicate_to_exp env p =
[ mkStmt ~valid_sid:true (If(e1, then_block, else_block, loc)) ])
| Por(p1, p2) ->
(* p1 || p2 <==> if p1 then true else p2 *)
- let e1, env1 = named_predicate_to_exp env p1 in
+ let e1, env1 = named_predicate_to_exp kf env p1 in
let e2, env2 =
- named_predicate_to_exp (Env.no_overlap ~from:env1 Env.empty) p2
+ named_predicate_to_exp kf (Env.no_overlap ~from:env1 Env.empty) p2
in
let env = Env.merge_block_vars ~from:env2 env1 in
Env.new_var
@@ -399,10 +399,10 @@ let rec named_predicate_to_exp env p =
[ mkStmt ~valid_sid:true (If(e1, then_block, else_block, loc)) ])
| Pxor _ -> Misc.not_yet "xor"
| Pimplies(p1, p2) ->
- named_predicate_to_exp env (Logic_const.por ((Logic_const.pnot p1), p2))
+ named_predicate_to_exp kf env (Logic_const.por ((Logic_const.pnot p1), p2))
| Piff _ -> Misc.not_yet "<==>"
| Pnot p ->
- let e, env = named_predicate_to_exp env p in
+ let e, env = named_predicate_to_exp kf env p in
new_exp ~loc (UnOp(LNot, e, TInt(IInt, []))), env
| Pif _ -> Misc.not_yet "_ ? _ : _"
| Plet _ -> Misc.not_yet "let _ = _ in _"
@@ -421,7 +421,7 @@ let rec named_predicate_to_exp env p =
statement (if any) for runtime assertion checking *)
(* ************************************************************************** *)
-let convert_preconditions env behaviors =
+let convert_preconditions kf env behaviors =
let do_behavior env b =
let assumes_pred =
List.fold_left
@@ -434,14 +434,14 @@ let convert_preconditions env behaviors =
let p =
Logic_const.pimplies (assumes_pred, Logic_const.unamed p.ip_content)
in
- let e, env = named_predicate_to_exp env p in
+ let e, env = named_predicate_to_exp kf env p in
Env.add_stmt env (Misc.mk_e_acsl_guard ~reverse:true e p))
env
b.b_requires
in
List.fold_left do_behavior env behaviors
-let convert_postconditions env behaviors =
+let convert_postconditions kf env behaviors =
(* generate one guard by postcondition of each behavior *)
let do_behavior env b =
List.fold_left
@@ -452,7 +452,7 @@ let convert_postconditions env behaviors =
if p <> Ptrue && b.b_assumes <> [] then
Misc.not_yet "assumes in conjunction with ensures in behaviors";
let p = Logic_const.unamed p in
- let e, env = named_predicate_to_exp env p in
+ let e, env = named_predicate_to_exp kf env p in
Env.add_stmt env (Misc.mk_e_acsl_guard ~reverse:true e p)
| Exits | Breaks | Continues | Returns ->
Misc.not_yet "abnormal termination case in behavior")
@@ -461,7 +461,7 @@ let convert_postconditions env behaviors =
in
List.fold_left do_behavior env behaviors
-let convert_behaviors env behaviors =
+let convert_behaviors kf env behaviors =
List.iter
(fun b ->
if b.b_assigns <> WritesAny then
@@ -469,10 +469,11 @@ let convert_behaviors env behaviors =
if b.b_extended <> [] then Misc.not_yet "grammar extensions in behavior")
behaviors;
let pre_env =
- convert_preconditions (Env.no_overlap ~from:env Env.empty) behaviors
+ convert_preconditions kf (Env.no_overlap ~from:env Env.empty) behaviors
in
let post_env =
- convert_postconditions (Env.no_overlap ~from:pre_env Env.empty) behaviors
+ convert_postconditions kf
+ (Env.no_overlap ~from:pre_env Env.empty) behaviors
in
let env = Env.merge_function_vars ~from:pre_env env in
let env = Env.merge_function_vars ~from:post_env env in
@@ -480,29 +481,29 @@ let convert_behaviors env behaviors =
Env.close_block_option post_env,
env
-let convert_spec env spec =
+let convert_spec kf env spec =
if spec.spec_variant <> None then Misc.not_yet "variant clause";
if spec.spec_terminates <> None then Misc.not_yet "terminates clause";
if spec.spec_complete_behaviors <> [] then Misc.not_yet "complete behaviors";
if spec.spec_disjoint_behaviors <> [] then Misc.not_yet "disjoint behaviors";
- convert_behaviors env spec.spec_behavior
+ convert_behaviors kf env spec.spec_behavior
-let convert_named_predicate env p =
- let e, env = named_predicate_to_exp env p in
+let convert_named_predicate kf env p =
+ let e, env = named_predicate_to_exp kf env p in
assert (Typ.equal (typeOf e) intType);
Env.add_stmt env (Misc.mk_e_acsl_guard ~reverse:true e p)
-let convert_code_annotation env annot =
+let convert_code_annotation kf env annot =
try
match annot.annot_content with
| AAssert(l, p) ->
if l <> [] then Misc.not_yet "assertions applied only on some behaviors";
- convert_named_predicate env p, None
+ convert_named_predicate kf env p, None
| AStmtSpec(l, spec) ->
if l <> [] then
Misc.not_yet "statement contract applied only on some behaviors";
let pre_block, post_block, new_env =
- convert_spec env spec
+ convert_spec kf env spec
in
let env = Env.merge_function_vars ~from:new_env env in
let env = match pre_block with
@@ -559,8 +560,12 @@ class e_acsl_visitor prj generate = object (self)
(self :> Visitor.frama_c_visitor)
(Kernel_function.get_spec old_kf)
in
+ (* We definitely are inside a function here. *)
+ let kf =
+ Cil.get_kernel_function self#behavior (Extlib.the self#current_kf)
+ in
let pre_b, post_b, env =
- Project.on prj (convert_spec Env.empty) spec
+ Project.on prj (convert_spec kf Env.empty) spec
in
pre_block <- pre_b;
post_block <- post_b;
@@ -586,13 +591,19 @@ class e_acsl_visitor prj generate = object (self)
let env, post_stmts =
Annotations.single_fold_stmt
(fun (User old_a | AI(_, old_a)) (env, post_stmts) ->
- let a =
- Visitor.visitFramacCodeAnnotation
- (self :> Visitor.frama_c_visitor)
+ let a =
+ (* [VP] Don't use Visitor here, as it will fill the
+ queue in the middle of the computation...
+ *)
+ Cil.visitCilCodeAnnotation
+ (self :> Cil.cilVisitor)
old_a
in
+ let kf =
+ Cil.get_kernel_function self#behavior (Extlib.the self#current_kf)
+ in
let env, post_block =
- Project.on prj (convert_code_annotation env) a
+ Project.on prj (convert_code_annotation kf env) a
in
let post_stmts = match post_block with
| None -> post_stmts