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 <[email protected]> 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 <[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
