--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on September 2009 ---
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