Use of Cabs2cil.fresh_global
ID0000680: This issue was created automatically from Mantis Issue 680. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000680 | Frama-C | Plug-in > Eva | public | 2011-01-20 | 2011-10-10 |
| Reporter | yakobowski | Assigned To | pascal | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20101202-beta2 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information