Segmentation error occured while processing statement contract
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)