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] Problems with division in lemmas
- Subject: [Frama-c-discuss] Problems with division in lemmas
- From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
- Date: Thu, 16 Jul 2009 16:53:45 +0200
- References: <283BBA28B2314A2ABCDA8F0487D9B207@AHARDPLACE>
On Christoph Weber's request I forward the following mail: ----------------------------- Hello, I am exploring the possibilitys of lemmas to assist proofs. As I allready mentioned before, I cannot proof the lemma (mean) you provided with any prover. It seems to me, that the division within prevents a solution. For example the following: /*@ lemma test1 : \forall int x; x/1 == x; */ /*@ lemma test2 : \forall int x; x/x == 1; */ The computations would result in unknowns. I would like to know if this is a general problem and if there is a way to circumvent it. Sincerely Christoph
- Follow-Ups:
- [Frama-c-discuss] Problems with division in lemmas
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Problems with division in lemmas
- Prev by Date: [Frama-c-discuss] How to compil Frama-C with an existing Why installation
- Next by Date: [Frama-c-discuss] Problems with division in lemmas
- Previous by thread: [Frama-c-discuss] Frama-C/Jessie: not_assigns and mutable parameter
- Next by thread: [Frama-c-discuss] Problems with division in lemmas
- Index(es):