2021-02-24 19:19 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000680Frama-CPlug-in > Evapublic2011-10-10 14:14
Reporteryakobowski 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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

-Relationships
+Relationships

-Notes

~0001401

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.

~0001414

monate (reporter)

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

~0001415

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.

~0001416

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.

~0001531

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.

~0002015

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.

~0002016

yakobowski (manager)

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

-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