WP - strcpy not proved
ID0001652: This issue was created automatically from Mantis Issue 1652. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001652 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| Reporter | dharma | Assigned To | - | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | Ubuntu | OS | Linux | OS Version | 64 bit |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | - |
Description :
I took the attached program from one of the WP tutorials but added the main function which calls strcpy. I wonder why the requires are not valid. I do not know what is wrong with my two strings in main.
Steps To Reproduce :
[formal_verification]$ frama-c -pp-annot -wp -wp-rte -wp-proof why3:Z3,alt-ergo -wp-split -wp-model Typed+ref string_lib.c [kernel] preprocessing with "gcc -C -E -I. -dD string_lib.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function main [wp] Collecting variable usage [wp] 4 goals scheduled [wp] [Qed] Goal typed_ref_main_call_strcpy_pre_2_part1 : Valid [wp] [Qed] Goal typed_ref_main_call_strcpy_pre_2_part1 : Valid [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre : Unknown [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre_2_part2 : Unknown (Qed:4ms) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre_2_part2 : Unknown (Qed:4ms) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre : Unknown [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre_3 : Valid (24ms) (22) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre_3 : Valid (10ms)