--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on October 2014 ---
[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
>