Testing example which is OK for Jessie-plugin fails with wp-plugin.
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.