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-08-12 17:58
Assigned Toyakobowski 
PlatformOSOS Version
Product VersionFrama-C 15 Phosphorus 
Target VersionFixed in Version 
Summary0002326: Value.cmo needs LoopAnalysis.cmo

Value plugin needs LoopAnalysis, but appears first during the linking
phase. In order to workaround that, we move it before Value.cmo in the

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
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/

Do you build without optimisations?

Anyway, the correct patch consists in commenting out the "then" part.

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.

- 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

Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker