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 <david.greve@rockwellcollins.com> wrote:

  Are they generated automatically from Haskell code?

On Tue, Jan 27, 2015 at 3:31 PM, Gerwin Klein <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 <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.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.systems
https://sel4.systems/lists/listinfo/devel