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

Hi,

The explanation for this VC is that in the design of Jessie, it was
decided that pointer comparison should be allowed only for pointers to
the same block of memory. This is clearly desirable for <, >, <= and >=,
and indeed questionable for == and !=. In fact, as you can see, for
equality it is also allowed to compare with NULL. At some point it was
decided to keep disallowing equality tests for non-null pointers if they
do not point to the same block, but I must admit I do not remember the
reason.

(Note: this has nothing to do with the separation policy, the same
phenomenon would appear in both policies)

That being said, you should be aware that the proper way of expressing
"pointers must not point to the same memory area" is

requires \base_addr(t1) != \base_addr(t2)

Final thing: if you plan to verify "low-level" C code, "low-level" in
the sense that the memory layout of data is important, then Jessie is
probably not the best choice, I'd like to recommend using the WP plugin
instead, with the so-called "RunTime" memory model.


Hope this helps,

- Claude


Le 19/06/2013 10:12, benoit.gerard at dga.defense.gouv.fr a ?crit :
> 
> 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]
> 
> 
> _______________________________________________
> 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
> 

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |