2021-02-24 19:19 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000680Frama-CPlug-in > Evapublic2011-10-10 14:14
Assigned Topascal 
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000680: Use of Cabs2cil.fresh_global
DescriptionA 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.
TagsNo tags attached.
Attached Files




pascal (reporter)

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.


monate (reporter)

@boris: Do you mean that Cabs2cil.alphaTable should be projectified?


monate (reporter)

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.


yakobowski (manager)

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.


yakobowski (manager)

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.


yakobowski (manager)

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.


yakobowski (manager)

Actually this was committed by accident in revision 12161... Sorry for the noise.

-Issue History
Date Modified Username Field Change
2011-01-20 15:05 yakobowski New Issue
2011-01-20 15:05 yakobowski Status new => assigned
2011-01-20 15:05 yakobowski Assigned To => pascal
2011-01-21 00:35 pascal Note Added: 0001401
2011-01-24 12:55 monate Note Added: 0001414
2011-01-24 12:58 monate Note Added: 0001415
2011-01-24 13:00 yakobowski Note Added: 0001416
2011-02-24 14:41 yakobowski Note Added: 0001531
2011-07-06 14:50 yakobowski Note Added: 0002015
2011-07-06 14:52 yakobowski Note Added: 0002016
2011-07-06 14:52 yakobowski Status assigned => resolved
2011-07-06 14:52 yakobowski Fixed in Version => Frama-C GIT, precise the release id
2011-07-06 14:52 yakobowski Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version Frama-C GIT, precise the release id => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History