Hi Claude,
Le 04/02/2019 à 11:08, Claude Marché a écrit :
We didn't try such kind of mappings. I can't answer on whether they
would be useful, except by trying them and evaluate the results on our
benchmarks.
Opened a ticket: https://gitlab.inria.fr/why3/why3/issues/268
Thanks, I am curio
(to_int %1)
(- (to_int (- %1"
syntax function floor "(to_int %1)"
syntax function ceil "(- 1 (to_int (- 1.0 %1)))"
remove allprops
end
Thanks for your help,
--
Claire Dross, PhD
Software Engineer
_
Hi François,
Le 25/07/2018 à 18:59, François Bobot a écrit :
Hi Claire,
Le 25/07/2018 à 17:31, Claire Dross a écrit :
I have been trying to adapt the spark tool to use the new Why3 release.
I just finished doing it for Frama-c.
I cannot say how it is going yet, I still have a long way to
It has been only (less than?) one day since the SPARK team tried to
use Why3 master: perhaps there should be more thinking about the
possible workarounds before trying to change anything in Why3.
I think everybody agrees with that, and no changes were asked. Thanks
for clarifying though.
-
On 25 July 2018 at 17:31, Claire Dross wrote:
I have been trying to adapt the spark tool to use the new Why3 release. I
cannot say how it is going yet, I still have a long way to go, but I already
have some questions:
- the "no inlining" and "lskept" metas seem to have
On 25/07/2018, Yannick Moy wrote:
-- Andrei Paskevich (2018-07-25)
This is also on purpose: the tt'int operation is used for
specification purposes, if you make it non-ghost, you would need to
link the extracted code with an arbitrary-precision arithmetic
library.
so type "int" is also ghost
Thanks Andrei for your answers.
Le 25/07/2018 à 21:51, Andrei Paskevich a écrit :
On 25 July 2018 at 17:31, Claire Dross wrote:
I have been trying to adapt the spark tool to use the new Why3 release. I
cannot say how it is going yet, I still have a long way to go, but I already
have some
Hi Why3 team,
I have been trying to adapt the spark tool to use the new Why3 release.
I cannot say how it is going yet, I still have a long way to go, but I
already have some questions:
- the "no inlining" and "lskept" metas seem to have disappear, did
they changed names or are they complet
Hi Andrei,
thank you for your answer. That is not urgent though I would use this
mechanism in SPARK as soon as it is implemented.
See you,
--
Claire
On 13/05/2016 17:30, Andrei Paskevich wrote:
Hi Claire,
the answer is "no", there is no mechanism to force inlining of a
symbol, but it won'
every occurrence of f, provided f is not recursive?
I would like to be sure before I spend to much time working on this
feature in SPARK.
Thanks in advance,
--
Claire Dross, PhD
Software Engineer
___
Why3-club mailing list
Why3-club@lists.
rting!
Best,
Andrei
Thank you Andrei for your quick fix, it seems to be working fine now.
Best,
--
Claire Dross, PhD
Software Engineer
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
e map__ref = {mutable content : map}
end
module My_Var
use map.Map
clone My_array with type map = int
val x : My_array.map__ref
end
Can you highlight me on this behavior ?
Thanks in advance,
--
Claire Dross, PhD
Software Engineer
___
Why3-club mailing
Hi Andrei,
Le 07/05/2015 10:07, Andrei Paskevich a écrit :
I would suggest adding [meta "encoding : lskept"
function singleton] right after the function definition.
Ok, thank you, I will add this to all my array axioms.
Claire
___
Why3-club mailin
used
on this example ?
See you,
Claire
Le 06/05/2015 15:11, Andrei Paskevich a écrit :
-- Forwarded message --
From: Andrei Paskevich
Date: 6 May 2015 at 14:41
Subject: Re: [Why3-club] strange translation of arrays in smtlib
To: Claire Dross
Cc: why3
Hi Claire,
the problem is
14 matches
Mail list logo
