"Unknown Error" with Alt-Ergo
Before submitting the issue, please confirm (by adding a X in the [ ]):
-
the issue has not yet been reported on Gitlab; -
the issue has not yet been reported on our old BTS (note: the old BTS is deprecated); -
you installed Frama-C as prescribed in the instructions.
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 21.1 (Scandium)
- Plug-in used: wp
- OS name: Windows (via WSL 1)
- OS version: Windows 10 Pro build 19041.685
I have also done rm -f ~/.why3.conf; why3 config --detect --full-config
quite a few times now.
Steps to reproduce the issue
Just creating a simple C file called swap.c
:
/*@
requires \valid(a) && \valid(b);
assigns *a, *b;
ensures *a == \old(*b);
ensures *b == \old(*a);
*/
void swap(int *a, int *b) {
int tmp = *a;
*a = *b;
*b = tmp;
}
int main() {
int a = 42;
int b = 37;
swap(&a, &b);
//@ assert a == 37 && b == 42;
return 0;
}
And running it with
frama-c -wp swap.c
Expected behaviour
All goals proven.
Actual behaviour
Alt-Ergo gives an Unknown error
.
[kernel] Parsing swap.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_swap_ensures : Failed
Unknown error
[wp] Proved goals: 5 / 6
Qed: 5
Alt-Ergo 2.2.0: 0 (failed: 1)
I'm seeing this happen with a much larger project for just about every single goal there, too. I cannot verify a single C program with ACSL annotations, it seems.
Fix ideas
No idea. I can't seem to find any information about this aside from a single unanswered StackOverflow question.