Home My Page Projects The Why platform
Summary Activity Forums Tracker Lists Tasks Docs News SCM Files

[#21668] Potential Bug of frama-c Jessie plug-in

Date:
2018-05-18 15:05
Priority:
3
State:
Open
Submitted by:
Jianyang PAN (projectyoung)
Assigned to:
Nobody (None)
Hardware:
PC
Product:
none
Operating System:
Linux
Component:
none
Version:
none
Severity:
none
Resolution:
none
URL:
Summary:
Potential Bug of frama-c Jessie plug-in

Detailed description
Hi,

I'm using Jessie to try some proofs. (frama-c 20171101, why 2.40)

When I try a simple C program (also attached):

/*@ ensures \result == 0; */
int main(void)
{
if(1 + 1 == 2 && 2 + 2 == 4) {
return 0;
} else {
return 0;
}
}

I got an error as following:

RPK@MSI:/mnt/d/MPFR$ frama-c -jessie ex.c
[kernel] Parsing ex.c (with preprocessing)
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir ex.jessie
[jessie] File ex.jessie/ex.jc written.
[jessie] File ex.jessie/ex.cloc written.
[jessie] Calling Jessie tool in subdir ex.jessie
Generating Why function main
Calling Why3...
[Config] reading extra configuration file /home/RPK/.opam/4.06.1/lib/why/why3/why3.conf
Error while opening session:
File "././ex/../ex.mlw", line 266, characters 0-1063:
This function raises Return_label_exc but does not specify a post-condition for it

I guess it's a bug of jessie? Or maybe I did something wrong with config or whatever?

Best,
Jianyang
Message  ↓
Date: 2018-05-23 19:52
Sender: Claude Marché


Yes, a bug in the generation of the intermediate Why3 code.
A workaround is to always add a final return in the body of the function, even if like in that case it is unreachable.

Attachments:
Size Name Date By Download
125 bytesex.c2018-05-18 15:05projectyoungex.c
Field Old Value Date By
File Added6114: ex.c2018-05-18 15:05projectyoung