No, they’re manually written, so the comments themselves may be wrong or out of date. The assertions will still be proved, though.
Cheers, Gerwin On 28.01.2015, at 08:37, David Greve <[email protected]<mailto:[email protected]>> wrote: Are they generated automatically from Haskell code? On Tue, Jan 27, 2015 at 3:31 PM, Gerwin Klein <[email protected]<mailto:[email protected]>> wrote: Hi David, these comments are supposed to document that the assertion or condition corresponds to a ‘fail’ statement on the design level that we will have to prove does not occur. Cheers, Gerwin > On 28.01.2015, at 00:38, David Greve > <[email protected]<mailto:[email protected]>> > wrote: > > > What is the significance of the various "Haskell error:" comments found > throughout the kernel code? > > _______________________________________________ > Devel mailing list > [email protected]<mailto:[email protected]> > https://sel4.systems/lists/listinfo/devel ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list [email protected]<mailto:[email protected]> https://sel4.systems/lists/listinfo/devel
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
