diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index db32e083853b0f47d2e51061cde25d9e19676f46..3533691b55f7a5a731cd1fc42f4ac255547d7a8e 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -5263,6 +5263,14 @@ class constFoldVisitorClass (machdep: bool) : cilVisitor = object (* Do it bottom up *) ChangeDoChildrenPost (e, constFold machdep) + (* Optimization: only visits function and variable definitions. *) + method! vglob = function + | GFun _ | GVar _ -> DoChildren + | _ -> SkipChildren + + method! vtype _ = SkipChildren + method! vspec _ = SkipChildren + method! vcode_annot _ = SkipChildren end let constFoldVisitor (machdep: bool) = new constFoldVisitorClass machdep