--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Specification Examples



Hi,

Sorry, I did only check on the current unreleased version. I'll check on a
released version next time. This will be available in the next release so.

Yannick

On Tue, Oct 14, 2008 at 12:16 PM, Jens Gerlach <
jens.gerlach@first.fraunhofer.de> wrote:

> Dear Yannik,
>
>
>> But if I am using the Pre Label I don't meet the ensures requirements, or
>> at least I don't get a green bullet.
>>
>
> as I told you, the normal way of treating separation in Jessie is to divide
> heap into regions automatically, which will become the default in the next
> release. With only one region for memory, your example is proved with any of
> Z3, Alt-Ergo and Simplify (not Yices though).
>
> To prove instead that the value of [a] after copying is the same as the
> value of [b] before, you need to strengthen the loop invariant like follows,
> to assess that all of [b] does not change during the loop.
>
> /*@ requires 0 < n;
>   @ requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1);
>   @ requires disjoint_arrays(a, b, n);
>   @ ensures  \forall int k; 0 <= k < n ==> a[k] == \at(b[k],Pre);
>   @*/
> void array_cpy(int* a, int n, int* b)
> {
>    /*@ loop invariant 0 <= i <= n;
>      @ loop invariant \forall int m; 0 <= m < n  ==> b[m] == \at(b[m],Pre);
>      @ loop invariant \forall int m; 0 <= m < i  ==> a[m] == b[m];
>      @*/
>    for (int i = 0; i < n; i++)
>      a[i] = b[i];
> }
>
>
> I just run this example under Helium (Mac OS X) (adding the disjoint_arrays
> predicate) and received the following error message
>
> running gcc -C -E -I. array.c
> File array.c, line 7, characters 50-63:
> Error during analysis of annotation: logic label `Pre' not found
> array.c:7: Warning: ignoring logic specification of function array_cpy
> Parsing
>
> Best regards
>
> Jens Gerlach
>
> With these annotations, Z3, ALt-Ergo and Simplify still prove your function
> (not Yices).
>
>
>>
>> Currently I'm stuck with an other Problem. Within some annotated string.h
>> examples I found a dereferenced \result.
>>
>> Attempts to apply it to my example will result in the following error.
>>
>> Fatal error: exception Assert_failure("src/jessie/interp.ml", 336, 14)
>>
>> do I get it due to my Hydrogen version ?
>>
>
> Most probably, yes. There was such a problem with derefencing \result and
> it was solved. The best way to track this kind of problem is to fill in a
> bug report on the Frama-C public BTS, so that you get a precise answer when
> the bug gets fixed.
>
> HTH.
>
> --
> Yannick
>  _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>


-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081014/155292f7/attachment.html