--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on May 2014 ---
Hi all, I am trying to develop a frama-c script that uses wp api to get a list of list of pos. I am using Annotations.fold_all_code_annot and applying the function goals_of_property to get the proof obligations list, after i invoke wp_run() and a function that calls the prover on the annotations. The types all check correctly but when i use it it always returns me an empty list. I think i am not invoking wp plugin correctly or not using fold_all_code_annot correctly. If you could explain me what i am doing wrong i would be very grateful. I have tried to study wp plugin but there is little information about how you can use the api and only how to use the wp plugin itself, which is understandable due to be still in development. In annex, i attach my script and the example i use as input. Thanks in advance, Jos? Pinheiro -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140527/5f368bd0/attachment.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: wp_script.ml Type: application/octet-stream Size: 3217 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140527/5f368bd0/attachment.obj> -------------- next part -------------- A non-text attachment was scrubbed... Name: swap.c Type: text/x-csrc Size: 229 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140527/5f368bd0/attachment.c>