Dear Andrei,
many thanks for your quick answer. I finally succeeded in modifying my files to
release 1.2.0 … BUT I now have:
- many xxx.contents in my text to translate an xxx Appset into a xxx Set :-(
- to define a virtual ‘selements’ function to have a code version of the
‘elements’ function
Dear Jean-Jacques,
"val constant nn : int" should do the trick.
Best,
Andrei
On Mon, 25 Mar 2019 at 17:54, Jean-Jacques Levy
wrote:
> Dear Why3 Friends, in release 1.2.0, I cannot have global constants in
> code.
>
> module Test0
>
> constant nn: int
>
> let ma
Dear Why3 Friends, in release 1.2.0, I cannot have global constants in code.
module Test0
constant nn: int
let main() = nn
end
File "bb.mlw", line 5, characters 13-15:
Logical symbol nn is used in a non-ghost context
-
On Mon, 25 Mar 2019, Andrei Paskevich wrote:
> Commited in 5e93e6d7 in master. You can put the attribute [@inline:trivial]
> over the predicate symbol (right after the name) or over its definition
> (right before the formula). The symbol will be inlined automatically for the
> majority
> of t
Commited in 5e93e6d7 in master. You can put the attribute [@inline:trivial]
over the predicate symbol (right after the name) or over its definition
(right before the formula). The symbol will be inlined automatically for
the majority of the automated provers via their drivers. Alternatively, you
ca
On Mon, 25 Mar 2019, Andrei Paskevich wrote:
> Hi Julia,
>
> would it help to label such predicates explicitly in order to always inline
> them when passing the task to a prover (as you suggested in an earlier mail)?
> I am inclined to add this functionality to the "inline_trivial"
> transfor
*Frama-C & SPARK Day 2019 : Formal Analysis and Proof
for Programs in C and Ada*
Date: Monday June 3rd, 2019
Location: Paris, La Fabrique Événementielle, 52 ter Rue des Vinaigriers,
75010
This one-day workshop aims at gathering both academic and industrial
users of the en
Hi Julia,
would it help to label such predicates explicitly in order to always inline
them when passing the task to a prover (as you suggested in an earlier
mail)? I am inclined to add this functionality to the "inline_trivial"
transformation. One downside of this is that the predicate is not inli
My natural inclination is to make predicates that combine other
predicates, in order to avoid massive code duplication. But it seems that
doing so makes it very hard for why3 to find the information it needs. So
to get the proof to go through, I have to manually inline the predicates,
which clutt
