Re: [seL4] Haskell error comments

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 mailto:david.greve@rockwellcollins.com> wrote: Are they generated automatically from Haskell code? On Tue, Jan 27, 2015 at 3:31 PM, Gerwin Klein mailto:Gerwin.Klein@nicta.com.au> 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 mailto:david.greve@rockwellcollins.com> wrote:

What is the significance of the various "Haskell error:" comments found throughout the kernel code?

_______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems 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 Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel