Re: [CZT-Devel] adding SectWarningAnn to Z.xml - or warning annotation support for terms

[Mark U. <ma...@cs...>]

Leo

You wrote:
>
>>
>> Yes, we need to develop a standard way of handling warnings (and
>> errors) in CZT.
>>
>
> Good. I think a good place for a base architecture for those is "util".
>
>
>> So two design issues:
>> 1.  Where to put the warnings:
>>    a.  in the section manager (works well for parsing)
>>    b.  at the top of the ZSect  (or Spec?)   (what if you parse/check
>> an expr or something?)
>>    c.  at the point where the warning occurred  (a pain to search for
>> these)
>>    d.  inside the visitor that is processing the AST
>>
>
> I think those choices (a, b, c) are not necessarily exclusive.
I agree.  Different tools might want to use different approaches, or
perhaps several approaches at once.
> having it at the point of occurrence is useful (i.e. for
> Expr/Pred alone, as in rewriting rules or verification condition
> generation). Having it globally is also useful for displaying
> purposes (i.e. like in zsidekick errorlist plugin). As the
> Section manager already works well, then perhaps leaving it there
> would be a good idea.
Yes, this is sometimes *necessary*.  For example, when parsing fails, no
AST is produced, so it is not possible to attach warnings (or errors) to
the tree,
but it works well to put them in the section manager.
> On the other hand, my experience is that students and "street users"
> of CZT are not very happy with dealing with the Section manager at
> first. They do resist in using it and prefer to stick to AST visiting
> only, which is, for them, complicated enough.
Yes, when processing a single expression, the "at the point of the warning"
approach might be best.
>
> The only option I am not so sure about is the one inside visitors.
> It would imply all visitors that wanted warning support would need
> to derive from a base class (or implement the interface themselves),
> which is not always convenient.
They could just implement a "WarningHandler" interface, by providing a
single method that accepts a warning and stores it away somewhere
(eg. using approach 1-3 above, or just adding it to some internal list).

Visitor methods that generate warnings could then do this:

   if (visitor instanceof WarningHandler) {
     ((WarningHandler)visitor).handleWarning(...);
   }

>
> The idea of having some sort of WarningAnn class is that we could
> have any of the three above as needed.
>
>> 2.  Whether to have warning strings or warning objects.
>>   Our preference is to have warning objects, because it is more
>> flexible and can be easily be extended via subclassing.
>>
>
> I also agree that warning objects are better. In the end, they
> might just carry a string and that is it. We could create a
> basic interface for warnings where a method, such as "asString"
> (for human readable), is present.
>
I imagine that all warnings should include location information as well
as a message.
So if we add a WarningAnn class, perhaps it should subclass LocAnn.

Cheers!
Mark