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] Pointer Aliasing

  • Subject: [Frama-c-discuss] Pointer Aliasing
  • From: barbaraisabelvieira at gmail.com (Bárbara Vieira)
  • Date: Wed Dec 3 16:23:38 2008
 

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