's apparently a utility module that ships with why3:
$ find . -name number.ml
./src/util/number.ml
You are probably missing "-I src/util" in the compilation switches, so that
Number is visible.
Best regards
--
Yannick Moy, Senior Software Engineer, AdaCore
___
r one, it won't be possible to
> instantiate an abstract terminating function (that is, any "val" without an
> explicit "diverges" clause) with a potentially diverging implementation. And
> this is no more the question of usability but of correctness.
sure, bu
-- Johannes Kanig (2014-02-10)
>
> On Mon, 10 Feb 2014 18:28:15 +0100, Yannick Moy wrote:
>> Or have a more clever warning which does not warn on "while True" loops.
>
> Yannick, If I understand correctly, the warning is supposed to be "complete",
>
kely
to happen on purpose.
> All this is to say that I'm rather
> cautious about defining what "is expected to be fine".
I'd say an infinite loop with raised exceptions and no variant should be
"fine", in the sense that this should not be an obvious cau
27;ll simply
mark all our generated "while True" loops as potentially diverging, which
should not (I hope) have any impact whatsoever on VC generation.
--
Yannick Moy, Senior Software Engineer, AdaCore
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
y do as
> you wish!
In our translation to Why3, we use "requires { true }" when there is no
explicit precondition on the Ada subprogram, but we do not end with a subgoal
of "true" in that case, so it must be discarded by the WP.
--
Yannick Moy, Senior Software Engineer, AdaCo
this work?
--
Yannick Moy, Senior Software Engineer, AdaCore
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
-- Alan Schmitt (2014-02-20)
>
> Yannick Moy writes:
>
>> Quick question to Mac users: how do you get labgtksourceview2?
>
> Through opam, by first installing gtksourceview using homebrew.
Thanks! I had gtksourceview already installed with macports, so I simply used
ing XQuartz 2.7.5 and why3 0.82. Everything is
> installed through homebrew / opam.
Not seeing it either, using X11 and the latest sources of why3.
--
Yannick Moy, Senior Software Engineer, AdaCore
___
Why3-club mailing list
Why3-club@lists.gforge
-- Yannick Moy (2014-02-21)
>
>
> Thanks! I had gtksourceview already installed with macports, so I simply used
> opam to get lablgtk-extras, and it worked! For others who have the same
> problem, here is exactly what I did, using macports+opam:
Argh! I just saw the maintai
, see the description of the position at INRIA:
http://www.inria.fr/en/institute/recruitment/offers/r-d-engineers/%28view%29/details.html?id=PNGFK026203F3VBQB6G68LOE1&LOV5=4510&ContractType=6502&LG=EN&Resultsperpage=20&nPostingID=8315&nPostingTargetID=14052&option=52&
SMT solving with
CVC4 and model checking with Kind 2. A very exciting mix!
I should also stress that Corfu must provide a rather relaxing surrounding
around this time of the year, despite the name of the school. See you there...
--
Yannick Moy, Senior Software Engineer, Ada
mponents", etc.)
2. translate your structure into a concrete Why3 type (for example a record as
in your example) and impose further restrictions with predicates applied to
specific values of the type
I think there is now a notion of type invariant in Why3 which would be more
like what you
line in
provers-detection-data.conf file, or something else?
My advice is to simply remove -rs from the Z3 entry in your local
.why3.conf generated by running why3config --detect-provers.
--
Yannick Moy, Senior Software Engineer, AdaCore
___
Why3-club ma
=%S %f"
However, I don't think it's available yet on the command line, only through the
API.
(and BTW for Why3 team, this field is not yet documented in Why3 manual at
http://why3.lri.fr/doc-0.85/manual011.html#sec117)
--
Yannick Moy, Senior Software Engineer, AdaCore
_
he SPARK User's Guide at
http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html#how-to-investigate-unproved-checks
<http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html#how-to-investigate-unproved-checks>
I believe Why
https://hal.inria.fr/hal-01314885
<https://hal.inria.fr/hal-01314885>
or the longer research report: https://hal.inria.fr/hal-01271174
<https://hal.inria.fr/hal-01271174>
Maybe David you may want to give additional info on how to use counterexamples
in Why3 that is not given curren
rexamples in SPARK is that we generate a special
VC just for counterexample (not for proof) using a modified CVC4 driver, that
forces the logic to AUFLIRA. Then CVC4 emits an error when a nonlinear
arithmetic operation is found, but at least we get counterexamples when no suc
pens in
your case. But this is not coming from your file, so from int.Int? Can you look
at the SMT2 file generated to see where it uses non-linear arithmetic? That's
strange, as we do use import int.Int like this in SPARK, without any problem.
--
Yannick Moy,
asily generated. The problem then is that it may likely
be a spurious one. I believe the notions of soft/hard time limits that we
proposed in our article is better, as it's easy for the prover to check that
current ground terms do not contradict the counterexample. But this has not
made it so
be expanded. On the contrary,
> "let" is an "opaque" function definition only seen through its contract.
> It can have side effects.
>
> Am I correct?
AFAIK, yes.
--
Yannick Moy, Senior Software Engineer, AdaCore
___
"command" field, you may not need the
"command_steps" field in your case)
--
Yannick Moy, Senior Software Engineer, AdaCore
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
.
But it just answers with:
$ why3 prove -P Eprover quantarrays.mlw
Unknown printer 'tptp-fof'
Do you get this error when calling TPTP provers?
Should I configure why3 differently?
Thanks in advance.
--
Yannick Moy, Senior Software Enginee
t;/lib/why3/plugins/tptp" in my source or
installed why3 directory.
How do I get this created? Is it a special argument to configure?
TIA
--
Yannick Moy, Senior Software Engineer, AdaCore
___
Why3-club mailing list
Why3-clu
-- Yannick Moy (2017-11-14)
> indeed, why3config did not generate the "plugin" line.
> But in any case, I have no such "/lib/why3/plugins/tptp" in my source or
> installed why3 directory.
> How do I get this created? Is it a special argument to configure?
Forge
binary could be all Apache 2.0, and that you can just avoid
distributing the non-Apache prelude files to get a free software version.
Mohamed, do you confirm that?
--
Yannick Moy, Senior Software Engineer, AdaCore
___
Why3-club mailing list
W
? we might need to mark all the generated Why3 code
as ghost then.
--
Yannick Moy, Senior Software Engineer, AdaCore
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
If indeed Why3 as a source language benefits from
different choices than Why3 as an intermediate language, I suggest the
introduction of a "mode" to switch between these two ways to use Why3.
--
Yannick Moy, Senior Software Engineer, AdaCore
_
-- Claire Dross (2018-07-26)
No, the polymorphism encoding didn't change at all, so everything
should still be there, see François' reply.
>
> I don't see his reply, were is it? On Why3 list?
yes to why3-club@
___
Why3-club mailing list
Why3-
rch-corner-proving-security-of-binary-programs-with-spark
<https://blog.adacore.com/research-corner-proving-security-of-binary-programs-with-spark>
I cannot comment on the assessment of your professor, I suggest you discuss
with him/her the rationale for his assessment?
Hope that help
It's called What4:
https://galois.com/blog/2020/07/what4-new-library-to-help-devs-build-verification-program-tools/
:-)
Of course, no successor here, only an homage to Why3 in picking the name of
their tool for addressing different SMT solvers from Haskell code.
--
Yannick Moy
Senior Sof
congrats Why3 team:
https://systematic-paris-region.org/presse/why3-laureat-du-prix-coup-de-coeur-academique-du-hub-open-source-du-pole-systematic/
well deserved if you ask me. :-)
and I totally approve your choice of funding Wikimedia and Framasoft with
the prize.
--
Yannick Moy
Senior Software
32 matches
Mail list logo
