diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle index 81cf9b246df3d570b24e87e36cf0e0e11c4019f3..28d42c036e394314e15f148be188d770b46886e9 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 11f5ef65b0eda0f0b4f850b39e7595246a5cc234..cfdb769ed8d5e5412d854f0a741ba18d912fcfaf 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 485abcec7f4dbb6805bd76a022af060cb23a0804..6cec0abadff6e4e4fd12bfb6d6629c04e09816a6 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 dba5b7b5f4a3904ab10ba039dce5bee0734e2101..cc295b086555e3e3854cbe0f8013b3f96f464c7d 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