From 8ddd387d3787964ffdb13f0afc62e86c119f2001 Mon Sep 17 00:00:00 2001
From: Benjamin Monate <benjamin.monate@cea.fr>
Date: Mon, 16 May 2011 08:38:02 +0000
Subject: [PATCH] Fixed oracle broken by kernel fix
---
.../e-acsl/tests/e-acsl-runtime/oracle/empty.err.oracle | 1 -
.../e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle | 1 -
.../e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c | 3 ++-
.../tests/e-acsl-runtime/oracle/other_constants.res.oracle | 3 ++-
4 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.err.oracle
index c789997e5fa..8438c04ee4e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.err.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.err.oracle
@@ -1,4 +1,3 @@
gcc: autom4te.cache/: linker input file unused because linking not done
-gcc: doc/: linker input file unused because linking not done
gcc: share/: linker input file unused because linking not done
gcc: tests/: linker input file unused because linking not done
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
index 9464c770e75..36ef1e3e940 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
@@ -1,5 +1,4 @@
[kernel] preprocessing with "gcc -C -E -I. autom4te.cache/"
-[kernel] preprocessing with "gcc -C -E -I. doc/"
[kernel] preprocessing with "gcc -C -E -I. share/"
[kernel] preprocessing with "gcc -C -E -I. tests/"
/* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
index e3ce7f6a71b..e2e610c62b1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
@@ -584,7 +584,8 @@ int main(void)
}
/*@ assert false ≢ true; */ ;
- if (! ((int)false != (int)true)) { e_acsl_fail((char *)"(false != true)");
+ if (! ((unsigned int)false != (unsigned int)true)) {
+ e_acsl_fail((char *)"(false != true)");
}
__retres = 0;
return (__retres);
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 2835d90b3ff..5aebbdd4cb4 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
@@ -112,7 +112,8 @@ int main(void)
}
/*@ assert false ≢ true; */ ;
- if (! ((int)false != (int)true)) { e_acsl_fail((char *)"(false != true)");
+ if (! ((unsigned int)false != (unsigned int)true)) {
+ e_acsl_fail((char *)"(false != true)");
}
__retres = 0;
return (__retres);
--
GitLab