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] Annotation pre-processing

  • Subject: [Frama-c-discuss] Annotation pre-processing
  • From: benoit.gerard at dga.defense.gouv.fr (benoit.gerard at dga.defense.gouv.fr)
  • Date: Wed, 19 Jun 2013 10:12:09 +0200
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>