From 108f6b68777bde0333577a8e74783c30656840b2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 26 Mar 2020 15:25:22 +0100
Subject: [PATCH] [tests] avoid duplication definition warnings in oracles
---
.../instantiate/tests/stdlib/oracle/calloc.res.oracle | 3 ---
.../instantiate/tests/stdlib/oracle/free.res.oracle | 11 -----------
.../instantiate/tests/stdlib/oracle/malloc.res.oracle | 3 ---
src/plugins/instantiate/tests/stdlib/test_config | 2 +-
4 files changed, 1 insertion(+), 18 deletions(-)
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
index 81cf9b246df..28d42c036e3 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
@@ -272,9 +272,6 @@ int main(void)
[kernel] Parsing tests/stdlib/result/calloc.c (with preprocessing)
-[kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
-[kernel] tests/stdlib/calloc.c:14: Warning:
- def'n of func main at tests/stdlib/calloc.c:14 (sum 7290) conflicts with the one at tests/stdlib/result/calloc.c:253 (sum 9064); keeping the one at tests/stdlib/result/calloc.c:253.
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
index 11f5ef65b0e..cfdb769ed8d 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
@@ -139,17 +139,6 @@ void with_incomplete(struct incomplete *t)
[kernel] Parsing tests/stdlib/result/free.c (with preprocessing)
-[kernel] Parsing tests/stdlib/free.c (with preprocessing)
-[kernel] tests/stdlib/free.c:3: Warning:
- dropping duplicate def'n of func foo at tests/stdlib/free.c:3 in favor of that at tests/stdlib/result/free.c:30
-[kernel] tests/stdlib/free.c:6: Warning:
- dropping duplicate def'n of func bar at tests/stdlib/free.c:6 in favor of that at tests/stdlib/result/free.c:62
-[kernel] tests/stdlib/free.c:9: Warning:
- dropping duplicate def'n of func baz at tests/stdlib/free.c:9 in favor of that at tests/stdlib/result/free.c:94
-[kernel] tests/stdlib/free.c:12: Warning:
- dropping duplicate def'n of func with_void at tests/stdlib/free.c:12 in favor of that at tests/stdlib/result/free.c:100
-[kernel] tests/stdlib/free.c:15: Warning:
- dropping duplicate def'n of func with_incomplete at tests/stdlib/free.c:15 in favor of that at tests/stdlib/result/free.c:132
/* Generated by Frama-C */
#include "stdlib.h"
struct incomplete;
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
index 485abcec7f4..6cec0abadff 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
@@ -217,9 +217,6 @@ int main(void)
[kernel] Parsing tests/stdlib/result/malloc.c (with preprocessing)
-[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
-[kernel] tests/stdlib/malloc.c:16: Warning:
- def'n of func main at tests/stdlib/malloc.c:16 (sum 7290) conflicts with the one at tests/stdlib/result/malloc.c:199 (sum 9064); keeping the one at tests/stdlib/result/malloc.c:199.
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
diff --git a/src/plugins/instantiate/tests/stdlib/test_config b/src/plugins/instantiate/tests/stdlib/test_config
index dba5b7b5f4a..cc295b08655 100644
--- a/src/plugins/instantiate/tests/stdlib/test_config
+++ b/src/plugins/instantiate/tests/stdlib/test_config
@@ -1 +1 @@
-OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-instantiate @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
\ No newline at end of file
+OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-instantiate @PTEST_DIR@/result/@PTEST_NAME@.c -ocode="" -print
--
GitLab