y case the loop expression actually
contains a raise expression.
--
Johannes Kanig
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
t news. Completely interchangeable, as in
assert { True }
and
function b : bool = true
?
Johannes
--
Johannes Kanig
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
milar) was guaranteed to
work and not suppress VCs, we could get rid of "keep_on_simp".
What do you think?
--
Johannes Kanig
simp.mlw
Description: Binary data
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
which function/statement belongs a given warning? Not
something that we want to tackle right now.
--
Johannes Kanig
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
verge. You are talking about a more
heuristic warning.
--
Johannes Kanig
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
a ref;
* I would prefer to not have this warning.
What do you think?
--
Johannes Kanig
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
at right?
I'm not sure, in any case it never came up up to now. So I would say do as you
wish!
Johannes
--
Johannes Kanig
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
s*
used!), and I would prefer not to have it, or some way to disable it.
--
Johannes Kanig
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
ut I don't see a deficiency of Why3 to fix in this
example.
I agree that's the real issue here.
--
Johannes Kanig
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
n,
* a VC, even if it is simply "true", when there is a precondition, and the call has a
"keep_on_simp" tag.
No urgency of course, just wanted to let you know our preference.
Best,
Johannes
--
Johannes Kanig
___
Why3-club mailing list
W
On Mon, 03 Mar 2014 10:02:19 +0100, Johannes Kanig wrote:
I was confused - we would indeed want to make the distinction you describe:
And attached is a file which describes the issue: currently Why issues a VC on
the call, although it doesn't have a precondition.
Best,
Joh
(e.g. on libre.adacore.com). There
should be no problem to have two installs of why3 on a system, as long
as they are not installed in the same place.
--
Johannes Kanig
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http
Oh, as a side note, I think the INSTALL instructions may be out-of-date.
It seems the correct install target is now "install-all", not "byte
install-lib"
To which INSTALL instructions are you referring?
Thanks for your efforts,
Johannes
--
Johannes Kanig
_
ac45b;hb=HEAD
OK, then that's for the upstream Why3 people to fix.
--
Johannes Kanig
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
ork.
Johannes
--
Johannes Kanig
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
l it "why3-spark2014" or some such.
2) it would be best not to have this package at all, it is useless in
itself and only useful as a component of SPARK 2014.
You are free to do whatever you want, of course.
--
Johannes Kanig
___
Why3-club ma
because ...
Where is prover_result defined? How am I supposed to access the
proof_attempt_status?
... you can find that type in the file /src/driver/call_provers.ml[i]
--
Johannes Kanig, PhD
Senior Software Engineer
___
Why3-club
the context;
* axiom: does not generate a proof obligation, will appear in the context.
Johannes
--
Johannes Kanig, PhD
Senior Software Engineer
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club
an be easily removed (e.g.
prenex quantifiers in the goal).
With Why3, it is relatively hard to produce goals without quantifiers,
so in most cases the prover will say "unknown" instead of "sat".
--
Johannes Kanig, PhD
Senior Software Engineer
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
using sessions? If not, you can just replace your
pids by the "prover_call" type of call_provers.mli. The call_on_*
functions of that file (and the more high-level ones of driver.mli)
return immediately, so they are suitable for running provers in parallel.
--
Johannes Kanig, PhD
Senio
rguments for that process, e.g. using "ps" if still
running, or using strace?
- what happens if you run that process by hand using the same arguments?
Best,
Johannes
--
Johannes Kanig, PhD
Senior Software Engineer
___
Why3-club mailing lis
ub.com/AdaCore/why3
- see the contents of the old transformation:
git show 9bed9dea98f532afdf6eebfb3545ab7c58493daa:src/transform/gnat_float.ml
But note that the code is from 2015, so it probably won't compile with
today's Why3 and requires some modification.
--
Johannes Kanig, PhD
22 matches
Mail list logo
