The researchers Willard Rafnsson, Deepak Garg and Andrei Sabelfeld have recently published a paper at ESSoS 2016 conference on how to tweak the flow analysis performed in SPARK to account for the side channel of non-terminating programs. The rationale is that, currently, SPARK flow analysis does not make a difference between a program which would terminate or not depending on the value of some data. In security, where this data could be a secret key, this could allow a malicious developer to insert a backdoor to evesdrop on secrets without being caught by SPARK analysis. This work is currently not implemented, but as the researchers show in their paper, it would require only a minor modification of the existing SPARK analysis. For all details, see their paper online.