ID0001054: **This issue was created automatically from Mantis Issue 1054. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001054 | Frama-C | Plug-in > wp | public | 2011-12-16 | 2011-12-19 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | naveugene | **Assigned To** | correnson | **Resolution** | no change required | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - | ### Description : [Sorry for my English] I tried to verificate function with Frama-C Carbon + wp plugin + Alt-Ergo: void set_array (int t[] , int n, int a) { for (int i=0; i < n; i++) t[i] = a; } using Frama-C Boron + jessie plugin + Alt-Ergo all is OK: " total : 15 valid : 15 (100%) " but using wp: " No proofs : 3 Partial proofs : 1 Complete proofs : 3 Total : 7 " files from "logs" folder (store_set_array_assert_3_rte_log.txt , store_set_array_assert_4_rte_log.txt , store_set_array_post_1_log.txt) are empty. ================== Why count of "No proofs", "Partial proofs" is not 0? Why logfiles are empty? (I'm including console output for jessie, wp for my example, and file arr_set_for.c with procedure and ACSL implementation in "arr_set_for.zip".) ### Tags : jessie, wp ### Additional Information : The examples from "frama-c-wp-manual.pdf", page 8 (swap1.c, swap 2.c) are OK. ## Attachments - [arr_set_for.zip](/uploads/0f9a00c0f09c4866ce250f20a557f9f2/arr_set_for.zip)