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] Issues with WP on program doing simple pointer arithmetic

  • Subject: [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 4 Sep 2013 15:17:35 +0200
Hello,

I am trying to verify with WP (Frama-C Fluorine June release, Alt-Ergo
0.95.1) the absence of Run Time Errors (RTE) in the attached program
which does some simple pointer manipulation.

I don't understand to main points:
  1. In main(), why WP cannot prove simple invariant like "0 <= i <=
99;"? The call to pop() or push() apparently annoys it. But I don't
understand why. In loop(), I have similar invariant without such call
which are correctly proved.

  2. Why WP does not even try to prove ("Status: no verification
attempted") some predicates: \valid() in pop() and push() requires
clauses, loop assigns and variant in main(), even rte for i++ in the
first loop of main()? In the same way, in loop() function I have a
requirement on \valid(global_i_ptr) and this predicate is properly
checked and proved.

If somebody has some enlightenments, I would very glad to hear them.

I launch WP with:
 frama-c-gui -cpp-command 'gcc -C -E -I/path/to/share/frama-c/libc'
-wp -wp-rte -wp-par 8 q6_stack.c

The properties are proved using Value analysis and -slevel 1000
(except assigns and loop variant which are not looked at).

Best regards,
david
-------------- next part --------------
A non-text attachment was scrubbed...
Name: q6_stack.c
Type: text/x-csrc
Size: 1763 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130904/66087f56/attachment.c>