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 ## Attachments - [count.c](/uploads/5d2267bc8572f7408b3f4710096bd854/count.c)