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 |
|
![]() |
|
correnson (manager) 2015-09-14 16:51 |
This is an error in the native boolean driver for Alt-Ergo. You can use Alt-Ergo through Why3 instead: # opam install why3 # frama-c -wp-prover why3:alt-ergo |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2015-09-14 14:30 | azaostro | New Issue | |
2015-09-14 14:30 | azaostro | Status | new => assigned |
2015-09-14 14:30 | azaostro | Assigned To | => correnson |
2015-09-14 14:30 | azaostro | File Added: repr.c | |
2015-09-14 16:51 | correnson | Note Added: 0006035 | |
2015-09-14 16:51 | correnson | Status | assigned => acknowledged |
2015-11-25 15:36 | correnson | Status | acknowledged => resolved |
2015-11-25 15:36 | correnson | Fixed in Version | => Frama-C Aluminium |
2015-11-25 15:36 | correnson | Resolution | open => fixed |
2016-06-21 14:08 | signoles | Status | resolved => closed |