Glad to clear that up. Thanks to Tom for raising that point: C "assert" is indeed stripped in the preprocessing phase for the production kernel, but "halt" isn't. It's the design-level (Haskell) assertions we prove don't fail.
Cheers, Gerwin > On 28.01.2015, at 2:29 pm, David Greve <david.gr...@rockwellcollins.com> > wrote: > > On Tue, Jan 27, 2015 at 5:43 PM, Thomas Sewell <thomas.sew...@nicta.com.au> > wrote: > > > There's a bit of history. > > There always is .. > > > We did discover once, after verification, that one of the > > C assertions was wrongly transcribed from its Haskell > > counterpart, so the debug build of the kernel could > > panic in a situation where nothing was actually wrong. > > That is an interesting story. > > > Well, that's probably more details than you ever wanted to know. > > Actually, this is precisely why I asked. > > Thanks, > Dave > > _______________________________________________ > 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
