--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on December 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] jessie: Unbound variable failure if unsigned char* arguments used



Dear colleagues,

Are any workarounds for the following jessie failure:

 > frama-c -jessie -jessie-atp pvs memcpy.c
[kernel] preprocessing with "gcc -C -E -I.  -dD memcpy.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir memcpy.jessie
[jessie] File memcpy.jessie/memcpy.jc written.
[jessie] File memcpy.jessie/memcpy.cloc written.
[jessie] Calling Jessie tool in subdir memcpy.jessie
Generating Why function memcpy
[jessie] Calling VCs generator.
WHYLIB=/usr/local/lib/why why -pvs -dir pvs -pvs-preamble "IMPORTING 
why at jessie"  -split-user-conj -explain -locs memcpy.loc 
/usr/local/lib/why/why/jessie_bitvectors.why why/memcpy.why
File "why/memcpy.why", line 678, characters 33-71:
Unbound variable unsigned_char_P_dst_1_alloc_table
make: *** [pvs/memcpy_why.pvs] Error 1
[jessie] user error: Jessie subprocess failed: make -f memcpy.makefile pvs

If someone replaces 'unsigned char*' with 'char*', jessie works well.

--
Regards,
Alexey Khoroshilov
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: khoroshilov at linuxtesting.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: memcpy.c
Type: text/x-csrc
Size: 618 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101203/626a2c1a/attachment.c>