Frama-C Bug Tracking System - Frama-C
View Issue Details
0002326Frama-CPlug-in > Evapublic2017-08-11 18:472017-09-01 10:08
mehdi 
yakobowski 
normalminoralways
closedfixed 
Frama-C 15-Phosphorus 
 
0002326: Value.cmo needs LoopAnalysis.cmo
Hi, Value plugin needs LoopAnalysis, but appears first during the linking phase. In order to workaround that, we move it before Value.cmo in the PLUGIN_CMO_LIST variable. Please find attached a simple patch which fixes this in the Makefile.
No tags attached.
patch 0005-Value.cmo-needs-LoopAnalysis.cmo.patch (891) 2017-08-11 18:47
https://bts.frama-c.com/file_download.php?file_id=1204&type=bug
Issue History
2017-08-11 18:47mehdiNew Issue
2017-08-11 18:47mehdiStatusnew => assigned
2017-08-11 18:47mehdiAssigned To => yakobowski
2017-08-11 18:47mehdiFile Added: 0005-Value.cmo-needs-LoopAnalysis.cmo.patch
2017-08-12 13:44yakobowskiNote Added: 0006438
2017-08-12 15:31mehdiNote Added: 0006441
2017-08-12 17:58yakobowskiNote Edited: 0006438View Revisions
2017-09-01 10:08yakobowskiNote Added: 0006455
2017-09-01 10:08yakobowskiStatusassigned => closed
2017-09-01 10:08yakobowskiResolutionopen => fixed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0006438)
yakobowski   
2017-08-12 13:44   
(edited on: 2017-08-12 17:58)
This one is probably a "false positive". Value should not depend on LoopAnalysis. The only dependency is in a left-over debug code if false then LoopAnalysis.Loop_analysis.get_bounds stmt else None in domains/gauges/gauges_domain.ml Do you build without optimisations? Anyway, the correct patch consists in commenting out the "then" part.
(0006441)
mehdi   
2017-08-12 15:31   
Optimisations are enabled, but they are not enough on bytecode architectures. So, indeed, we don't observe this issue on native architectures.
(0006455)
yakobowski   
2017-09-01 10:08   
Fixed in Phosphorus bugfix (https://github.com/Frama-C/Frama-C-snapshot/commit/30b819710d7630)