GitLab

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.