dialyzer: will it ever catch out of bounds errors like this?

[Tobias Lindahl]

In Dialyzer lists are collapsed to include the contents and the 
termination. The length of a list is not recorded, only if it is a 
non-empty list.

Roger Larsson wrote:
> -module(bounds).
> -export([wrong/0, harder/1]).
> 
> wrong() -> lists:nth(4, [1, 2, 3]).

This could probablybly be caught by a special case for constant lists, 
but currently it is not.

> triple(X) -> lists:duplicate(3, X).
> harder(X) -> lists:nth(4, triple(X)).

This is not caught since the return type of triple/1 is [any(),...] 
which indicates a non-empty list containing anything. The information 
that it is of length 3 is not recorded.

In general I do not think that a more precise list type would be worth 
the extra work (both for the analysis and for me ;-). I have been 
thinking about using a list type that explicitly captures the cons-cells 
up to a limit and then abstracts into the current representation, but 
typically the only time this kind of information would be found is in 
small constructed examples such as the one above. Recursion over lists 
most often do not have a limit on the size of the list, and the input 
list is seldom a constant outside the wonderful world of benchmarks.

Best,
Tobias

> 
> 
> As wanted in "The Next Mainstream Programming Language"
> http://www.st.cs.uni-sb.de/edu/seminare/2005/advanced-fp/docs/sweeny.pdf
> (Haskell for Next Generation Games)
> 
> /RogerL