From b3aa6f4a9297e1265e808bbee6cba206f87a849b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 1 Oct 2020 12:35:15 +0200
Subject: [PATCH] Fix problem of linking ordering of OCaml modules
remove Cil.set_dependencies_of_ast
---
Makefile | 2 +-
src/kernel_services/ast_data/ast.ml | 4 +++-
src/kernel_services/ast_queries/cil.ml | 11 ++---------
src/kernel_services/ast_queries/cil.mli | 9 +--------
src/kernel_services/parsetree/cabshelper.ml | 1 -
5 files changed, 7 insertions(+), 20 deletions(-)
diff --git a/Makefile b/Makefile
index 2480471e21d..d8f4f803ea1 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 1ff587fce07..37093f443f8 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 04582c3557e..71a319595cd 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 df110d9e57e..52b030aafbe 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 98bfca99fad..06e7abf6f1f 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 =
--
GitLab