seL4 Developers: I apologize in advance if this is not the correct place for this email. I am experimenting with Autocorres as an intern at Rockwell Collin's Advanced Technology Center in Minnesota. My latest experiment is in building a small verified library for manipulation and analysis of adjacency lists. My initial work towards this end generated the following error: exception CTERM raised (line 948 of "~/development/rockwellcollins/verification/l4v/tools/autocorres/utils.ML"): autocorres: Internal var uu_::"int" is exposed. Please notify the AutoCorres maintainers of this failure. In the meantime, use "autocorres [keep_going]" to ignore the failure. I am using the latest version of Autocorres and Isabelle. The c and theory file that generated this error can be found here: https://github.com/chaosape/autocorresexperiments/tree/master/graph Thanks! Dan DaCosta
Hi Dan, as good a place as any to ask about the seL4 verification tools. We’ll have a look. You’re including <malloc.h> in graphs.c - which library is that from? (The problem may be coming from there). Cheers, Gerwin
On 21 Jun 2016, at 11:05 AM, Dan DaCosta <chaosape@gmail.com> wrote:
seL4 Developers:
I apologize in advance if this is not the correct place for this email.
I am experimenting with Autocorres as an intern at Rockwell Collin's Advanced Technology Center in Minnesota. My latest experiment is in building a small verified library for manipulation and analysis of adjacency lists. My initial work towards this end generated the following error:
exception CTERM raised (line 948 of "~/development/rockwellcollins/verification/l4v/tools/autocorres/utils.ML"): autocorres: Internal var uu_::"int" is exposed. Please notify the AutoCorres maintainers of this failure. In the meantime, use "autocorres [keep_going]" to ignore the failure.
I am using the latest version of Autocorres and Isabelle. The c and theory file that generated this error can be found here: https://github.com/chaosape/autocorresexperiments/tree/master/graph
Thanks! Dan DaCosta
_______________________________________________ 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.
Gerwin: In the theory file, I am using the "new_C_include_dir" to include headers files from the "seL4/musllibc" library. I suspect that this is not the answer you need though; thus far in my experiments I have only reasoned over c files that were self-contained. I am missing some understanding of what needs to be provided when reasoning over c files that make use of functions that are expected to exist in separate libraries. Thanks! Dan DaCosta On Tue, Jun 21, 2016 at 1:39 PM, Gerwin Klein <Gerwin.Klein@nicta.com.au> wrote:
Hi Dan,
as good a place as any to ask about the seL4 verification tools. We’ll have a look.
You’re including <malloc.h> in graphs.c - which library is that from? (The problem may be coming from there).
Cheers, Gerwin
On 21 Jun 2016, at 11:05 AM, Dan DaCosta <chaosape@gmail.com> wrote:
seL4 Developers:
I apologize in advance if this is not the correct place for this email.
I am experimenting with Autocorres as an intern at Rockwell Collin's Advanced Technology Center in Minnesota. My latest experiment is in building a small verified library for manipulation and analysis of adjacency lists. My initial work towards this end generated the following error:
exception CTERM raised (line 948 of "~/development/rockwellcollins/verification/l4v/tools/autocorres/utils.ML"): autocorres: Internal var uu_::"int" is exposed. Please notify the AutoCorres maintainers of this failure. In the meantime, use "autocorres [keep_going]" to ignore the failure.
I am using the latest version of Autocorres and Isabelle. The c and theory file that generated this error can be found here: https://github.com/chaosape/autocorresexperiments/tree/master/graph
Thanks! Dan DaCosta
_______________________________________________ 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.
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.
participants (3)
-
Dan DaCosta -
Gerwin Klein -
Japheth Lim