Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to resolve the FUNCTION_BODY_NOT_IN_INPUT_...

Email Gateway (Apr 12 2024 at 15:57):

From: "\"DongZe Su\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi, everyone.

When using autocorres in Isabelle to analyze C functions, I encountered the
issue FUNCTION_BODY_NOT_IN_INPUT_C_FILE. How should I resolve this?

I have tried adding the corresponding function to the C file, which solves the
problem, but I do not want to disrupt the original code structure. Is there a
way to read the code from both files without moving the function?

Thanks!!

Last updated: May 05 2024 at 08:17 UTC