--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on February 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] requires fail in WP plugin?



Hi,

I took this 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.


[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)


Thanks for your help.
Dharma
-------------- next part --------------
A non-text attachment was scrubbed...
Name: string_lib.c
Type: text/x-csrc
Size: 921 bytes
Desc: string_lib.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140219/cd76ab13/attachment.c>