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.
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
