Re: [seL4] Autocorres Error.

Hi Dan, thanks for the bug report. AutoCorres printed this message while trying to come up with a variable name for the result of if (it->src == node) { return 0; } else { break; } However, this code never returns (returnOk in the exception monad), and AutoCorres fails to detect this. Unfortunately, fixing this issue properly is a bit difficult. You can pass keep_going, which will leave the result with the unusable name “uu_” — this should be fine because you shouldn't need to refer to it. Another workaround is to remove the variable using a rewrite rule (add this before running autocorres): lemma [L2opt]: fixes C L R S I A shows "L2_seq (L2_condition C (L2_throw L I) (L2_throw R A)) S = L2_condition C (L2_throw L I) (L2_throw R A)" apply (monad_eq simp: L2_defs) apply blast done Hope this helps. -- Japheth ________________________________ 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.