--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on July 2010 ---
[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>