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] question about treatment of assigns clauses in WP (Neon)

Jens,

On this example, WP behaves correctly in respect of the ACSL semantics 
of assigns clauses:
an asssigns clause only states over memory locations that are allocated 
in both the pre-state and the post-state.
There is nothing about validity.

Assigns clauses shouldn't be seen as main specification goals but only 
as intermediate goals necessary to give for dealing with proof of other 
properties :
- assigns clauses at top level of a function help analysis tools to 
handle calls to that function,
- loop assigns clauses help to handle loops.
It is the reason why these properties have been introduced into ACSL.
Weak semantics have been given to these properties in order to ease 
their proof (which can be seen as an overhead).

You are looking for stronger semantics...
It seems you want a new clause :
- stronger_assigns *(a+(0..n));
which can be automatically rewritten into a normal
- assigns *(a+(0..n));
and an assert at the entry point of the function:
- \valid(a+(0..n));

A plug-in can do that...

Patrick.


20/04/2014 20:26, Gerlach, Jens wrote:
> Here is a simple function foo that sets all elements of an array to zero.
>
> /*@
>      requires \valid(a + (0..n-1));
>      assigns  a[0..n];  // should be a[0..n-1]
> */
> void foo(int* a, unsigned int n)
> {
>     /*@
>         loop invariant 0 <= i <= n;
>         loop assigns i, a[0..n]; // should be a[0..n-1];
>         loop variant n-i;
>     */
>     for(unsigned int i = 0; i < n; ++i)
>         a[i] = 0;
> }
>
> Using the command line
>
> 	frama-c-gui.byte -wp -wp-rte -wp-model Typed+ref -wp-timeout 10 -wp-prover alt-ergo -wp-out loop_assigns.wp  loop_assigns.c
>
> I can see that all proof obligations are discharged by either Qed or Alt-Ergo.
>
> My question is about the assigns clause which refers to all offsets of a in the range [0..n].
> (Note that I use the same range in the loop assigns clause.)
> The precondition, however, only states that array offsets in the range [0..n-1] are valid.
> I think I would prefer if WP issued a warning about this discrepancy.
> What do you think?
>   
> Regards
>
> Jens
>
>