--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on February 2014 ---
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>