Hi,
On Thu, Aug 27, 2009 at 12:03:15PM +0200, Roberto Bagnara wrote:
> Let us consider this example: [snip]
> Generally speaking, I wonder how the program verification
> tools based on CIL cope with this kind of problems (this
> is not the first such problem I report on the list).
This is definitely a bug in CIL. I just stumbled upon the relevant part
of the code and noticed that things are handled correctly in the case of
simple assignments, but not for compound assignements (as you noticed).
You will find a patch attached. Please, test it and tell me if anything
looks wrong in it. It fixes the above (snipped) example at least, and
should not break anything, but still…
> P.S. I just noticed that Frama-C uses a modified version
> of CIL: perhaps they have fixed these problems.
No, they haven't (AFAICT). But they could apply the attached patch
easily (provided it is correct).
Regards,
--
Gabriel Kerneis
diff -rN old-cil-darcs/src/frontc/cabs2cil.ml new-cil-darcs/src/frontc/cabs2cil.ml
3876c3876,3886
< let _, result' = castTo tresult (typeOfLval lv1) result in
---
> let tresult', result' = castTo tresult (typeOfLval lv1) result in
> (* Catch the case of an lval that might depend on itself,
> e.g. p[p[0]] when p[0] == 0. We need to use a temporary
> here if the result of the expression will be used:
> tmp := e1 bop e2; lv := tmp; use tmp as the result *)
> let needsTemp = match what, lv1 with
> (ADrop|AType), _ -> false
> | _, (Mem e, off) -> not (isConstant e)
> || not (isConstantOffset off)
> | _, (Var _, off) -> not (isConstantOffset off)
> in
3877a3888,3896
> if needsTemp then
> let descr = (dd_lval () lv1) in
> let tmp = var (newTempVar descr true tresult') in
> finishExp (se1 @@ se2 +++
> (Set(tmp, result', !currentLoc)) +++
> (Set(lv1, Lval tmp, !currentLoc)))
> (Lval tmp)
> t1
> else
------------------------------------------------------------------------------
Come build with us! The BlackBerry(R) Developer Conference in SF, CA
is the only developer event you need to attend this year. Jumpstart your
developing skills, take BlackBerry mobile applications to market and stay
ahead of the curve. Join us from November 9 - 12, 2009. Register now!
http://p.sf.net/sfu/devconference
_______________________________________________
CIL-users mailing list
CIL-users@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/cil-users
