search

Frama-C / Frama-C-snapshot

Release snapshots of the Frama-C platform for source code analysis
http://frama-c.com
168 stars 38 forks source link

Why3-1.x.x #17

Closed xtrm0 closed 5 years ago

xtrm0 commented 5 years ago

I am trying to port wp to use why3-1.2.0, but it's kind of difficult because I am not familiar with why3. So one of the problems I found is that it fails to compile against why3, because why3-1.2.0 doesn't defines map.Map.get anymore (previously defined insided why3 on lib/coq/map/Map.v). More specifically on src/plugins/wp/share/why3/Qedlib.v, this function is used:

Definition select {A B : Type}
  (m : farray A B) (k : A) : B := @Map.get A (whytype1 m) B (whytype2 m) m k.

Copying the function there is possible, but it's a hack and not a formalization; and also it breaks some proofs because I guess other theorems defined on why3 are not available anymore. Any thoughts on how to fix it?

Is there any planned release supporting this version of why3?

bobot commented 5 years ago

Yes the next version of frama-c will support why3 1.2.0 . Thank you for considering making the migration yourself.

xtrm0 commented 5 years ago

Do you have any planned release date?

bobot commented 5 years ago

The next release is planned for mid-May.

xtrm0 commented 5 years ago

I managed to make frama C 18.0 compile with why3.1.2.0 and coq.8.9.0, but I still can't get why3-ide to start under frama C, or why3 to work with coq because I guess the interface fro why3 ide is different (under: https://github.com/xtrm0/Frama-C-snapshot/tree/why3-1.2.0). I am going to rely on alt-ergo and direct translation to coq for now, and wait till may to finish harder proofs for my thesis :P