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] *p and p[0]
- Subject: [Frama-c-discuss] *p and p[0]
- From: tzuhsiang.chien at gmail.com (Logan Chien)
- Date: Sat, 10 Jul 2010 19:12:44 +0800
- In-reply-to: <AANLkTinvdPYahtS5k3P6tYIPT0mD_SNPABwA5IIiLyhz@mail.gmail.com>
- References: <AEF3FB2726363B4CB096A240443255105212E5@SCTEX008.st-cloud.dassault-avion.fr> <4C36E6E8.9040906@inria.fr> <AANLkTimquupyQ16hYIjfm3arVpZ5AB7eVNtDTHXzxFe-@mail.gmail.com> <AANLkTinvdPYahtS5k3P6tYIPT0mD_SNPABwA5IIiLyhz@mail.gmail.com>
Hi, After further investigation, it seems that the statement "global = 402;" is considered as a part of initialization statement of the loop. So it is EXPECTED and CORRECT that the theorem prover regards the proof obligation of the loop invariant as UNKNOWN (or TLE) since global != global0. Though, I think it will be better to have an independent "assigns" annotation proof, so that it will be much easier to figure out which code is violating the specification. Logan (Tzu-hsiang Chien) On Fri, Jul 9, 2010 at 11:02 PM, Logan Chien <tzuhsiang.chien at gmail.com>wrote: > This can reproduced by following code, which is written incorrectly > intentionally. > I am expecting that Frama-C/Jessie will tell me that the function code > violate > the "assigns" annotation. However, Frama-C/Jessie tells me that loop > invariant > can't be proved. > > ------------------------------------------------------------ > -------------------------------------- > int global; // Here comes an global > > /*@ requires n > 0; > requires \valid(p+ (0..n-1)); > assigns \nothing; // Specify that this function do not assign any > non-local or local-static variable. > ensures \forall integer i; 0 <= i <= n-1 ==> \result >= \old(p)[i]; > ensures \exists integer e; 0 <= e <= n-1 && \result == \old(p)[e]; > */ > int max_seq(int* p, int n) { > global = 402; // Just assign something and VIOLATE the "assigns" > annotation. > int res = *p; > /*@ assert res == p[0]; */ > /*@ loop invariant p == \at(p, Pre) + i; // Some of the loop invariant > can't be proved > loop invariant 0 <= i <= n; > loop invariant \forall integer j; 0 <= j < i ==> \at(p, Pre)[j] <= > res; > loop invariant \exists integer k; (k == 0 || 0 <= k < i) && \at(p, > Pre)[k] == res; > loop variant n - i; > */ > for(int i = 0; i < n; i++) { > if (res < *p) { res = *p; } > p++; > } > return res; > } > > ---------------------------------------------------------------------------------------- > > "Function max_seq Default Behavior > 7. loop invariant initially holds" > - Alt-Ergo (0.91) gives Unknown > - CVC3 (0.22) gives TLE > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100710/79d0d97b/attachment.htm>
- References:
- [Frama-c-discuss] *p and p[0]
- From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
- [Frama-c-discuss] *p and p[0]
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] *p and p[0]
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] *p and p[0]
- From: tzuhsiang.chien at gmail.com (Logan Chien)
- [Frama-c-discuss] *p and p[0]
- Prev by Date: [Frama-c-discuss] Pointer problem with nested objects
- Next by Date: [Frama-c-discuss] Frama-C can't detect "Undefined side-effects in expressions"
- Previous by thread: [Frama-c-discuss] *p and p[0]
- Next by thread: [Frama-c-discuss] *p and p[0]
- Index(es):