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

--