21 Jun
2016
21 Jun
'16
6:05 p.m.
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
21 Jun
21 Jun
6:39 p.m.
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(a)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(a)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.
7:22 p.m.
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(a)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(a)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(a)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. 
24 Jun
24 Jun
5:42 a.m.
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.
2157
days inactive
2160
days old
3 comments
3 participants
participants (3)
-
Dan DaCosta -
Gerwin Klein -
Japheth Lim