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 ## Attachments - [repr.c](/uploads/78cf3015b33886cf55680addd2e02316/repr.c)