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