0002159: alt-ergo: undefined symbol andb - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

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

Notes
(0006035) 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

Issue History
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	Note Added: 0006036
2015-09-14 16:51	correnson	Status	assigned => acknowledged
2015-09-14 16:51	correnson	Note Edited: 0006036	View Revisions
2015-09-14 16:52	correnson	Note Deleted: 0006036
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