pointer casts not supported
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