Skip to content
Snippets Groups Projects
Commit 96fd47bd authored by Julien Signoles's avatar Julien Signoles
Browse files

update oracles according to changes of kernel message

parent 0ca5c947
No related branches found
No related tags found
No related merge requests found
...@@ -94,7 +94,7 @@ PROJECT_FILE.i:145:[value] Assertion got status valid. ...@@ -94,7 +94,7 @@ PROJECT_FILE.i:145:[value] Assertion got status valid.
[value] Done for function mpz_init [value] Done for function mpz_init
[value] computing for function mpz_com <- main. [value] computing for function mpz_com <- main.
Called from PROJECT_FILE.i:149. 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] Done for function mpz_com
[value] computing for function mpz_cmp <- main. [value] computing for function mpz_cmp <- main.
Called from PROJECT_FILE.i:150. Called from PROJECT_FILE.i:150.
......
gcc: autom4te.cache/: linker input file unused because linking not done 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: share/: linker input file unused because linking not done
gcc: tests/: linker input file unused because linking not done gcc: tests/: linker input file unused because linking not done
[kernel] preprocessing with "gcc -C -E -I. autom4te.cache/" [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. share/"
[kernel] preprocessing with "gcc -C -E -I. tests/" [kernel] preprocessing with "gcc -C -E -I. tests/"
/* Generated by Frama-C */ /* Generated by Frama-C */
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment