"assert i >= 0;" not proven for unsigned char
ID0000094:
**This issue was created automatically from Mantis Issue 94. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000094 | Frama-C | Plug-in > jessie | public | 2009-05-25 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mottainai | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
The first assertion in the the following code fragment is not proven.
(neither alt-ergo nor yices nor cvc3).
unsigned char uchar_range(unsigned char i)
{
//@ assert i >= 0;
//@ assert i <= UCHAR_MAX;
return i;
}
### Additional Information :
I am using Frama-C Lithium-20081201 on Mac OS X 10.5.7
issue