From 900c3df469a6c11f7cb0ba8f47aafe7e3d95215d Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 6 Sep 2018 18:12:07 +0200
Subject: [PATCH] synchronize with frama-c/frama-c!1717
---
src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c | 6 ++++++
.../e-acsl/tests/temporal/oracle/t_getenv.res.oracle | 4 ++--
2 files changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
index 0ce7ca09746..3408a9d5cd5 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
@@ -39,6 +39,9 @@ int main(int argc, char const **argv)
/*@ assert g1 ≡ \null ∨ \valid(g1); */
{
int __gen_e_acsl_or;
+ /*@ assert
+ Value: ptr_comparison: \pointer_comparable((void *)g1, (void *)0);
+ */
if (g1 == (char *)0) __gen_e_acsl_or = 1;
else {
int __gen_e_acsl_initialized;
@@ -60,6 +63,9 @@ int main(int argc, char const **argv)
/*@ assert g2 ≡ \null ∨ \valid(g2); */
{
int __gen_e_acsl_or_2;
+ /*@ assert
+ Value: ptr_comparison: \pointer_comparable((void *)g2, (void *)0);
+ */
if (g2 == (char *)0) __gen_e_acsl_or_2 = 1;
else {
int __gen_e_acsl_initialized_2;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
index b315d3a44d1..27722df6cd9 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
@@ -2,10 +2,10 @@
[e-acsl] Warning: annotating undefined function `getenv':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:417: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:419: Warning:
E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:417: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:419: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
--
GitLab