--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic



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>