With the last commit, it depends on whether you have "keep_on_simp" on
top of the function call. If it's there, there will be a subgoal for
it. If it's not, there will be none.
A.
On 12 February 2014 18:43, Yannick Moy <m...@adacore.com> wrote:
> -- Johannes Kanig (2014-02-12)
>>
>>
>>> your example. There is a catch, however. Internally, Why3 keeps a
>>> single formula for a precondition, not a list of formulas. That is,
>>> "requires { true }" is the same as no "requires" at all. I can imagine
>>> that you wouldn't want to see a subgoal "true" in your example if f2
>>> didn't have preconditions, which means that you want to distinguish
>>> the two cases. Is that right?
>>
>> I'm not sure, in any case it never came up up to now. So I would say 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, AdaCore
>
>
>
>
>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
