C code has extern keyword in pointer check.

[Elowen-jjw]

Example 1:

extern int arr[];

int main(){
	int *p = arr;
	int a = *p;
	
	return 0;
}

int arr[] = {1,2};

Example 2:

extern int arr[];

int arr[] = {1,2};

int main(){
	int *p = arr;
	int a = *p;
	
	return 0;
}

In Example 1, I run cbmc <filename.c> --pointer-check and cbmc gave FAILURE result with the message dereference failure: pointer outside object bounds in *p: FAILURE.

Then I moved this statement int arr[] = {1,2}; forward to get Example 2. And the pointer-check result became SUCCESSFUL.

In the two examples, p both pointed to the array arr[]. Why did pointer-check give different results? Is it releated to the extern keyword?

Please help me to explain this situation. Thanks.

CBMC version: 5.88.0
Operating system: Ubuntu 22.04, MacOS

[NlightNFotis]

When you say extern int arr[], it means that the canonical definition for the object is in a different translation unit, which you don't provide, so cbmc has no way of knowning how big the object is, and thus no way of knowing whether the access patterns within the current translation unit can violate the bounds.

[NlightNFotis]

After a bit more investigation into this, I'm going to classify this as a bug, so as to remind us to look more into this.

I have gone through:

1. The --show-goto-functions,
2. The --show-vcc
3. The --program-only
4. The --show-symbol-table

options for both of these programs, diffing them and I can't find any discernable difference between the two diffs - thus, the mechanism by which one comes successful and the other doesn't isn't apparent to me, thus requiring a deeper dive to understand the behaviour.

I believed it must be the array definition coming above the function, thus bounding the array, but having a closer look on the symbol tables/vccs of both of these, it seems that both see arr as an array of size 2, with no extern label anywhere.

Worth noting that looking at the vccs, you need to disable simplification (or at least propagation, --no-propagation) to get the vccs otherwise the simplification engine kills them.

[NlightNFotis]

Note to self: have a look at the object_size implementation in the decision procedure.

[thomasspriggs]

It is probably also worth looking at cprover_initialise function generated for these two examples. This is where I would expect initialisation of global variables to be carried out before entering the user's main() function.