Extend safety to include portability issues

[r-ross]

The tutorial associates safety with not having C undefined behaviours, but consider extending that to other portability issues as described in ISO/IEC 9899:1999 Annex J. For example, a program relying on the values of padding bytes is relying on unspecified behavior instead of undefined behavior but is not really safe. Some of the listed portability issues would be very difficult to check so no one should expect completeness, but finding as many as reasonably possible can help avoid scenarios where "it works for me" and "it works for the rest of the team" yet "it blows up in the customer's face."

[dc-mak]

Is this an issue for the tutorial wording, or for CN as a proof tool? Because CN does tend to take a conservative stance to such issues, or make it explicit (for example, endianness).

[r-ross]

Tutorial wording based on what CN is intended to check in the absence of user-defined specs. For example, integer overflows are reported since they are undefined behavior according to C standards, but what other portability issues are expected to be covered?

[dc-mak]

CN is an academic research project under active development, with limited resources. We aim to be about as comprehensive as the underlying Cerberus frontend (https://www.repository.cam.ac.uk/handle/1810/350157) but do not currently maintain a list of which portability issues we cover, and how. If you are interested in this information, and are willing to compile it, then we can point you in the right direction.