diff --git a/Makefile b/Makefile
index 2480471e21dcd61dc588e36f212ddb203e47b3e2..d8f4f803ea19ec06624474811f18a59a2502a81a 100644
--- a/Makefile
+++ b/Makefile
@@ -168,7 +168,7 @@ force-reconfigure:
 ##############################################################################
 .PHONY: tests clean-tests
 
-TESTS=builtins callgraph cil constant_propagation float idct impact libc metrics misc occurrence pdg rte rte_manual scope slicing sparecode syntax test value jcdb journal
+TESTS=builtins callgraph cil constant_propagation float idct impact libc metrics misc occurrence pdg rte rte_manual scope slicing sparecode syntax test value jcdb journal spec
 tests: config.sed
 	find tests -name dune | grep -e "oracle.*/\|result.*/" | xargs --no-run-if-empty rm
 	dune exec -- ptests/ptests.exe
diff --git a/src/kernel_services/ast_data/ast.ml b/src/kernel_services/ast_data/ast.ml
index 1ff587fce07fce4de9d9223619bf712ee3d69ac4..37093f443f8b83a7f7efac2458c680fa828906c2 100644
--- a/src/kernel_services/ast_data/ast.ml
+++ b/src/kernel_services/ast_data/ast.ml
@@ -87,7 +87,9 @@ let () =
                  Cil_datatype.Varinfo.Hptset.self ];
   add_monotonic_state Cil_datatype.Stmt.Hptset.self;
   add_monotonic_state Cil_datatype.Varinfo.Hptset.self;
-  Cil.set_dependencies_of_ast self;
+  State_dependency_graph.add_dependencies ~from:self
+    [Cabshelper.Comments.self;Cil.selfFormalsDecl;
+     Cil.Frama_c_builtins.self;Cil.switch_case_state_self];
   Logic_env.init_dependencies self;
 
 exception Bad_Initialization of string
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 04582c3557e7c494163aa7e400bbd6ad1c7753b9..71a319595cd3b794c0d6145eb6d193f94b8a24d4 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -70,11 +70,6 @@ let () = Log.set_current_source (fun () -> fst (CurrentLoc.get ()))
 
 let pp_thisloc fmt = Location.pretty fmt (CurrentLoc.get ())
 
-let set_dependencies_of_ast, dependency_on_ast  =
-  let list_self = ref [] in
-  (fun ast -> State_dependency_graph.add_dependencies ~from:ast !list_self),
-  (fun state -> list_self := state :: !list_self)
-
 let voidType = Cil_const.voidType
 let intType = TInt(IInt,[])
 let uintType = TInt(IUInt,[])
@@ -698,7 +693,6 @@ module FormalsDecl =
     end)
 
 let selfFormalsDecl = FormalsDecl.self
-let () = dependency_on_ast selfFormalsDecl
 
 let makeFormalsVarDecl ?ghost (n,t,a) =
   let vi = makeVarinfo ?ghost ~temp:false false true n t in
@@ -4871,8 +4865,6 @@ module Frama_c_builtins =
       let size = 3
     end)
 
-let () = dependency_on_ast Frama_c_builtins.self
-
 let is_builtin v = hasAttribute "FC_BUILTIN" v.vattr
 
 let is_unused_builtin v = is_builtin v && not v.vreferenced
@@ -7165,7 +7157,8 @@ module Switch_cases =
       let dependencies = []
       let size = 49
     end)
-let () = dependency_on_ast Switch_cases.self
+
+let switch_case_state_self = Switch_cases.self
 let separate_switch_succs = Switch_cases.memo separate_switch_succs
 
 class dropAttributes ?select () = object
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index df110d9e57e479c9d9642a4aa05770c490d6b758..52b030aafbe623ced3815a3d59b3c56c478d40f4 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2316,14 +2316,7 @@ val separate_if_succs: stmt -> stmt * stmt
 
 (**/**)
 
-val dependency_on_ast: State.t -> unit
-(** indicates that the given state depends on the AST. *)
-
-val set_dependencies_of_ast : State.t -> unit
-(** Makes all states that have been marked as depending on the AST by
-    {!dependency_on_ast} depend on the given state. Should only be used
-    once when creating the AST state.
-*)
+val switch_case_state_self: State.t
 
 val pp_typ_ref: (Format.formatter -> typ -> unit) ref
 val pp_global_ref: (Format.formatter -> global -> unit) ref
diff --git a/src/kernel_services/parsetree/cabshelper.ml b/src/kernel_services/parsetree/cabshelper.ml
index 98bfca99fad1154402b5b27145a88793feab1e91..06e7abf6f1fa93b1e90d10ea8cf8b9f617ff1503 100644
--- a/src/kernel_services/parsetree/cabshelper.ml
+++ b/src/kernel_services/parsetree/cabshelper.ml
@@ -71,7 +71,6 @@ module Comments =
           let default () = MyTable.empty
          end)
     let self = MyState.self
-    let () = Cil.dependency_on_ast self
 
     (* What matters is the beginning of the comment. *)
     let add (first,last) comment =