From 0bae683ebf1bc36b4193ebe7e7bdc0ad131d1ef9 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 7 May 2021 15:10:51 +0200
Subject: [PATCH] update test oracles
---
.../e-acsl/tests/format/oracle_ci/fprintf.res.oracle | 6 +++---
src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c | 2 +-
src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c | 2 +-
src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle | 6 +++---
src/plugins/variadic/tests/known/oracle/fcntl.res.oracle | 6 +++---
src/plugins/variadic/tests/known/oracle/open.res.oracle | 6 +++---
.../variadic/tests/known/oracle/open_wrong.res.oracle | 6 +++---
src/plugins/variadic/tests/known/oracle/openat.res.oracle | 6 +++---
8 files changed, 20 insertions(+), 20 deletions(-)
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
index 15a3701b3de..8055b166f12 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
@@ -14,7 +14,7 @@
[e-acsl] Warning: annotating undefined function `fork':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:854: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:856: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: Warning:
@@ -41,9 +41,9 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:859: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:859: Warning:
function __gen_e_acsl_fork: postcondition 'result_ok_child_or_error' got status unknown.
[kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning:
Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
index 7f462f80f72..0433d13f02b 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
@@ -110,7 +110,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",857);
+ "FRAMAC_SHARE/libc/unistd.h",859);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
index 0a22e2db5a4..3f1ff2269f2 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
@@ -682,7 +682,7 @@ pid_t __gen_e_acsl_fork(void)
else __gen_e_acsl_or_2 = __retres == -1;
__e_acsl_assert(__gen_e_acsl_or_2,1,"Postcondition","fork",
"result_ok_child_or_error: \\result == 0 || \\result > 0 || \\result == -1",
- "FRAMAC_SHARE/libc/unistd.h",857);
+ "FRAMAC_SHARE/libc/unistd.h",859);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
index cb01c6b6e06..1faab6ba910 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
@@ -29,7 +29,7 @@
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:854: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:856: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:354: Warning:
@@ -104,9 +104,9 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:859: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:857: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:859: Warning:
function __gen_e_acsl_fork: postcondition 'result_ok_child_or_error' got status unknown.
[kernel:annot:missing-spec] tests/format/printf.c:180: Warning:
Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
diff --git a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
index 9a28a06f1dd..5764d84562d 100644
--- a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:113:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:117:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:116: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:122:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:120: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:126:
Declaration of variadic function openat.
[variadic] tests/known/fcntl.c:8:
Translating call to the specialized version fcntl(int, int).
diff --git a/src/plugins/variadic/tests/known/oracle/open.res.oracle b/src/plugins/variadic/tests/known/oracle/open.res.oracle
index 840ef4ab762..156a72c8328 100644
--- a/src/plugins/variadic/tests/known/oracle/open.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:113:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:117:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:116: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:122:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:120: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:126:
Declaration of variadic function openat.
[variadic] tests/known/open.c:7:
Translating call to the specialized version open(char const *, int, mode_t).
diff --git a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
index b7200eb4eb8..285d13c560c 100644
--- a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:113:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:117:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:116: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:122:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:120: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:126:
Declaration of variadic function openat.
[variadic] tests/known/open_wrong.c:13: Warning:
No matching prototype found for this call to open.
diff --git a/src/plugins/variadic/tests/known/oracle/openat.res.oracle b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
index 2fe15e305f2..b9409a83506 100644
--- a/src/plugins/variadic/tests/known/oracle/openat.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:113:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:117:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:116: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:122:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:120: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:126:
Declaration of variadic function openat.
[variadic] tests/known/openat.c:8:
Translating call to the specialized version openat(int, char const *, int, mode_t).
--
GitLab