From 6a59a791dfd9702214d8db8a91ac6499ea2b3158 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 20 Jan 2022 17:49:14 +0100
Subject: [PATCH] [kernel] Optimizes the [contract_special_float] code
transformation.
Only processes function specifications.
Does not use a visitor anymore.
---
.../ast_transformations/contract_special_float.ml | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/kernel_services/ast_transformations/contract_special_float.ml b/src/kernel_services/ast_transformations/contract_special_float.ml
index fa2996946b0..763b1fd5b49 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"
--
GitLab