Software Assurance Reference Dataset

Andrei Alexandrescu via Digitalmars-d digitalmars-d at puremagic.com
Thu Jun 26 21:26:23 PDT 2014


On 6/26/14, 5:29 PM, Timon Gehr wrote:
> On 06/27/2014 01:47 AM, Andrei Alexandrescu wrote:
>> On 6/26/14, 4:16 PM, Timon Gehr wrote:
>>> ...
>>>
>>> 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).
>
> I don't think it makes sense to imply that I am defending an extreme
> position. I wasn't discussing design choices, truth is not a continuum
> and I was just objecting to the line of reasoning that went like
> "undecidability of the halting problem implies that formal reasoning is
> pointless.", which is clearly untrue.

I agree.

>> My understanding is that it can be done
>> but only with annotations or whole program analysis.
>> ...
>
> Any way it is done, it doesn't come for free.

That's not a fair characterization. Interprocedural analysis is quite a 
different ball game from classic semantic checking.


Andrei



More information about the Digitalmars-d mailing list