--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on September 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] support assigns clauses



Hello,

thank you for your previous answers.

Today I would like to know, if I can help a prover to solve an assigns
clause.

Since the feature is rather new, I have little experience.

To illustrate my problem, I have appended the function "remove_copy_array".

Using the new assigns clauses, I cannot prove all VC.
In particular the comparison with the axiomatization will fail.

Is there a way to help the prover to process the assigns clause?


Sincerely

Christoph
-------------- next part --------------
A non-text attachment was scrubbed...
Name: remove_copy_array.c
Type: application/octet-stream
Size: 668 bytes
Desc: remove_copy_array.c
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090922/e25595ae/attachment.obj 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: remove_copy_array.h
Type: text/x-c
Size: 3163 bytes
Desc: remove_copy_array.h
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090922/e25595ae/attachment.bin