In general Spark mode can be straight forward (atleast for Silver) but appears to be more work than it is worth for any file that withs a lot of volatiles like those generated by svd2ada.
Would you agree or encourage me to persevere across the learning curve?
Is codepeer a good alternative in this case?
I suppose that it depends if you can tweak the generator to generate SPARK code or not. Reads of volatile data are an effect in SPARK, hence are syntactically restricted to be directly on the lhs or rhs of assignments (the complete variable or a path from it), and not as part of a more expression. This and the fact that functions that read volatile data must be Volatile_Function, and also can’t have an effect. For more details, you can see a course on that topic.
CodePeer’s goal is different from SPARK, as it tries to detect bugs instead of giving guarantees about properties of the program (like absence of runtime errors or functional behavior).
Thankyou. I had implemented some of that shown in the link once before but certainly needed to recap, however I was really thinking.
Driver code is often quite simple but might need extra information adding to set a max loop count on say a hw status flag dependent while loop. Otherwise I guess sparks flow information shall be incomplete. Then there is all the volatility changes. I tried to isolate the data handling but that was fairly problematic.
However there may be an exit loop when the array is full in any case. Would codepeer see that and confirm that a runtime exception from constraint error is unlikely, if not proven?
My goal is runtime exception avoidance and not formal verification.
The alternative is just to handle the exception and log the event but catching bugs before they happen would be nice.
With SPARK, you can include the bound information in the type of your volatile data, or check that it fits the bounds of a given subtype (after storing it in a temporary variable to be able to do this check, and then do the loop on the value of the temporary).
CodePeer is less predictable when it comes to loops, as it works with heuristics, and is also not meant to report all possible errors like SPARK.
I wonder if volatility matters to mode Silvers absense of runtime errors 