0000216: Uncaught exception in scope - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000216

Frama-C

Plug-in > scope

public

2009-08-25 14:20

2014-02-12 16:56

Reporter

pascal

Assigned To

pascal

Priority

high

Severity

crash

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Beryllium-20090601-beta1

Target Version

Fixed in Version

Frama-C Beryllium-20090901

Summary

0000216: Uncaught exception in scope

Description

In 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 Information

The 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

Tags

No 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