Deduplicate generated code for header files
Currently the type definitions in header files are duplicated for each C file that the header is included in. This leads to problems when one want to prove additional lemmas about these definitions (e.g. a new subtyping rule) as the lemma will talk about a different definition of the same type and thus not apply.
Idea: In rcgen, when generating a type definition, lookup from which file the definition comes from. If it comes from a .h file, generate a (..._h_spec.v
?) file next to the .h file. Import the ..._h_spec.v
file from the ..._c_spec.v
file generated for the .c
file.
Problem: Which files should the ..._h_spec.v
file import? Probably some other header files, but which? Or should we call rcgen
once on the .h
file and once on the .c
file instead of only on the .c
file?