frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-04-15T09:14:52Z
https://git.frama-c.com/pub/frama-c/-/issues/389
wp: the example from Getting Started guide doesn't work (all goals are Unknown)
2021-04-15T09:14:52Z
mantis-gitlab-migration
wp: the example from Getting Started guide doesn't work (all goals are Unknown)
ID0002261:
**This issue was created automatically from Mantis Issue 2261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002261:
**This issue was created automatically from Mantis Issue 2261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002261 | Frama-C | Plug-in > wp | public | 2016-12-14 | 2016-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vlad | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Windows | **OS** | Windows 7 | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm trying to reproduce ASCL example from frama-c manual. For some reason all goals sent to alt-ergo end up with unknown result.
Code:
$ cat frama-c-test.c
/*@ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b);
@ ensures B: *b == \old(*a);
@ assigns *a,*b;
@*/
void swap(int * a, int * b);
void swap(int *a,int *b)
{
int tmp = *a ;
*a = *b ;
*b = tmp ;
return ;
}
Frama-C result:
$ frama-c -wp -wp-rte frama-c-test.c
[kernel] Parsing .opam/4.02.3+mingw32c/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing frama-c-test.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function swap
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_4 : Unknown (65ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_3 : Unknown (64ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access_2 : Unknown (61ms)
[wp] [Alt-Ergo] Goal typed_swap_assert_rte_mem_access : Unknown (60ms)
[wp] Proved goals: 0 / 4
Alt-Ergo: 0 (unknown: 4)
The exact same code works with Frama-C Aluminum on Linux. I'm running Frama-C on Windows 7 (with cygwin).
### Additional Information :
$ alt-ergo -version
1.30
$ frama-c --version
Silicon-20161101
Virgile Prevosto
Virgile Prevosto