ID0000633: **This issue was created automatically from Mantis Issue 633. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000633 | Frama-C | Plug-in > jessie | public | 2010-12-01 | 2011-07-29 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Astra | **Assigned To** | pascal | **Resolution** | fixed | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - | ### Description : During the processing of /*@ ensures lbstack[stackpos] < ub; */ if (lb < p-1) Frama gives the next message: tester@ubuntu-fm:~/workspace/prac1$ frama-c -jessie -jessie-atp gui qsorti_bug.c[kernel] preprocessing with "gcc -C -E -I. -dD qsorti_bug.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir qsorti_bug.jessie [jessie] File qsorti_bug.jessie/qsorti_bug.jc written. Segmentation error The similar "ensures" for the next "if"-statement causes no error. The source file is attached. ### Additional Information : OS: UbuntuFM 10.04 (in Oracle VM VirtualBox) ## Attachments - [qsorti_bug.c](/uploads/1d94fa197ef462be8d4e2b0e23595009/qsorti_bug.c)