Email Gateway (Mar 22 2021 at 10:23): Email Gateway (Mar 22 2021 at 10:23):From: Adriana Stancu <adriana.stancu95@gmail.com>
Hello,
I am not sure if this is the right mailing list for this question: I am
using C-to-Isabelle parser to include a small C program, the structure is
as follows:
external_file "bar.c"install_C_file "bar.c"
The functions from foo.c are not parsed, only the declaration of the
functions found in foo.h.
In parser output: Added external decl for timeout_set with 2 args. Where
timeout_set is a function declared in foo.h and implemented in foo.c
How can I include also the implementation of the functions found in foo.c
when parsing bar.c?
Best regards,
Adriana Stancu
Email Gateway (Mar 22 2021 at 10:41):From: Thomas Sewell <tals4@cam.ac.uk>
It's possible that this has changed or been improved. However, when I
was working with it, the C-to-Isabelle parser needed to know the names
and types of all local and global variables in order to set up the state
type, so it needed to see all the C source.
The typical solution is simple and ugly: use the C preprocessor to
include
all the source files into a single target. The C-to-Isabelle parser runs
the
preprocessor, so you can do this by pointing it at a small C file that
simple
contains #include directives for foo.c and bar.c.
Yes, it's not ideal. There are reasons it's hard to fix which I could
explain
in more length, if anyone really cares.
Best wishes,
Thomas.
Email Gateway (Mar 22 2021 at 10:54):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Or use the better and more advanced/elegant/powerful C11-parsing framework
on a top on Isabelle which is:
https://www.isa-afp.org/entries/Isabelle_C.html
Best wishes,
Yakoub.
Email Gateway (Mar 23 2021 at 10:20):From: Jaap Boender <jaapb@kerguelen.org>
I'd definitely be interested - it's certainly a limitation we'd like to get rid
of at some point, if at all possible.
best
Jaap
Last updated: Jan 04 2025 at 20:18 UTC