--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on December 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Pointer Aliasing



 

Hi everyone!

 

I?m trying to define the following precondition: for two pointers u1 and u2,
I want to say that the pointers are not in the same block memory, i.e.  

\base_addr(u1)!=\base_addr(u2). 

 

But it seems that Jessie Puglin doesn?t support this feature (I suppose that
base_addr is not yet supported, because with this annotation Jessie produces
an error as output). 

 

 I tried to define 

                u1 != u2

 

But the hypothesis that is generated in Coq is sub_pointer u1 u2 = 0 ->
false, and I can?t do anything with this hypothesis.

(I want to use this to prove that  (shift u1 k) != (shift u2 k) ).

 

I was wondering, if adding the axioms, initial defined in caduceus.why,
which are related with the \base_addr predicate to the why file (generated
after compile the Jessie file) will not solve the problem, and then change
the annotation in the pre-condition of why code to base_addr(u1) <>
base_addr(u2). 

 

But I really don?t know if I do this, I will not introduce some
contradiction in the why code, because Frama-C memory model is different
from Caduceus memory model.

 

I really need this annotation in the code, and one possible solution is to
change the why code that is generated by the compiler. Is that any way in
why to introduce this assertion?

 

Note: I?m using Frama-C Helium version, because I need some features
available in this version.

 

Thanks for everything.

Best regards,

B?rbara 

    

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081203/de8ebfc0/attachment.html