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