--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on June 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Annotation pre-processing



Dear all,
Following the answer to my last question I tried to prove some programs 
with the SeparationPolicy option set to none.
I have a program where the two arrays given as parameters must not be 
equal (that is the corresponding pointers must not point to the same 
memory area). I tried to prove the following contract to suh a function.

#define ERROR 0xFFu
#define OK 0x00u
#pragma SeparationPolicy(none)

/*@ requires (t1 == NULL) || \valid(t1+(0..9));
  @ requires (t2 == NULL) || \valid(t2+(0..9));
  @ behavior err:
  @   assumes (t1 == NULL) || (t2 == NULL) || (t1 == t2);
  @   ensures \result == ERROR;
  @ behavior ok:
  @   assumes (t1 != NULL) && (t2 != NULL) && (t1 != t2);
  @   ensures \result == OK; */

unsigned f( unsigned t1[10], unsigned t2[10] )
{
  if ( ( t1 == NULL ) || ( t2 == NULL ) || ( t1 == t2 ) )
    return ERROR;
  // some code
  return OK;
}
I do not expect this to work with the default SeparationPolicy (if I 
understood correctly the point) but I thought this would work with the 
"none" parameter.
Moreover I also tried with an  additional requires clause specifying that 
if t1 != t2 then t1+i != t2+j for 0 <= i,j < 10 but I also get stuck.
The VC I cannot prove is a "precondition safety" VC which goal is 
 goal WP_parameter_f_safety :
    same_block t1 t2 \/
     t1 = (null:pointer unsigned_intP) \/ t2 = (null:pointer 
unsigned_intP)
The previous axioms state that the second and third conditions evaluates 
to false.

I do not understand why such a VC is generated, could you help me 
understand please?
Best Regards,
Beno?t GERARD

[ENVOYE PAR INTERNET] 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130619/83248f7d/attachment.html>