CODEWITHSUNDEEP
frama-c
jobnz
jobnz

Reputation: 398

Is it possible to write the result of code transformations back to the original source files?

I would like to perform code transformations on multiple files and write the changes that result from these transformations back, ideally the original files. For example, I would like to add an if-Statement to a function funcA that originates from file fileA.c and a function funcB that is defined in file fileB.c. After performing transformations on funcA and funcB, I would like to overwrite files fileA.c and fileB.c with the resulting source code. I do not necessarily need the source code before macro expansions (I suspect this would not be possible).

Is there a sensible way of doing this using Frama-C?

Upvotes: 3

Views: 77

Answers (1)

anol
anol

Reputation: 8953

Currently, you can do it for a single file by simply writing the output to a file (with options -print and -ocode <file>), as in:

frama-c file.c [add your transformation options here] -print -ocode file.c

This will work because Frama-C reads input source files to parse them and build its AST before actually writing the output. So, by the time it truncates the original file to start overwriting it, the file has already been entirely read.

Note that, strictly speaking, this behavior could change in the future (in other words, this is not a recommended way to use Frama-C, although it should work in practice).

However, for multiple files, this is not currently possible: Frama-C always merges them all in a single, unified AST, before further processing. While the AST elements do retain location information about which source file they come from, there is currently nothing that tells the pretty-printer to output each part to a different file.

Note that, in general, this is somewhat complex: C allows multiple declarations of globals, so you can have a file a.c declaring a struct st; without specifying its fields, then another file b.c which actually declares its fields; when pretty-printing these files, you'd need to remember all the original declarations. And depending on the kind of syntactic changes that were performed, these might impact some of the declarations, but not all.

Overall, I believe it is theoretically possible to somehow tell Frama-C to remember all of those details and try to use location information to pretty-print its AST to multiple files (and if we include logic preprocessing, with ACSL annotations and such, I'm not even sure that is doable), but it would require deep changes to the kernel.

Therefore, currently, I'd say that there is no sensible way to tell Frama-C to do it, at least in the general case. For some specific subtasks related to that (e.g., pretty-printing a few select globals), it is possible to create an AST visitor that, when visiting such elements, pretty-prints them to a file whose name is related to the original name (e.g., for an AST node whose location is f.c, print it to f-out.c). But ensuring that such files are syntactically valid C in all cases makes it much more complex. And it would require at least writing a decent amount of OCaml code for a script.

Upvotes: 3

Related Questions