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