How to get length of array in boogie code?

[Luweicai]

I want to get the lenght of array in boogie code so I can write some checking like the arr a; assert (for all 0 <= x < arrlen(a), a[x] meets some property).
I find the $Arraylength function in ModifiedBag.bpl. However, the boogie code I generate from .c file do not have such function.
Such a .c file could be like

void tt(int *a, int b, int arr[]){
	a[2] = b;
	arr[2] = b*2;
}

I wounder how can I get the $Arraylength function or is there any other solutions to meet my requirement.

[bkragl]

In Boogie, arrays (and more generally, maps) don't have a length. You can read from and write to any index. If you read from an index that was not written before, then you just get a nondeterministic value, meaning the value is completely unconstrained so you cannot assert anything nontrivial about it.

If you want to reason about bounded arrays or memory allocation in Boogie, you need to explicitly model that. You mentioned C, where arrays are treated as pointers that don't carry the number of array elements, so you typically see the length passed as an additional argument to functions. You might be able to use such parameters for the range in your assertions. Note however that Boogie does not check that the length parameter is correct. That's again something you'd have to model in your translation to Boogie.