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] (no subject)

As said others before, your contract on main() is not valid.

As the name "new_value" suggests, do you expect that this function
returns a freshly allocated pointer? In that case, your contract should
reflect this. Here is a possible specification. Notice also that your
initial ensures "\result != \null" is not enough to guarantee that the
resulting pointer is \valid


/*@ assigns \nothing;
  @ allocates \result;
  @ ensures \valid(\result) && \fresh(\result,sizeof(int*));
  @*/
extern int *new_value();

/*@ requires \valid(p);
  @ assigns *p;
  @*/
void f(int* p){
  *p = 8;
}

/*@ assigns \nothing;
  @*/
int main(void){
 int *p = new_value();
 f(p);
}

Side note: the allocates clause might not be well supported by plugins
WP and Jessie. With Jessie, such a code triggers an error, unless you
add the pragma

#pragma SeparationPolicy(none)

(this is a known bug of the separation analysis in presence of dynamic
allocation)

- Claude



On 10/31/2014 04:09 PM, gavran at mpi-sws.org wrote:
> Hi,
> 
> I have a problem with assigns clause. Assume the following code:
> 
> /*@ ensures \result != \null;
>   @ assigns \nothing;
>   @*/
> extern int *new_value();
> 
> //@ assigns *p;
> void f(int* p){
>   *p = 8;
> }
> //@ assigns \nothing;
> int main(void){
>  int *p = new_value();
>  f(p);
> }
> 
> The prover is unable to prove that main assigns \nothing, which makes
> sense, as main assigns to *p through function f. However, how should I
> state that in \assigns clause, since p is local variable and can not be
> accessed within annotation?
> 
> Ivan
> p.s. I repeat the question posted on SO -
> http://stackoverflow.com/questions/26591694/assigns-clause-for-local-variables-in-frama-c
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>