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.