Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2547

Closed
Open
Created Mar 26, 2021 by Qix@Qix-3 of 3 tasks completed3/3 tasks

"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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking