Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002326Frama-CPlug-in > value analysispublic2017-08-11 18:472017-09-01 10:08
Reportermehdi 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C 15 Phosphorus 
Target VersionFixed in Version 
Summary0002326: Value.cmo needs LoopAnalysis.cmo
DescriptionHi,

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.
TagsNo tags attached.
Attached Filespatch file icon 0005-Value.cmo-needs-LoopAnalysis.cmo.patch [^] (891 bytes) 2017-08-11 18:47 [Show Content]

- Relationships

-  Notes
(0006438)
yakobowski (manager)
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 (reporter)
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 (manager)
2017-09-01 10:08

Fixed in Phosphorus bugfix (https://github.com/Frama-C/Frama-C-snapshot/commit/30b819710d7630 [^])

- Issue History
Date Modified Username Field Change
2017-08-11 18:47 mehdi New Issue
2017-08-11 18:47 mehdi Status new => assigned
2017-08-11 18:47 mehdi Assigned To => yakobowski
2017-08-11 18:47 mehdi File Added: 0005-Value.cmo-needs-LoopAnalysis.cmo.patch
2017-08-12 13:44 yakobowski Note Added: 0006438
2017-08-12 15:31 mehdi Note Added: 0006441
2017-08-12 17:58 yakobowski Note Edited: 0006438 View Revisions
2017-09-01 10:08 yakobowski Note Added: 0006455
2017-09-01 10:08 yakobowski Status assigned => closed
2017-09-01 10:08 yakobowski Resolution open => fixed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker