diff --git a/src/kernel_services/ast_transformations/contract_special_float.ml b/src/kernel_services/ast_transformations/contract_special_float.ml
index fa2996946b088c563e6a59a8b3bfbf1bd64cd711..763b1fd5b493dfd02f108b132170c58f3c0dc0ec 100644
--- a/src/kernel_services/ast_transformations/contract_special_float.ml
+++ b/src/kernel_services/ast_transformations/contract_special_float.ml
@@ -121,14 +121,14 @@ let update_spec spec =
       spec.spec_complete_behaviors <- map_filter spec.spec_complete_behaviors;
       spec.spec_disjoint_behaviors <- map_filter spec.spec_disjoint_behaviors
 
-let visitor = object
-  inherit Cil.nopCilVisitor
-  method! vspec spec = update_spec spec; Cil.SkipChildren
-end
+let visit_global = function
+  | GFun (fundec, _) -> update_spec fundec.sspec
+  | GFunDecl (spec, _, _) -> update_spec spec
+  | _ -> ()
 
 let run ast =
   if Kernel.SpecialFloat.get () <> "none" then
-    Cil.visitCilFileSameGlobals visitor ast
+    Cil.iterGlobals ast visit_global
 
 let transform =
   File.register_code_transformation_category "contract_special_float"