Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] requires fail in WP plugin?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Wed, 19 Feb 2014 20:47:50 -0500
  • In-reply-to: <CAHRgRYtUGg4dCvS9FEUVpDwEkf3dy9=BmcdoY797m4mgC2X8fg@mail.gmail.com>
  • References: <CAHRgRYtUGg4dCvS9FEUVpDwEkf3dy9=BmcdoY797m4mgC2X8fg@mail.gmail.com>
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>