--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on February 2018 ---
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