Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
F
frama-c
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 336
    • Issues 336
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 0
    • Merge Requests 0
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2547

Closed
Open
Opened 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
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: pub/frama-c#2547