If we drop the restriction that the pointer, or the array index, be fixed at compile time, then there must be enough bounding information in context to ensure we still have a valid dereference. A contrived example is as follows:
int
foo(int index)
{
int k = 0;
return *(&k+index);
}
Evidently foo(x) is only valid when x is 0.
Similarly, in
bar(int index, int value)
{
int arr[50];
arr[index] = value;
}
we have bar(x, 20) valid when x is an integer in [0, 50).
We need semantic-abstract notation to capture these requirements.
Because foo is so basic, we can express its assumptions with the following:
int
foo(int index) ~ [ setup: index = 0; ];
In bar's case our current repertoire of setup-statements does not appear to be sufficiently powerful.
Perhaps we should introduce a range operator:
bar(int index, int value) ~ [ setup: index = 0:50; ];
We could remove $ and have : represent an arbitrary value of the type.
If we drop the restriction that the pointer, or the array index, be fixed at compile time, then there must be enough bounding information in context to ensure we still have a valid dereference. A contrived example is as follows:
Evidently
foo(x)is only valid whenxis0.Similarly, in
we have
bar(x, 20)valid whenxis an integer in[0, 50).We need semantic-abstract notation to capture these requirements. Because
foois so basic, we can express its assumptions with the following:In
bar's case our current repertoire of setup-statements does not appear to be sufficiently powerful.Perhaps we should introduce a range operator:
We could remove
$and have:represent an arbitrary value of the type.