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

[Frama-c-discuss] Specification Examples



Thanks for the advice with the integer.

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.

Currently I'm stuck with an other Problem. Within some annotated string.h 
examples I found a dereferenced \result.

/*@
 requires last > first;
 requires \valid_range(first, 0, last-first-1);
 ensures *\result == value;
*/
int* find_int_array (int* first, int* last, int value );

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 ?

Christoph

----- Original Message ----- 
From: "Claude March?" <Claude.Marche@inria.fr>
To: "Christoph Weber" <Christoph.Weber@first.fraunhofer.de>
Cc: <frama-c-discuss@lists.gforge.inria.fr>
Sent: Monday, October 13, 2008 1:51 PM
Subject: Re: [Frama-c-discuss] Specification Examples


>
>
> Christoph Weber wrote:
>> Hi and a thank you for the help,
>>
>> but I like to continue questioning where I stopped.
>>
>> You remember the array_cpy:
>> /*@
>>  requires 0 < n;
>>  requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1)&& 
>> disjoint_arrays(a, b, n);
>>  ensures  \forall int k; 0 <= k < n ==> a[k] == b[k];
>> */
>> void array_cpy(int* a, int n, int* b)
>> {
>>     /*@
>>      loop invariant 0 <= i <= n && \forall int m; 0 <= m < i  ==> a[m] == 
>> b[m];
>>     */
>>     for (int i = 0;i < n;i++)
>>     {
>>         a[i] = b[i];
>>     }
>> }
>>
>> This works fine with the Hydrogen-version on Win 32 and the Z3 prover. On 
>> the Helium edition on OSX it terminates successfully with CVC3 (Z3 not 
>> aviable). Now I'd like to know:
>> - what has to be done or added to let ergo v0.8 or simplify verify it as 
>> well.
>
> You have to improve ergo and simplify :-)
>
> One advice is to use "integer" instead of ints in your annotations:
>
> ensures  \forall integer k; 0 <= k < n ==> a[k] == b[k];
>
> and so on.
>
>> - array_cpy is only partial specified on my opinion the ensures clause 
>> has to be altered to
>>     ensures  \forall int k; 0 <= k < n ==> a[k] == \old(b[k]);
>> using this I receive an error due to preservation of loop invariant. I 
>> think  the comparison in the loop invariant has to be altered to a[m] == 
>> \at(b[m],Old);
>> but FramaC will return
>>     File array_test.c, line 28, characters 80-93:
>>     Error during analysis of annotation: logic label `Old' not found
>>     array_test.c:29: Warning: ignoring logic loop annotation
>> I tried a bit but I where unable to cheat my way around.
>
> Old does not mean anything in loop invariants. You have to use Pre:
> a[m] == \at(b[m],Pre)
>
>
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>