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

[#21687] why: needs porting to why3

Date:
2018-06-28 18:16
Priority:
3
State:
Open
Submitted by:
Ralf Treinen (treinen)
Assigned to:
Nobody (None)
Hardware:
none
Product:
none
Operating System:
none
Component:
none
Version:
none
Severity:
none
Resolution:
none
URL:
Summary:
why: needs porting to why3

Detailed description
why needs to be ported to the new syntax of WhyML introduced in why3 1.0.0.

For instance, I get the following error on the attached file, with why version 2.40:

$ frama-c -jessie -jessie-why3 "prove -P alt-ergo" minimum.c
[kernel] Parsing minimum.c (with preprocessing)
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir minimum.jessie
[jessie] File minimum.jessie/minimum.jc written.
[jessie] File minimum.jessie/minimum.cloc written.
[jessie] Calling Jessie tool in subdir minimum.jessie
Generating Why function max
Calling Why3...
[Config] reading extra configuration file /usr/share/why/why3/why3.conf
File "././minimum.mlw", line 3, characters 0-18:
warning: the keyword `import' is redundant here and can be omitted
File "././minimum.mlw", line 9, characters 0-50:
warning: the keyword `import' is redundant here and can be omitted
File "/usr/share/why/why3/jessie_why3theories.why", line 4, characters 0-18:
warning: the keyword `import' is redundant here and can be omitted
File "/usr/share/why/why3/jessie_why3theories.why", line 105, characters 0-20:
warning: the keyword `import' is redundant here and can be omitted
File "././minimum.mlw", line 23, characters 26-27:
syntax error

No Comments Have Been Posted

Attachments:
Size Name Date By Download
90 bytesminimum.c2018-06-28 18:16treinenminimum.c
Field Old Value Date By
File Added6122: minimum.c2018-06-28 18:16treinen