From: Adriana Stancu <firstname.lastname@example.org>
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
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?
From: Thomas Sewell <email@example.com>
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
all the source files into a single target. The C-to-Isabelle parser runs
preprocessor, so you can do this by pointing it at a small C file that
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
in more length, if anyone really cares.
From: Yakoub Nemouchi <firstname.lastname@example.org>
Or use the better and more advanced/elegant/powerful C11-parsing framework
on a top on Isabelle which is:
From: Jaap Boender <email@example.com>
I'd definitely be interested - it's certainly a limitation we'd like to get rid
of at some point, if at all possible.
Last updated: Sep 25 2021 at 09:17 UTC