diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle index 0541e861132e3b997b4b82f7ce5665f82a9799d1..69fdc5c217b22c0eebfd739016aacd0e3dddb422 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle @@ -94,7 +94,7 @@ PROJECT_FILE.i:145:[value] Assertion got status valid. [value] Done for function mpz_init [value] computing for function mpz_com <- main. Called from PROJECT_FILE.i:149. -[kernel] No code for function mpz_com, default assigns generated +[kernel] warning: No code for function mpz_com, default assigns generated [value] Done for function mpz_com [value] computing for function mpz_cmp <- main. Called from PROJECT_FILE.i:150. 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 8438c04ee4e2168cf3c22870c3fa5d772193a043..c789997e5fa8b33649a2cc0806e137d306a01a60 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,3 +1,4 @@ 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 36ef1e3e940097b682cb58a8b06b5a3e53b76cd9..9464c770e751fd1aaf2d23b74a2393e42a9857d4 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,4 +1,5 @@ [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 */