| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002159 | Frama-C | Plug-in > wp | public | 2015-09-14 14:30 | 2016-06-21 14:08 |
|
| Reporter | azaostro | |
| Assigned To | correnson | |
| Priority | normal | Severity | minor | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | 64 bit | OS | Ubuntu | OS Version | 14.04 |
| Product Version | Frama-C Sodium | |
| Target Version | | Fixed in Version | Frama-C Aluminium | |
|
| Summary | 0002159: alt-ergo: undefined symbol andb |
| Description | WP fails to handle my recursive boolean function, defined as "full_rec":
/*@ logic integer size_rec{L}(int* busybits, integer capa) =
@ (capa == 0) ? 0 :
@ (busybits[capa-1] != 0) ? 1 + size_rec(busybits, capa - 1) : 0;
@
@ logic boolean full_rec{L}(int *busybits, integer capa) =
@ (capa == 0) ? \true :
@ (busybits[capa-1] != 0) ? full_rec(busybits, capa - 1) : \false;
@
@ lemma full_rec_size_rec: \forall int* busybits, integer capa;
@ size_rec(busybits, capa) == capa <==> full_rec(busybits, capa);
*/
The result:
$ frama-c -wp repr.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing repr.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] 1 goal scheduled
/tmp/wpfaa705.dir/typed/lemma_full_rec_size_rec.ergo:13:[wp] user error: Alt-Ergo error:
characters 5-94:typing error: undefined symbol andb
[wp] [Alt-Ergo] Goal typed_lemma_full_rec_size_rec : Failed
Error: characters 5-94:typing error: undefined symbol andb
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (failed: 1) |
| Steps To Reproduce | run
frama-c -wp repr.c
on the attached file repr.c |
| Tags | No tags attached. |
|
| Attached Files |  repr.c [^] (462 bytes) 2015-09-14 14:30 [Show Content] [Hide Content]/*@ logic integer size_rec{L}(int* busybits, integer capa) =
@ (capa == 0) ? 0 :
@ (busybits[capa-1] != 0) ? 1 + size_rec(busybits, capa - 1) : 0;
@
@ logic boolean full_rec{L}(int *busybits, integer capa) =
@ (capa == 0) ? \true :
@ (busybits[capa-1] != 0) ? full_rec(busybits, capa - 1) : \false;
@
@ lemma full_rec_size_rec: \forall int* busybits, integer capa;
@ size_rec(busybits, capa) == capa <==> full_rec(busybits, capa);
*/
|
|
Relationships 
Relationships