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



Thanks, Claude, I’ll just ignore those warnings.
-Steve

> On Feb 5, 2018, at 3:14 AM, Claude Marché <Claude.Marche at inria.fr> wrote:
> 
> 
> 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                    |
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss