Frama-C Bug Tracking System - Frama-C
View Issue Details
0000680Frama-CPlug-in > Evapublic2011-01-20 15:052011-10-10 14:14
Frama-C Carbon-20101202-beta2 
Frama-C Nitrogen-20111001 
0000680: Use of Cabs2cil.fresh_global
A few functions in the value analysis (Eval.initialize_var_using_type, Eval.return_value, Eval.compute_call), as well as Builtins.frama_c_alloc_infinite call the function Cabs2cil.fresh_global. Since it is a global hashtable that is never reset, successive executions of the value analysis will yield different results over time. This causes convergence problems for, eg. fixpoint-based plugins.
No tags attached.
Issue History
2011-01-20 15:05yakobowskiNew Issue
2011-01-20 15:05yakobowskiStatusnew => assigned
2011-01-20 15:05yakobowskiAssigned To => pascal
2011-01-21 00:35pascalNote Added: 0001401
2011-01-24 12:55monateNote Added: 0001414
2011-01-24 12:58monateNote Added: 0001415
2011-01-24 13:00yakobowskiNote Added: 0001416
2011-02-24 14:41yakobowskiNote Added: 0001531
2011-07-06 14:50yakobowskiNote Added: 0002015
2011-07-06 14:52yakobowskiNote Added: 0002016
2011-07-06 14:52yakobowskiStatusassigned => resolved
2011-07-06 14:52yakobowskiFixed in Version => Frama-C GIT, precise the release id
2011-07-06 14:52yakobowskiResolutionopen => fixed
2011-10-10 14:13signolesFixed in VersionFrama-C GIT, precise the release id => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

2011-01-21 00:35   
This is what happens when you try to write any programs not in Haskell. You end up with side-effects. Work-around: rewrite Frama-C in Haskell.
2011-01-24 12:55   
@boris: Do you mean that Cabs2cil.alphaTable should be projectified?
2011-01-24 12:58   
By the way alphaTable is cleared by startFile. This means that exporting Cabs2cil.fresh_global is probably not safe: clashing identifiers might be produced when many files are parsed in sequence. I'm not sure I know how to produce a real bug because of that, but this seems possible.
2011-01-24 13:00   
Actually what I really need is that the plugins clear the names they have used when their analyses are cleared, so that they can be reused. Projectification would not be sufficient.
2011-02-24 14:41   
After further investigation, the most problematic case stems from the use of fresh_global to generate "alloced_return_" variables. Those are actually memoized, and are generated only once. However, the memoization is reset with the value analysis, and I think this is overkill. Technically, I propose making Eval.Leaf_Table.self depend on Ast.self instead of Db.Value.self.
2011-07-06 14:50   
I'm going to implement what I suggested in my last note. The only observable difference would be for someone who: - launches VA more than once on the same AST with different options - merges some of the results of the successive analyses - does not stub all its functions It is not clear that such a user exists. Moreover, he should be happier with the new behavior, as the results will be easier to merge.
2011-07-06 14:52   
Actually this was committed by accident in revision 12161... Sorry for the noise.