Software Assurance Reference Dataset

[bearophile via Digitalmars-d]

Walter Bright:

> It's an interesting list, and an opportunity for D. I once said 
> that my job was to put Coverity out of business. The more of 
> these issues D can automatically prevent with @safe, the better.

One kind of problem left is to avoid stack overflows. I have had 
several such cases in my D code (perhaps because I use 
fixed-sized arrays a lot).

I think they can be caused by:
1) Too much large allocations in stack frames;
2) By alloca();
3) By recursion and co-recursion chains;

The first cause is probably sufficiently easy to solve 
mechanically, with a conservative call tree analysis of the code. 
This is a job for external tools.

The second cause can be solved with a formal proof of the upper 
bounds of the arguments of alloca, or even more conservatively 
disallowing alloca.

The third cause, a cycle in the call graph, can be found with an 
external too, but in theory it's also easy to avoid with a 
@no_call_cyles annotation :-) Such annotation looks useful only 
if you want to avoid stack overflows, so it's better to use a 
more general annotation that also forbids alloca(). Something 
like @fixed_stack or @constant_memory.

I think adding this annotation to D is a little overkill (despite 
SPARK and Ada analysers are doing stack size analysis since many 
years). So I think a better solution (beside creating an external 
tool) is to add to D a more general feature to attach some 
compile-time semantics to user-defined annotations. To do this 
you need a trait that returns a sequence of all the functions 
called by a function.

Bye,
bearophile