> Yes, we could do that.  Though a simpler form may be preferable, like
> directly specifying a constant range/anti-range instead of encoding these
> in (multiple) ASSERT_EXPRs.
>
> I will think of something.

Thanks.

> As for Ada - both function entry and exit constraints will be checked by
> the caller/callee, correct?  So that once you inline VRP should be able
> to derive the ranges from existing checks?  Thus - a IPA VRP pass should
> be able to verify these properties across functions?

No, the model used by GNAT is "lazy" validity checks: the various validity 
checks are emitted just before uses of the value that are deemed sufficiently 
dangerous, as controlled by -gnatVx.  Parameter and return values are not
checked, unless explicitly requested.

VRP should be able to derive ranges when checks are present, but we would also 
need to be able to force ranges at will when checks are not present.

-- 
Eric Botcazou

Reply via email to