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] Specification Examples

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081014/9d075997/attachment.htm