ID0001153: **This issue was created automatically from Mantis Issue 1153. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001153 | Frama-C | Plug-in > jessie | public | 2012-04-16 | 2013-03-27 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | nmuller | **Assigned To** | cmarche | **Resolution** | won't fix | | **Priority** | normal | **Severity** | feature | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - | ### Description : such assertions seem not to be supported by jessie. /*@ assert ((8+(int )p[1] >= 0) && (8+(int )p[1] < 32)); */ /*@ assert ((16+(int )*p >= 0) && (16+(int )*p < 32)); */ p is a char * ### Additional Information : frama-c -jessie -jessie-atp alt-ergo endian.c [kernel] preprocessing with "gcc -C -E -I. -dD endian.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir endian.jessie [jessie] File endian.jessie/endian.jc written. [jessie] File endian.jessie/endian.cloc written. [jessie] Calling Jessie tool in subdir endian.jessie Generating Why function main Jessie support for unions and pointer casts is disabled [jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs endian.cloc endian.jc ## Attachments - [endian.c](/uploads/9443949c6de585136aae9015cc9f9f75/endian.c)