--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on December 2010 ---
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>