Make code generation more compliant with Frama-C.

[lambdaxdotx]

• Use Frama-C project to enable analysis chaining.
• Register globals in Frama-C tables.
• Compute CFG for the generated function.
• Use pointer arithmetic for array in loop since type is TPtr.

[lambdaxdotx]

I admit this is a more controversial PR than the previous ones.

Indeed, you may not want to ensure Frama-C compliance wrt the generated AST since ldrgen does not need to. That being said, at the moment, the generated AST is not "correct", and in particular, whenever one wants to chain another Frama-C analysis on the generated code, a crash is very probable.

This PR makes the AST more correct in that sense, and allows analysis chaining w/o apparent problems. Well, to be fair, computing the CFG for the generated function makes appear an undesired/useless statement of the form label: ; after every while loop. I did not find the cause of this, it may be a problem in the way the code is generated or a Frama-C bug (I would dare to say, less likely).

In the case you are interested in this PR in general, but are annoyed by the problems it raises, I could try to make the changes needed more by Frama-C than ldrgen itself conditional to some command line option (say, -fc-compliant?). It might be possible, it might.

Let me know if you need more details about the code changes.

[gergo-]

Looks good, I'm happy to have better compatibility with Frama-C.
It looks like the spurious break labels are introduced by CFG.prepareCFG. In my opinion it would be better if these weren't generated for loops that have no breaks, but I don't really mind.

[lambdaxdotx]

It looks like the spurious break labels are introduced by CFG.prepareCFG. In my opinion it would be better if these weren't generated for loops that have no breaks, but I don't really mind.

I agree, having such spurious labels is not perfect.

For sure, they are introduced by CFG.prepareCFG. The question is: is it a bug in CFG or rather a correct behavior in the presence of a malformed AST (hence, a ldrgen bug)? I didn't quite get if you think more of the former.

Anyway, I could open an issue to record such problem for the future once this PR gets merged.

[gergo-]

For sure, they are introduced by CFG.prepareCFG. The question is: is it a bug in CFG or rather a correct behavior in the presence of a malformed AST (hence, a ldrgen bug)? I didn't quite get if you think more of the former.

I think the core issue is in CFG. But if it's easy to work around it in ldrgen and harder to change CFG, then I'm fine with a workaround/fix/whatever we want to call it here.

Anyway, I could open an issue to record such problem for the future once this PR gets merged.

Please do.