Ghost code generation

Oct 3, 2012 at 1:10 AM
Edited Oct 3, 2012 at 6:53 AM


I am trying to implement ghost code generation to facilitate verification of linked data structures (linked lists, binary search trees, etc.).

What would be the best approach to automatically generate the ghost code? 

I think I need to access and update the AST to achieve that. On which part of the VCC code base should I focus?  

The VCC code seems to have some sort of plugin management. However,  according to this discussion, the support for plugin was discontinued. Would writing a plugin be a way to go?