Software Assurance Reference Dataset

[Andrei Alexandrescu via Digitalmars-d]

On 6/26/14, 4:16 PM, Timon Gehr wrote:
> - Annotations can include a formal proof.

If a function can be annotated with what other functions it calls
(non-transitively), I agree that it can be guaranteed with local
semantic checking that a program won't overflow. However requiring such
annotations would be onerous, and deducing them would require whole
program analysis.

> We've had similar discussions before. Why do we _still_ have to argue
> about the _possibility_ of having a system that is helpful for
> proving stack overflows (or other bad behaviours) absent?
>
> You can say "out of scope" or "not a priority" or "this should be
> realized in third-party tool support" but not "it is impossible".

I also seem to reckon Walter is in the other extreme (he asserts it 
can't be done at all, period). My understanding is that it can be done 
but only with annotations or whole program analysis.


Andrei