Bounds checking in ranges is restricted to constant expressions.

[NlightNFotis]

As it works right now, the range bounds handling is working properly if they reduce to a clean integer constant expression, like the following:

type Int_Small is range -8 .. 8;

If the bounds are more elaborate expressions involving attributes, like this example:

type Range_Type range (Index + 1) .. Range_Type'Last;

Then gnat2goto is failing to process that node because of checks in gnat2goto_itypes.adb, function Do_Itype_Integer_Subtype that ensure that lower bound and upper bounds are constant exprs.

[chrisr-diffblue]

@NlightNFotis - My Ada knowledge is probably lacking here... but is that failing example actually valid Ada? It almost looks like it's a circular definition that attempts to defined the upper bound of a type, as the value of it's upper bound....

[NlightNFotis]

@chrisr-diffblue As it stands, the second code example shouldn't compile (it's not valid Ada). It's more of an example. The actual code listing that produces a crash is similar but it has the attribute of another object there. it looks like this:

for I in Types.Index range (Index + 1) .. Block'Last loop
...
end loop;

with Block being an array parameter to the function containing this statement.

[martin-cs]

i think there are at least three cases:

1. Bound is a constant.
2. Bound is statically determined.
3. Bound is actually variable.

I believe that we can do 1, it would not be hard to do 2 but 3 would require some work. I think 2 should be sufficient to solve this problem.