Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000216Frama-CPlug-in > scopepublic2009-08-25 14:202014-02-12 16:56
Reporterpascal 
Assigned Topascal 
PriorityhighSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090601-beta1 
Target VersionFixed in VersionFrama-C Beryllium-20090901 
Summary0000216: Uncaught exception in scope
DescriptionIn all versions since at least Lithium and until SVN 5989,
there seems to be the possibility
of the exception Lmap_bitwise.From_Model.Cannot_fold being raised
by Lmap_bitwise.From_Model.fold and not being caught in scope/datascope.ml.

The backtrace was obtained by running the GUI on a semi-confidential codebase,
using the Lithium release.

In SVN 5989 terms, the uncaught exception appears to originate from
the call to Lmap_bitwise.From_Model.fold as datascope.ml:116,
where I do not see immediately a handler for the exception.
Additional InformationThe backtrace is a little sketchy (but not inconsistent), I am not sure why.
But there is only one call to a function that can raise this exception
in the whole file datascope.ml anyway.

Fatal error: exception Lmap_bitwise.Make_bitwise(V).Cannot_fold
Raised at file "src/memory_state/lmap_bitwise.ml", line 132, characters 21-32
Called from file "list.ml", line 74, characters 24-34
Called from file "list.ml", line 74, characters 24-34
Called from file "src/scope/datascope.ml", line 158, characters 16-64
Called from file "src/scope/datascope.ml", line 410, characters 24-34
Called from file "src/scope/datascope.ml", line 458, characters 34-70
Called from file "cil/src/cil.ml", line 6527, characters 15-31
Called from file "src/kernel/visitor.ml", line 60, characters 18-62
Called from file "cil/src/cil.ml", line 6557, characters 19-22
Called from file "cil/src/cil.ml", line 6597, characters 22-55
Called from file "list.ml", line 62, characters 22-25
Called from file "src/kernel/visitor.ml", line 103, characters 13-105
Called from file "src/kernel/visitor.ml", line 141, characters 42-65
Called from file "cil/src/cil.ml", line 7465, characters 4-81
Called from file "cil/src/cil.ml", line 6557, characters 19-22
Called from file "cil/src/cil.ml", line 7584, characters 15-39
Called from file "cil/src/cil.ml", line 6537, characters 21-41
Called from file "cil/src/cil.ml", line 7527, characters 17-25
Called from file "cil/src/cil.ml", line 6537, characters 21-41
Called from file "cil/src/cil.ml", line 7465, characters 4-81
Called from file "cil/src/cil.ml", line 6557, characters 19-22
Called from file "cil/src/cil.ml", line 7584, characters 15-39
Called from file "cil/src/cil.ml", line 6537, characters 21-41
Called from file "cil/src/cil.ml", line 7791, characters 13-38
Called from file "cil/src/cil.ml", line 6537, characters 21-41
Called from file "cil/src/cil.ml", line 7766, characters 4-96
Called from file "cil/src/cil.ml", line 7842, characters 15-37
Called from file "cil/src/cil.ml", line 6557, characters 19-22
Called from file "cil/src/cil.ml", line 6597, characters 22-55
Called from file "cil/src/cil.ml", line 7836, characters 4-59
Called from file "cil/src/cil.ml", line 8014, characters 24-33
Called from file "cil/src/cil.ml", line 8016, characters 2-19
Called from file "cil/src/cil.ml", line 6537, characters 21-41
Called from file "cil/src/cil.ml", line 8032, characters 14-38
Called from file "src/scope/datascope.ml", line 478, characters 9-102
Called from file "src/value/register.ml", line 62, characters 8-34
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/toplevel/main.ml", line 56, characters 4-21
Called from file "src/toplevel/main.ml", line 72, characters 4-36
Re-raised at file "src/toplevel/main.ml", line 41, characters 2-971
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 109, characters 2-33
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000344)
Anne (reporter)
2009-08-25 14:34

Ok. I have done something but I don't know how to test it. Could you tell me if it works and if it makes sense in your example ?

BTW, do you know how to build an example where Lmap_bitwise.From_Model.fold raise the exception ?

Thank you.
(0000345)
pascal (reporter)
2009-08-25 15:17

I will try to obtain the original example.

I have been unable to write a small example where the
from computation degenerates in just the right way (keeping in mind that it relies
on the already computed fixpoints of the value analysis).

I will also backport the fix to Lithium and suggest the patch to the
original reporter.
(0000350)
Anne (reporter)
2009-08-26 11:37

Still need an example to see if the fix is correct.

- Issue History
Date Modified Username Field Change
2009-08-25 14:20 pascal New Issue
2009-08-25 14:20 pascal Status new => assigned
2009-08-25 14:20 pascal Assigned To => Anne
2009-08-25 14:33 svn Checkin
2009-08-25 14:34 Anne Note Added: 0000344
2009-08-25 15:17 pascal Note Added: 0000345
2009-08-26 11:36 Anne Status assigned => resolved
2009-08-26 11:36 Anne Fixed in Version => Frama-C svn, precise the release id
2009-08-26 11:36 Anne Resolution open => fixed
2009-08-26 11:37 Anne Assigned To Anne => pascal
2009-08-26 11:37 Anne Note Added: 0000350
2009-08-26 11:37 Anne Status resolved => feedback
2009-08-26 11:37 Anne Resolution fixed => reopened
2009-08-26 17:18 Anne Status feedback => resolved
2009-08-26 17:18 Anne Resolution reopened => fixed
2009-09-02 10:54 signoles Status resolved => closed
2009-09-23 16:58 signoles Fixed in Version Frama-C svn, precise the release id => Frama-C Beryllium


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker