--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on February 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] warnings from Why3



Hello,
I’m using Frama-C+WP+Why3 through frama-c-gui (Sulfur).  I installed everything using opam.

I get these warnings in a little pop up box when I try to prove things through why3.   Just wondering if anyone else sees this or if I’m doing anything wrong…


File "/home/user/.opam/system/share/frama-c/wp/why3/Qed.why", line 68, characters 6-17: axiom c_euclidian does not contain any local abstract symbol

File "/home/user/.opam/system/share/frama-c/wp/why3/Qed.why", line 73, characters 6-16: axiom cdiv_cases does not contain any local abstract symbol

File "/home/user/.opam/system/share/frama-c/wp/why3/Qed.why", line 83, characters 6-16: axiom cmod_cases does not contain any local abstract symbol

File "/home/user/.opam/system/share/frama-c/wp/why3/Qed.why", line 93, characters 6-20: axiom cmod_remainder does not contain any local abstract symbol

[12 more warnings. See stderr for details]

-Steve