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>
- Follow-Ups:
- [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
- From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
- [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
- From: loic.correnson at cea.fr (Loïc Correnson)
- [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
- Prev by Date: [Frama-c-discuss] Assignments proof
- Next by Date: [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
- Previous by thread: [Frama-c-discuss] How to reply a specific topic without opening a new topic.
- Next by thread: [Frama-c-discuss] Issues with WP on program doing simple pointer arithmetic
- Index(es):