Howdy,
Is there a guide to the dos and don'ts of C according to the seL4 verification process? I kinda remember reading a quick summary somewhere, but can't find it on the wiki. Maybe I read it in one of the papers?
I certainly remember reading the moral equivalent of "lol no strings". ;-)
Thanks, Jeff
On 30 Nov 2016, at 14:40, Jeff Waugh jdub@bethesignal.org wrote:
Howdy,
Is there a guide to the dos and don'ts of C according to the seL4 verification process? I kinda remember reading a quick summary somewhere, but can't find it on the wiki. Maybe I read it in one of the papers?
It’s described in the original SOSP paper, but some of the restrictions may have been relaxed since, with improvements to the C parser. The main restriction beyond general good coding practice remains no passing of references to automatic variables.
You’re right, an up-to-date description on the wiki would be useful.
Gernot
-
Gernot.Heiser＠data61.csiro.au -
Jeff Waugh