Undefined C behaviour in `vmpu_acl_update_box_region`

**_Summary**_: Bad input can cause a shift left of 32 on a uint32_t (undefined C)

Found using CBMC.
## Description

The procedure `vmpu_acl_update_box_region` (in `core/system/src/mpu/vmpu_armv7.c`) initialises a TMpuRegion for a given `box_id`, `base`, `size` and `acl`.

We check that if the procedure returns normally (without HALTing) then the region size must be non-zero. Consider the following scenario:

```
// box_id unconstrained
base = 0x0000_0000
size = 0x8000_0001
acl = 0xff00_00b4
```

In this case, `vmpu_region_bits(size)` returns 32. Then, the shift left to produce `size_rounded` is undefined (Section 6.5.7 of N1570).

In the taxonomy of [Regehr](http://blog.regehr.org/archives/213), `vmpu_acl_update_box_region` is a type-2 function (it is defined for some inputs but undefined for others). That is, an implicit assumption of the function is that it will never be called with inputs that cause undefined behaviour. This is false since parameters can be passed from an arbitrary configuration and no check is performed.

If we assume (erroneously) that the shift will result in 0 then this means that the uVisor will initialise a region of size 0 (which fails the testbench).
## Files

Can be found in the review repo under `issues/vmpu_acl_update_box_region_undefined`.
- `check_vmpu_acl_update_region.c` -- top-level testbench
- `tb_common.{h,c}` -- testbench utilities
- `run_cbmc.sh` -- script to invoke model checker
- `cex.txt` -- example counterexample output
## Reproducing

Requires:
- testbench files as above
- cbmc installed and on path
- `$UVISOR` environment variable setup to point to local copy of uVisor repo

``` bash
$ ./run-cbmc.sh check_vmpu_acl_update_box_region.c tb_common.c --ILP32 --stop-on-fail -DCEX_PRINTING | tee cex.txt && grep ">" cex.txt
```

This will produce a counterexample in [cex.txt] and a summary. This will be something like:

```
> box_id = 0
> base = 0
> size = 2147483649
> acl = 4278190260
> acl is round up = 1
> acl is round down = 0
```

Start with core/system/src/mpu/vmpu_armv7.c and the vmpu_acl_update_box_region procedure, then inspect issues/vmpu_acl_update_box_region_undefined/check_vmpu_acl_update_region.c and run run-cbmc.sh with the documented arguments. Done means the supplied counterexample no longer triggers undefined behavior and the CBMC check completes without the reported failure.

Written by the indexing model from the issue text.