[SystemSafety] systemsafety Digest, Vol 75, Issue 24

[Rod Chapman]

 >The  only way a static analyser can cope with this is to check under
every
>order of evaluation that the compiler permits. I'm not aware of any that
>do that for C but AFAI am aware the SPARK tools do it for Ada.

That's not quite the way it works in SPARK.  I don't know of any SV tool
that attempts to analyse "every order of evaluation", since that would
be (in the worst worst case) O(2**N).

In SPARK, any evaluation order is allowed, but the rules of the language
are such that any evaluation order always yields the same result. This
avoids
a potential explosion in analysis time and complexity, and also means that
SPARK
works with any compiler, no matter what choice it makes.

There are subtleties to do with overflows and equal-precedence operators,
but I won't bore this group with all the details..
 - Rod
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20181022/a181a0fd/attachment.html>