Hi again,
I cannot find what is going wrong, but a few comments and ideas anyway:
> open Pretty
> open Cil
>
> class svaModifyVisitor varlist = object(self)
> inherit nopCilVisitor
>
> method vstmt s =
> let verify_func = emptyFunction "someFunction" in
> let verify_exp = (Lval((Var(verify_func.svar)),NoOffset)) in
> match s.skind with
> | Loop(_,loc,_,_) ->
> ignore (printf "VSTMT: Loop() at %s:%i\n" loc.file loc.line);
> self#queueInstr [Call(None,verify_exp,[],loc)];
> DoChildren;
Random fix (should not work, but I'm trying things just in case):
| Loop(_,loc,_,_) ->
ignore (printf "VSTMT: Loop() at %s:%i\n" loc.file loc.line);
ChangeDoChildrenPost(s, fun s ->
self#queueInstr [Call(None,verify_exp,[],loc)];
s)
> | _ -> DoChildren;
> end
You could merge this visitor with the following one: add the vstmt
method to svaAnalyzeVisitor and change vglob to "DoChildren" on GFun and
"SkipChildren" otherwise.
Let me know if this (coincidentally) fixes the problem.
> class svaAnalyzeVisitor f = object
> inherit nopCilVisitor (* only look at function bodies *)
> method vglob gl = match gl with
> GFun(fundec,funloc) ->
> let modify = new svaModifyVisitor [] in
> fundec.sbody <- visitCilBlock modify fundec.sbody ;
> ChangeTo([GFun(fundec,funloc)])
ChangeTo is useless: you modify fundec.sbody in an imperative fashion
above, so returning SkipChildren would be juste fine.
> | _ -> DoChildren
Here, SkipChildren will save some time too (since you won't find any
GFun anyway).
> end
>
> let sva (f : file) =
> visitCilFile (new svaAnalyzeVisitor f) f;
> f
Returning f is useless here too. It has been modified by visitCilFile
(which should be visitCilFileSameGlobals in your case, using the
SkipChildren explained above), and the caller obviously knows f already.
>
> let default_sva (f : file) =
> ignore (sva f)
>
> let feature1 : featureDescr =
> { fd_name = "sva";
> fd_enabled = Cilutil.doSva;
> fd_description = "blabla";
> fd_extraopt = [];
> fd_doit = (function (f: file) -> default_sva f);
> fd_post_check = true;
> }
What you might want to do is a few "E.log" just before every
call to assertEmptyQueue in cil.ml to track down where the bug happens
exactly. Setting debugVisit to true (in cil.ml) could also help.
(I never used queueInstr, but I studied extensively the code of the
visitor, hence my lack of experience.)
Regards,
--
Gabriel Kerneis
------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now. http://p.sf.net/sfu/bobj-july
_______________________________________________
CIL-users mailing list
CIL-users@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/cil-users
