Successive calls of Cil.emptyfunction generate a Failure("trying to redefine an existing kernel function")
ID0000831: This issue was created automatically from Mantis Issue 831. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000831 | Frama-C | Kernel | public | 2011-05-20 | 2012-06-10 |
| Reporter | ploc | Assigned To | virgile | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
Cil.emptyFunction relies on makeGlobalVar, that calls makeVarinfo to build a new varinfo. This varinfo has vid = -1, but the function set_vid from Cil_const is called that provides a fresh vid to it, using the Build_Counter (register with Computation.Ref).
The issue is the following: working in a project, I introduce a new function when applying a cil copy visitor. Then on the new project I introduce another new function. The problem is that the two successive calls to Cil.emptyfunction will provide the same vid.
The project created through the cil copy visitor will not keep the Computation.Ref Build_Counter. So the successive introductions of new function will be associated to the same vid.
Is there a way do solve this ? How to copy the Build_Counter information in the new project ? Or is there nicer way to handle this ?