[C-safe-secure-studygroup] Code that is useless in normal situations: proposed classification

Roberto Bagnara bagnara at cs.unipr.it
Wed May 3 16:47:50 UTC 2017


Related to the current discussion on MISRA-C:2012
Rule 1.3, I would like to propose a finer classification.
Code may be:

Unreachable:
  The code is not evaluated for purely syntactic reasons,
  i.e., its nodes in the control-flow graph are not connected
  to any root node.

Unfeasible:
  The code is not unreachable, but it is not evaluated because
  no actual control flow that leads to it can be followed.
  (According to the descriptions in MISRA-C:2012 pages 40-41
  and 225-226, MISRA-C:2012 calls this "unreachable" as well.)

Effectless:
  Not unfeasible, but the evaluation is redundant as it has no
  side effects.

Dead-effects:
  Not effectless, but its effects do not change the program semantics.

This way we have a quadri-partition of the broad informal category
of "code that is useless in normal situations" that, I believe,
is precise and useful.
Kind regards,

   Roberto

-- 
     Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                              BUGSENG srl - http://bugseng.com
                              mailto:roberto.bagnara at bugseng.com

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2093 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://lists.trustable.io/pipermail/c-safe-secure-studygroup/attachments/20170503/636e4c70/attachment.bin>


More information about the C-safe-secure-studygroup mailing list