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]

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>