You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
While we have mostly used verse to generate code, it would be good if the verse also generates some
minimal documentation and header files for easy integration with outside projects. Here I collect some of
these information that can be useful.
Doxygen or some other documentation
Function prototypes
Header files
Somehow lift the names in Coq source to names in C code. Might need some tactics
For assembly code, annotate with the corresponding verse instruction.
Frama-C annotations for safety of the generated C functions.
The text was updated successfully, but these errors were encountered:
While we have mostly used verse to generate code, it would be good if the verse also generates some
minimal documentation and header files for easy integration with outside projects. Here I collect some of
these information that can be useful.
The text was updated successfully, but these errors were encountered: