Document [@vc:xxx] attributes
The current documentation (say http://why3.lri.fr/doc/vcgen.html) lists the possible attributes for altering VC generation: [@vc:divergent]
, [@vc:annotation]
, [@vc:sp]
, [@vc:wp]
, [@vc:white_box]
, [@vc:keep_precondition]
.
Only the [@vc:divergent]
is lightly documented with the sentence "disables generation of VC for termination".
It is desirable to document more. In particular, it should be said where these attributes should be put to have an effect. For example, [@vc:divergent]
has an effect when given as attribute to the body of a function. Is it the only place it has an effect?
Other cases include [@vc:white_box]
and [@vc:keep_precondition]
: where should these attributes be put to have an effect? And what effect exactly? For example, is it possible to put an attribute like [@vc:keep_precondition]
on a function contract to tell that precondition should be kept for all calls to this function? Or should it be put on individual function calls?
An example for each of these attributes would be welcome.
Side question: is the attribute [vc:white_box]
able to answer the question on the Zulip about inlining a function call in a VC computation ?