WP 0.5 crashes with an Unbound label parameter 'Here'
ID0001060: This issue was created automatically from Mantis Issue 1060. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001060 | Frama-C | Plug-in > wp | public | 2012-01-11 | 2012-06-10 |
| Reporter | Mounir | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
A reproductible bug for the attached example from "ACSL by example". It was proven correctly previously.
[wp] failure: Unbound label parameter 'Here' in predicate or function call [kernel] The full backtrace is: Raised at file "register.ml", line 610, characters 27-29 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 36, characters 4-20 Called from file "src/kernel/cmdline.ml", line 723, characters 2-9 Called from file "src/kernel/cmdline.ml", line 200, characters 4-8