alt-ergo: undefined symbol andb
ID0002159: This issue was created automatically from Mantis Issue 2159. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002159 | Frama-C | Plug-in > wp | public | 2015-09-14 | 2016-06-21 |
| Reporter | azaostro | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | 64 bit | OS | Ubuntu | OS Version | 14.04 |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | Frama-C Aluminium |
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