pointer arithmetic
ID0000652: This issue was created automatically from Mantis Issue 652. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000652 | Frama-C | Plug-in > jessie | public | 2010-12-24 | 2010-12-24 |
| Reporter | evdenis | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
Error occurs when I use "pattern + plen - suffixlen" instead of "&pattern[plen - suffixlen]" ( char * pattern, size_t plen, size_t suffixlen ) in source code.
tester@ubuntu-fm:~/workspace/test3$ frama-c -jessie -jessie-atp gui test.c [kernel] preprocessing with "gcc -C -E -I. -dD test.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir test.jessie [jessie] File test.jessie/test.jc written. [jessie] File test.jessie/test.cloc written. [jessie] Calling Jessie tool in subdir test.jessie Generating Why function _strncmp Generating Why function suffix_match [jessie] Calling VCs generator. gwhy-bin [...] why/test.why Computation of VCs... File "why/test.why", line 538, characters 35-89: Term neg_int(integer_of_uint32(offset)) is expected to have type uint32 make: *** [test.stat] Error 1 [jessie] user error: Jessie subprocess failed: make -f test.makefile gui