Hello,
I have been trying to study how seL4's C code is formally verified. So I looked into Autocorres tool and had a bit of hard time understanding how to use the tool to generate Isabelle definitions from C code. I tried to follow Autocorres' quickstart but I was confused since I do not know much about Isabelle/HOL.
I simply ran ``make AutoCorresTest" in l4v/tools/autocorres folder and it gave me this output:
``` Session Pure/Pure Session FOL/FOL Session HOL/HOL (main) Session HOL/HOL-Eisbach Session HOL/HOL-Library (main timing) Session HOL/HOL-Computational_Algebra (main timing) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Number_Theory (main timing) Session HOL/HOL-Statespace Session HOL/HOL-Word (main timing) Session Lib/Word_Lib (lib) Session Lib/Lib (lib) Session C-Parser/Simpl-VCG Session C-Parser/CParser Session Lib/CLib (lib) Session Unsorted/AutoCorres Session Unsorted/AutoCorresTest Building AutoCorresTest ... AutoCorresTest: theory AutoCorresTest.CustomWordAbs AutoCorresTest: theory AutoCorresTest.Test_Spec_Translation ... Finished AutoCorresTest (0:02:33 elapsed time, 0:08:14 cpu time, factor 3.23) ```
But I couldnt find any Isabelle definitions as output except "thy" files that contain:
``` theory somefile imports "AutoCorres.AutoCorres" begin
external_file "somefile.c"
install_C_file "somefile.c"
autocorres "somefile.c"
end ```
I suppose I need to invoke this file somehow using Isabelle in order to generate the definition but I'm not sure how to do that. Any help would be very appreciated.
Best Regards, Norrathep