My Frama-C plug-in creates some varinfos with makeGlobalVar ~logic:true name type
. These varinfos do not exist in the AST (they are placeholders for the results of calls to allocating functions in the target program, created “dynamically” during the analysis). If my plug-in takes care not to keep any strong pointer onto these varinfos, will they have a chance to be garbage-collected? Or are they registered in a data structure with strong pointers? If so, would it be possible to make that data structure weak? OCaml does not have the variety of weak data structure found in the literature for other languages, but there is nothing a periodical explicit pass to clean up empty stubs cannot fix.
Now that I think about it, I may not even have to create a varinfo. But it is a bit late to change my plug-in now. What I use of the varinfo is a name and a representation of a C type. Function makeGlobalVar
offers a guarantee of unicity for the name, which is nice, I guess, as long as it does not create a strong pointer to it or to part of it in the process.
Context:
Say that you are writing a C interpreter to execute C programs that call malloc()
and free()
. If the target program does not have a memory leak (it frees everything it allocates and never holds too much memory), you would like the interpreter to behave the same.
If you don't explicitely register the varinfos into one of the
Globals
table, Frama-C won't do it for you (and in fact, if you do, you're supposed to add their declaration in the AST and vice-versa), so I guess that you are safe here. The only visible side-effect as far as the kernel is concerned should be the incrementation of theVid
counter. Note however that makeGlobalVar itself does not guarantee the unicity of thevname
, but only of thevid
field.