Flags interaction

[paulineb30]

The properties checked for two check flags is not equal to the sum of the properties checked for the first flag and the properties checked for the second flag. For example, the set of properties generated by:

cbmc myfile.c --pointer-check --bounds-check --show-properties

Is larger than to the union of these two sets:

cbmc myfile.c --bounds-check --show-properties
cbmc myfile.c --pointer-check --show-properties

Which can be misleading.

[martin-cs]

On Wed, 2016-09-07 at 00:23 -0700, pbolignano wrote:

The properties checked for two check flags is not equal to the sum of the properties checked for the first flag and the properties checked for the second flag.

This is correct but note that the properties checked by two flags
will /include/ the properties checked by each.

For example, the set of properties generated by:

cbmc myfile.c --pointer-check --bounds-check --show-properties

Is larger than to the union of these two sets:

cbmc myfile.c --bounds-check --show-properties
cbmc myfile.c --pointer-check --show-properties

Which can be misleading.

I see your point but ...

There are some checks which require analysis from both, so our options
are:

1. Have a third flag --bounds-and-pointer-checks which enables the extra
   checks /and/ --bounds-check and --pointer-check. This means the setting
   of flags is non-orthogonal.
2. Have the combination of --bounds-check and --pointer-check add the
   extra checks. This means the effects of flags are non-orthogonal.

I'm open to suggestions but I can't see a solution that entirely gets
around this problem. I think the best fix might be to add something to
the manual.

Cheers,

• Martin

[tautschnig]

This will be fixed via #339 and #363.