Ghost variable initialization and logic functions
Steps to reproduce the issue
Here is example code:
/*@ axiomatic A {
logic integer Lneg(integer i) = -i;
}
*/
/*@ assigns \nothing; ensures \result == -i; */
int neg(int i) { return -i; }
void test(int j) {
//@ ghost int kk = Lneg(j);
int k = neg(j);
//@ assert k == kk;
}
frama-c -wp
produces
fc $ frama-c -wp logic.c
[kernel] Parsing logic.c (with preprocessing)
[kernel:typing:implicit-function-declaration] logic.c:10: Warning:
Calling undeclared function Lneg. Old style K&R code?
[kernel:ghost:bad-use] logic.c:10: Warning:
Call to non-ghost function from ghost code is not allowed
[kernel:annot:missing-spec] logic.c:9: Warning:
Neither code nor specification for function Lneg, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_test_assert : Timeout (Qed:1ms) (10s)
[wp] Proved goals: 2 / 3
Qed: 2 (0.21ms-0.72ms)
Alt-Ergo 2.4.1: 0 (interrupted: 1)
[wp:pedantic-assigns] logic.c:9: Warning:
No 'assigns' specification for function 'test'.
Callers assumptions might be imprecise.
[wp:pedantic-assigns] logic.c:10: Warning:
No 'assigns' specification for function 'Lneg'.
Callers assumptions might be imprecise.
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
It appears to treat Lneg as a regular function, complaining that it is non-ghost and has no specs.
However, if neg
is used instead, WP still complains, although now it runs the proof successfully:
[kernel] Parsing logic.c (with preprocessing)
[kernel:ghost:bad-use] logic.c:10: Warning:
Call to non-ghost function from ghost code is not allowed
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] Proved goals: 3 / 3
Qed: 3 (0.21ms-0.68ms-1ms)
[wp:pedantic-assigns] logic.c:9: Warning:
No 'assigns' specification for function 'test'.
Callers assumptions might be imprecise.
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
Expected behaviour
I would expect Lneg
to be allowed here. If a non-ghost function like neg
is allowed to be used as a ghost logic function, as it apparently is (e.g. as long as it is pure), then there should be no need for a warning.
Contextual information
Frama-C 25.0, built from source, with frama-clang added. Using WP as built with Frama-C. MacOS 12.5