Frama-C Bug Tracking System - Frama-C
View Issue Details
0000680Frama-CPlug-in > Evapublic2011-01-20 15:052011-10-10 14:14
yakobowski 
pascal 
normalminoralways
closedfixed 
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

Notes
(0001401)
pascal   
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.
(0001414)
monate   
2011-01-24 12:55   
@boris: Do you mean that Cabs2cil.alphaTable should be projectified?
(0001415)
monate   
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.
(0001416)
yakobowski   
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.
(0001531)
yakobowski   
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.
(0002015)
yakobowski   
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.
(0002016)
yakobowski   
2011-07-06 14:52   
Actually this was committed by accident in revision 12161... Sorry for the noise.