From c72da78ac96521a25087dc049de2bf510506f0a4 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 27 Jan 2017 10:18:03 +0100
Subject: [PATCH] Update test case oracles as per Frama-C MR# !1112
---
.../tests/bts/oracle/bts1740.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts1740.c | 7 +--
.../runtime/oracle/bypassed_var.res.oracle | 2 +-
.../runtime/oracle/early_exit.res.oracle | 2 +-
.../tests/runtime/oracle/gen_bypassed_var.c | 9 ++--
.../tests/runtime/oracle/gen_early_exit.c | 51 ++++++++++---------
6 files changed, 38 insertions(+), 35 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
index 4d0f31c840e..845be00612e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1740.i:12:[value] warning: locals {a} escaping the scope of a block of main through p
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
index e165312e35d..7d1822a0543 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
@@ -1,13 +1,14 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
int *p;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
{
int a;
- __e_acsl_store_block((void *)(& a),4UL);
+ __e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a));
a = 0;
__e_acsl_full_init((void *)(& p));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
index f8de72eb5d5..66bbcfdda01 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/bypassed_var.c:16:[value] warning: accessing uninitialized left-value. assert \initialized(&p);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
index 638dd2dcbe2..5c4f44cb7b1 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/early_exit.c:14:[value] warning: locals {a} escaping the scope of a block of goto_bts through p
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
index a1eb4fce0d0..acd909e18da 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
@@ -1,15 +1,16 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int bypassed_var(int i)
{
int lst[2];
- __e_acsl_store_block((void *)(lst),8UL);
+ __e_acsl_store_block((void *)(lst),(size_t)8);
if (i) goto L;
{
int *p;
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
p = (int *)(& lst);
- L: __e_acsl_store_block_duplicate((void *)(& p),8UL);
+ L: __e_acsl_store_block_duplicate((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
/*@ assert Value: initialisation: \initialized(&p); */
p ++;
@@ -60,7 +61,7 @@ int bypassed_var(int i)
int main(int argc, char const **argv)
{
int __retres;
- __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
+ __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
bypassed_var(0);
bypassed_var(1);
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
index 4ec72b8a82d..897f45cce1a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int goto_bts(void)
{
int __retres;
int *p;
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
{
int a;
- __e_acsl_store_block((void *)(& a),4UL);
+ __e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a));
a = 0;
__e_acsl_full_init((void *)(& p));
@@ -63,27 +64,27 @@ int goto_valid(void)
int *p;
int *q;
int *r;
- __e_acsl_store_block((void *)(& r),8UL);
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& r),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
a = 9;
{
int a1;
- __e_acsl_store_block((void *)(& a1),4UL);
+ __e_acsl_store_block((void *)(& a1),(size_t)4);
__e_acsl_full_init((void *)(& a1));
a1 = 0;
__e_acsl_full_init((void *)(& p));
p = & a1;
{
int a2;
- __e_acsl_store_block((void *)(& a2),4UL);
+ __e_acsl_store_block((void *)(& a2),(size_t)4);
__e_acsl_full_init((void *)(& a2));
a2 = 0;
__e_acsl_full_init((void *)(& q));
q = & a2;
{
int a3;
- __e_acsl_store_block((void *)(& a3),4UL);
+ __e_acsl_store_block((void *)(& a3),(size_t)4);
__e_acsl_full_init((void *)(& a3));
a3 = 0;
__e_acsl_full_init((void *)(& r));
@@ -238,10 +239,10 @@ int switch_valid(void)
int *p;
int *q;
int *s;
- __e_acsl_store_block((void *)(& s),8UL);
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& i),4UL);
+ __e_acsl_store_block((void *)(& s),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& i),(size_t)4);
__e_acsl_full_init((void *)(& i));
i = 1;
__e_acsl_full_init((void *)(& s));
@@ -250,14 +251,14 @@ int switch_valid(void)
default: ;
{
int a1;
- __e_acsl_store_block((void *)(& a1),4UL);
+ __e_acsl_store_block((void *)(& a1),(size_t)4);
__e_acsl_full_init((void *)(& a1));
a1 = 0;
__e_acsl_full_init((void *)(& p));
p = & a1;
{
int a2;
- __e_acsl_store_block((void *)(& a2),4UL);
+ __e_acsl_store_block((void *)(& a2),(size_t)4);
__e_acsl_full_init((void *)(& a2));
a2 = 0;
__e_acsl_full_init((void *)(& q));
@@ -397,13 +398,13 @@ int while_valid(void)
int *q;
int *r;
int i;
- __e_acsl_store_block((void *)(& r),8UL);
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& r),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
i = 5;
{
int a0;
- __e_acsl_store_block((void *)(& a0),4UL);
+ __e_acsl_store_block((void *)(& a0),(size_t)4);
__e_acsl_full_init((void *)(& a0));
a0 = 0;
__e_acsl_full_init((void *)(& r));
@@ -413,14 +414,14 @@ int while_valid(void)
if (! i) break;
{
int a1;
- __e_acsl_store_block((void *)(& a1),4UL);
+ __e_acsl_store_block((void *)(& a1),(size_t)4);
__e_acsl_full_init((void *)(& a1));
a1 = 0;
__e_acsl_full_init((void *)(& p));
p = & a1;
{
int a2;
- __e_acsl_store_block((void *)(& a2),4UL);
+ __e_acsl_store_block((void *)(& a2),(size_t)4);
__e_acsl_full_init((void *)(& a2));
a2 = 0;
__e_acsl_full_init((void *)(& q));
@@ -555,8 +556,8 @@ void continue_valid(void)
int i;
int *p;
int *q;
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
i = 0;
while (1) {
int tmp;
@@ -568,7 +569,7 @@ void continue_valid(void)
if (! tmp) break;
{
int a1;
- __e_acsl_store_block((void *)(& a1),4UL);
+ __e_acsl_store_block((void *)(& a1),(size_t)4);
/*@ assert ¬\valid(p); */
{
{
@@ -643,7 +644,7 @@ void continue_valid(void)
}
{
int a2;
- __e_acsl_store_block((void *)(& a2),4UL);
+ __e_acsl_store_block((void *)(& a2),(size_t)4);
__e_acsl_full_init((void *)(& a2));
a2 = 1;
__e_acsl_full_init((void *)(& q));
@@ -738,7 +739,7 @@ void continue_valid(void)
int main(int argc, char const **argv)
{
int __retres;
- __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
+ __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
goto_bts();
goto_valid();
switch_valid();
--
GitLab