--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on September 2013 ---
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>