The first example has a pretty nasty typo. This:
int *arr = malloc(9);
It should of course be:
int *arr = malloc(9 * sizeof *arr);
They then go onto demonstrate how it did in those injected bug cases (really well), but they don't really get into what they found for those "out in the wild" alarms in the third-party C source. The latter seem to be more interesting than the injected bugs.
All you need to do to use Inferbo is add `-a bufferoverrun` to your normal Infer command. Inferbo isn't included in 0.9.4.1, but we'll be creating a new release soon.