--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on September 2013 ---
Hello, Replacing in the source code in the main() function: for (i=98; i>0; i--) { if (pop() != i) abort(); } by: for (i=98; i>0; i--) { unsigned tmp = pop(); if (tmp != i) abort(); } permits to bypass the problem (ie, almost all VCs are discharged). I let Frama-C experts explain what occurred in more details?! HTH, D. > -----Message d'origine----- > De?: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c- > discuss-bounces at lists.gforge.inria.fr] De la part de David MENTRE > Envoy??: mercredi 4 septembre 2013 15:18 > ??: Frama-C public discussion > Objet?: [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