--- layout: fc_discuss_archives title: Message 3 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,

In short: you are doing nothing wrong, these axioms should have been
declared as lemmas instead.

This warning was introduced in Why3 to prevent a common mistake:
introducing an axiom not associated with the introduction of a logic
symbol. (Note that ACSL does something different: axiom can only be
given inside "axiomatic" blocks).

I don't see any simple workaround, apart from editing that Qed.why file
and replacing "axiom" by "lemma". (This will NOT require you to prove
these lemmas anyway)

- Claude

Le 04/02/2018 à 21:29, Stephen Siegel a écrit :
> 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
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> 

-- 
Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - ÃŽle-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |