| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | 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 | ||||||
| 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 |
|
 Relationships |
| Notes |
|
|
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. |
|
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. |
|
Anne (reporter) 2009-08-26 11:37 |
Still need an example to see if the fix is correct. |
| Notes |
| 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 | ||
| 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 |
| 2013-12-19 01:13 | Anne | Source_changeset_attached | => framac master 899ddcf7 |
| 2013-12-19 01:14 | Source_changeset_attached | => framac master a67c005b | |
| 2014-02-12 16:56 | Anne | Source_changeset_attached | => framac stable/neon 899ddcf7 |
| 2014-02-12 16:56 | Source_changeset_attached | => framac stable/neon a67c005b | |
| Issue History |