diff --git a/Changelog b/Changelog
index fdaed1119a1e396b13b59cbfb63c3f05ad63473b..28fc8cd5ea97a3cd4a75d1ad6c4fdc4b39895a55 100644
--- a/Changelog
+++ b/Changelog
@@ -21,6 +21,8 @@ Open Source Release <next-release>
o Kernel [2022-02-23] New visitor functions visitFramacFileFunctions
and visitCilFileFunctions to visit only function definitions,
for better performance.
+o! [kernel] [2022-02-23] Remove State_selection.Static (deprecated since
+ 10 years, use directly State_selection instead)
-* Kernel [2022-02-22] Fix list of potential types for decimal
integer literal constants
* Kernel [2022-02-17] Reject programs using unsupported
@@ -28,6 +30,9 @@ o Kernel [2022-02-23] New visitor functions visitFramacFileFunctions
* Kernel [2022-02-08] Reject array whose size is too big with a proper
error message instead of a crash (fixes ##2590)
o! Kernel [2022-01-19] Removed obsolete AST nodes IndexPI and Info
+o! Kernel [2022-02-19] Removed obsolete AST nodes IndexPI and Info
+* Kernel [2022-02-08] Reject array whose size is too big with a proper
+ error message instead of a crash (fixes ##2590)
o! Kernel [2021-12-03] Remove unused AST node Dcustom_annot and field
fpadding_in_bits. Do not cache size of types in the AST but in
a dedicated table.
diff --git a/bin/migration_scripts/chromium2manganese.sh b/bin/migration_scripts/chromium2manganese.sh
index bbdd045f4b7929eec5ba177745271336b1529dbd..9943edfa253fa68ca17c30f513c3a54eae4ac0d9 100755
--- a/bin/migration_scripts/chromium2manganese.sh
+++ b/bin/migration_scripts/chromium2manganese.sh
@@ -89,6 +89,7 @@ process_file ()
-e 's/(Integer\.pretty ~hexa:true)/Integer.pretty_hex/g' \
-e 's/Integer\.pretty ~hexa:false/Integer.pretty/g' \
-e 's/Integer\.pretty ~hexa:true/Integer.pretty_hex/g' \
+ -e 's/State_selection\.Static/State_selection/g'
# this line left empty on purpose
}
diff --git a/src/kernel_services/ast_data/ast.ml b/src/kernel_services/ast_data/ast.ml
index c02b22a6acb0022ad519d3351b26cb8e4a236062..e8e0396778181eb91d3734ae0df93a4452d557f3 100644
--- a/src/kernel_services/ast_data/ast.ml
+++ b/src/kernel_services/ast_data/ast.ml
@@ -208,7 +208,7 @@ let is_def_or_last_decl g =
| _ -> false
let clear_last_decl () =
- let selection = State_selection.Static.with_dependencies LastDecl.self in
+ let selection = State_selection.with_dependencies LastDecl.self in
Project.clear ~selection ()
let add_hook_on_update f =
diff --git a/src/kernel_services/plugin_entry_points/emitter.ml b/src/kernel_services/plugin_entry_points/emitter.ml
index 7b9005743b00145bb7b9a6064eefff258a6c7498..43d4b82ef8d8a26eec2b40b0bc2bb48636354b04 100644
--- a/src/kernel_services/plugin_entry_points/emitter.ml
+++ b/src/kernel_services/plugin_entry_points/emitter.ml
@@ -387,7 +387,7 @@ let register_tuning_parameter name p =
let () =
Cmdline.run_after_extended_stage
(fun () ->
- State_selection.Static.iter
+ State_selection.iter
(fun s ->
let tbl = Datatype.String.Hashtbl.create 7 in
let p = Typed_parameter.get (State.get_name s) in
diff --git a/src/libraries/project/state_selection.ml b/src/libraries/project/state_selection.ml
index 1ebecc9cb3f36c3fcc838cd62b26060ba307db81..1b47451c304629169556911d8dfe05cb382a6880 100644
--- a/src/libraries/project/state_selection.ml
+++ b/src/libraries/project/state_selection.ml
@@ -106,158 +106,132 @@ include Datatype.Make
Type.par p_caller Type.Call fmt pp
end)
-module type S = sig
- val with_dependencies: State.t -> t
- val only_dependencies: State.t -> t
- val with_codependencies: State.t -> t
- val only_codependencies: State.t -> t
- val union: t -> t -> t
- val list_union: t list -> t
- val diff: t -> t -> t
- val cardinal: t -> int
- val to_list: t -> State.t list
- val pretty: Format.formatter -> t -> unit
- val pretty_witness: Format.formatter -> t -> unit
- val iter_succ: (State.t -> unit) -> t -> State.t -> unit
- val fold_succ: (State.t -> 'a -> 'a) -> t -> State.t -> 'a -> 'a
- val iter: (State.t -> unit) -> t -> unit
- val fold: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
- val iter_in_order: (State.t -> unit) -> t -> unit
- val fold_in_order: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
-end
-
-module Static = struct
-
- let transitive_closure next_vertices s =
- let rec visit acc v =
- next_vertices
- (fun v' acc ->
- let e = v, v' in
- if Selection.mem_edge_e acc e then acc
- else visit (Selection.add_edge_e acc e) v')
- State_dependency_graph.graph v acc
- in
- (* add [s] in the selection even if it has no ingoing/outgoing edges *)
- visit (Selection.add_vertex Selection.empty s) s
-
- let with_dependencies s =
- Subset (transitive_closure State_dependency_graph.G.fold_succ s),
- WDependencies s
-
- let with_codependencies s =
- Subset (transitive_closure State_dependency_graph.G.fold_pred s),
- WCoDependencies s
-
- let only_dependencies s =
- let g = transitive_closure State_dependency_graph.G.fold_succ s in
- Subset (Selection.remove_vertex g s), WStrictDependencies s
-
- let only_codependencies s =
- let g = transitive_closure State_dependency_graph.G.fold_pred s in
- Subset (Selection.remove_vertex g s), WStrictCoDependencies s
-
- let diff (sel1, w1) (sel2, w2 as selw2) =
- let sel = match sel1, sel2 with
- | _, Full -> Subset Selection.empty
- | Full, _sel2 when is_empty selw2 -> Full
- | Full, Subset sel2 ->
- let selection =
- State_dependency_graph.G.fold_vertex
- (fun v acc ->
- if Selection.mem_vertex sel2 v then acc
- else Selection.add_vertex acc v)
- State_dependency_graph.graph
- Selection.empty
- in
- let sel =
- State_dependency_graph.G.fold_edges
- (fun v1 v2 acc ->
- if Selection.mem_vertex sel2 v1 || Selection.mem_vertex sel2 v2
- then acc
- else Selection.add_edge acc v1 v2)
- State_dependency_graph.graph
- selection
- in
- Subset sel
- | Subset sel1, Subset sel2 ->
- Subset
- (Selection.fold_vertex
- (fun v acc -> Selection.remove_vertex acc v) sel2 sel1)
- in
- sel, WDiff (w1, w2)
-
- module Operations = Graph.Oper.P(Selection)
-
- let union (sel1, w1) (sel2, w2) =
- let sel = match sel1, sel2 with
- | Full, _ | _, Full -> Full
- | Subset sel1, Subset sel2 -> Subset (Operations.union sel1 sel2)
- in
- sel, WUnion (w1, w2)
-
- let list_union l =
- let sel, _ = List.fold_left union empty l in
- let w = WOfList (List.map snd l) in
- sel, w
-
- let cardinal (sel, _) = match sel with
- | Full -> State_dependency_graph.G.nb_vertex State_dependency_graph.graph
- | Subset sel -> Selection.nb_vertex sel
-
- let iter_succ f (sel, _) v = match sel with
- | Full ->
- State_dependency_graph.G.iter_succ f State_dependency_graph.graph v
- | Subset sel -> Selection.iter_succ f sel v
-
- let fold_succ f (sel, _) v acc = match sel with
- | Full ->
- State_dependency_graph.G.fold_succ f State_dependency_graph.graph v acc
- | Subset sel -> Selection.fold_succ f sel v acc
-
- let iter f (sel, _) = match sel with
- | Full ->
- State_dependency_graph.G.iter_vertex f State_dependency_graph.graph
- | Subset sel -> Selection.iter_vertex f sel
-
- let fold f (sel, _) acc = match sel with
- | Full ->
- State_dependency_graph.G.fold_vertex f State_dependency_graph.graph acc
- | Subset sel -> Selection.fold_vertex f sel acc
-
- let to_list s = fold (fun s acc -> s :: acc) s []
-
- module TG = State_topological.Make(State_dependency_graph.G)
- module TS = State_topological.Make(Selection)
-
- let iter_in_order f (sel, _) = match sel with
- | Full -> TG.iter f State_dependency_graph.graph
- | Subset sel -> TS.iter f sel
-
- let fold_in_order f (sel, _) acc = match sel with
- | Full -> TG.fold f State_dependency_graph.graph acc
- | Subset sel -> TS.fold f sel acc
-
- let pretty fmt sel =
- Format.fprintf fmt "contents of the selection:@\n";
- let mem s =
- State_dependency_graph.G.mem_vertex
- State_dependency_graph.graph
- s
- in
- iter_in_order
- (fun s ->
- Format.fprintf fmt "\t state %S%s@\n"
- (State.get_unique_name s)
- (if mem s then "" else "(\"" ^ State.get_name s ^ "\")"))
- sel;
- Format.pp_print_flush fmt ()
-
- let pretty_witness fmt (_, w) =
- pretty_witness fmt w
-
-end
-
-include Static
+let transitive_closure next_vertices s =
+ let rec visit acc v =
+ next_vertices
+ (fun v' acc ->
+ let e = v, v' in
+ if Selection.mem_edge_e acc e then acc
+ else visit (Selection.add_edge_e acc e) v')
+ State_dependency_graph.graph v acc
+ in
+ (* add [s] in the selection even if it has no ingoing/outgoing edges *)
+ visit (Selection.add_vertex Selection.empty s) s
+
+let with_dependencies s =
+ Subset (transitive_closure State_dependency_graph.G.fold_succ s),
+ WDependencies s
+
+let with_codependencies s =
+ Subset (transitive_closure State_dependency_graph.G.fold_pred s),
+ WCoDependencies s
+
+let only_dependencies s =
+ let g = transitive_closure State_dependency_graph.G.fold_succ s in
+ Subset (Selection.remove_vertex g s), WStrictDependencies s
+
+let only_codependencies s =
+ let g = transitive_closure State_dependency_graph.G.fold_pred s in
+ Subset (Selection.remove_vertex g s), WStrictCoDependencies s
+
+let diff (sel1, w1) (sel2, w2 as selw2) =
+ let sel = match sel1, sel2 with
+ | _, Full -> Subset Selection.empty
+ | Full, _sel2 when is_empty selw2 -> Full
+ | Full, Subset sel2 ->
+ let selection =
+ State_dependency_graph.G.fold_vertex
+ (fun v acc ->
+ if Selection.mem_vertex sel2 v then acc
+ else Selection.add_vertex acc v)
+ State_dependency_graph.graph
+ Selection.empty
+ in
+ let sel =
+ State_dependency_graph.G.fold_edges
+ (fun v1 v2 acc ->
+ if Selection.mem_vertex sel2 v1 || Selection.mem_vertex sel2 v2
+ then acc
+ else Selection.add_edge acc v1 v2)
+ State_dependency_graph.graph
+ selection
+ in
+ Subset sel
+ | Subset sel1, Subset sel2 ->
+ Subset
+ (Selection.fold_vertex
+ (fun v acc -> Selection.remove_vertex acc v) sel2 sel1)
+ in
+ sel, WDiff (w1, w2)
+
+module Operations = Graph.Oper.P(Selection)
+
+let union (sel1, w1) (sel2, w2) =
+ let sel = match sel1, sel2 with
+ | Full, _ | _, Full -> Full
+ | Subset sel1, Subset sel2 -> Subset (Operations.union sel1 sel2)
+ in
+ sel, WUnion (w1, w2)
+
+let list_union l =
+ let sel, _ = List.fold_left union empty l in
+ let w = WOfList (List.map snd l) in
+ sel, w
+
+let cardinal (sel, _) = match sel with
+ | Full -> State_dependency_graph.G.nb_vertex State_dependency_graph.graph
+ | Subset sel -> Selection.nb_vertex sel
+
+let iter_succ f (sel, _) v = match sel with
+ | Full ->
+ State_dependency_graph.G.iter_succ f State_dependency_graph.graph v
+ | Subset sel -> Selection.iter_succ f sel v
+
+let fold_succ f (sel, _) v acc = match sel with
+ | Full ->
+ State_dependency_graph.G.fold_succ f State_dependency_graph.graph v acc
+ | Subset sel -> Selection.fold_succ f sel v acc
+
+let iter f (sel, _) = match sel with
+ | Full ->
+ State_dependency_graph.G.iter_vertex f State_dependency_graph.graph
+ | Subset sel -> Selection.iter_vertex f sel
+
+let fold f (sel, _) acc = match sel with
+ | Full ->
+ State_dependency_graph.G.fold_vertex f State_dependency_graph.graph acc
+ | Subset sel -> Selection.fold_vertex f sel acc
+
+let to_list s = fold (fun s acc -> s :: acc) s []
+
+module TG = State_topological.Make(State_dependency_graph.G)
+module TS = State_topological.Make(Selection)
+
+let iter_in_order f (sel, _) = match sel with
+ | Full -> TG.iter f State_dependency_graph.graph
+ | Subset sel -> TS.iter f sel
+
+let fold_in_order f (sel, _) acc = match sel with
+ | Full -> TG.fold f State_dependency_graph.graph acc
+ | Subset sel -> TS.fold f sel acc
+
+let pretty fmt sel =
+ Format.fprintf fmt "contents of the selection:@\n";
+ let mem s =
+ State_dependency_graph.G.mem_vertex
+ State_dependency_graph.graph
+ s
+ in
+ iter_in_order
+ (fun s ->
+ Format.fprintf fmt "\t state %S%s@\n"
+ (State.get_unique_name s)
+ (if mem s then "" else "(\"" ^ State.get_name s ^ "\")"))
+ sel;
+ Format.pp_print_flush fmt ()
+
+let pretty_witness fmt (_, w) =
+ pretty_witness fmt w
(*
Local Variables:
diff --git a/src/libraries/project/state_selection.mli b/src/libraries/project/state_selection.mli
index 3c0517faa5f6e6ce9506daea23699f1a583c8765..3a97d3488988fd17848791879149d62e84ca23b5 100644
--- a/src/libraries/project/state_selection.mli
+++ b/src/libraries/project/state_selection.mli
@@ -77,113 +77,99 @@ val mem: t -> State.t -> bool
(** {2 Specific selections} *)
(* ************************************************************************** *)
-(** Operations over selections which depend on a State Dependency Graph
- implementation.
- @since Carbon-20101201 *)
-module type S = sig
-
- (* ************************************************************************ *)
- (** {2 Builders from dependencies} *)
- (* ************************************************************************ *)
-
- val with_dependencies: State.t -> t
- (** The selection containing the given state and all its dependencies.
- @since Carbon-20101201
- @plugin development guide *)
- val only_dependencies: State.t -> t
- (** The selection containing all the dependencies of the given state (but not
- this state itself).
- @since Carbon-20101201
- @plugin development guide *)
+(* ************************************************************************ *)
+(** {3 Builders from dependencies} *)
+(* ************************************************************************ *)
- val with_codependencies: State.t -> t
- (** The selection containing the given state and all its co-dependencies.
- @since Carbon-20101201 *)
+val with_dependencies: State.t -> t
+(** The selection containing the given state and all its dependencies.
+ @since Carbon-20101201
+ @plugin development guide *)
- val only_codependencies: State.t -> t
- (** The selection containing all the co-dependencies of the given state (but
- not this state itself).
- @since Carbon-20101201 *)
+val only_dependencies: State.t -> t
+(** The selection containing all the dependencies of the given state (but not
+ this state itself).
+ @since Carbon-20101201
+ @plugin development guide *)
- (* ************************************************************************ *)
- (** {2 Builders by operations over sets} *)
- (* ************************************************************************ *)
+val with_codependencies: State.t -> t
+(** The selection containing the given state and all its co-dependencies.
+ @since Carbon-20101201 *)
- val union: t -> t -> t
- (** Union of two selections.
- @since Carbon-20101201 *)
+val only_codependencies: State.t -> t
+(** The selection containing all the co-dependencies of the given state (but
+ not this state itself).
+ @since Carbon-20101201 *)
- val list_union: t list -> t
- (** Union of an arbitrary number of selection (0 gives an empty selection)
- @since Oxygen-20120901
- *)
+(* ************************************************************************ *)
+(** {3 Builders by operations over sets} *)
+(* ************************************************************************ *)
- val diff: t -> t -> t
- (** Difference between two selections.
- @since Carbon-20101201 *)
+val union: t -> t -> t
+(** Union of two selections.
+ @since Carbon-20101201 *)
- (* ************************************************************************ *)
- (** {2 Specific Getters} *)
- (* ************************************************************************ *)
+val list_union: t list -> t
+(** Union of an arbitrary number of selection (0 gives an empty selection)
+ @since Oxygen-20120901
+*)
- val cardinal: t -> int
- (** Size of a selection.
- @since Carbon-20101201 *)
+val diff: t -> t -> t
+(** Difference between two selections.
+ @since Carbon-20101201 *)
- val to_list: t -> State.t list
- (** Convert a selection into a list of states.
- @since Fluorine-20130401 *)
+(* ************************************************************************ *)
+(** {3 Specific Getters} *)
+(* ************************************************************************ *)
- val pretty: Format.formatter -> t -> unit
- (** Display a selection.
- @since Carbon-20101201 *)
+val cardinal: t -> int
+(** Size of a selection.
+ @since Carbon-20101201 *)
- val pretty_witness: Format.formatter -> t -> unit
- (** Display a selection in a more concise form. (Using the atomic operations
- that were used to create it.)
- @since Aluminium-20160501 *)
+val to_list: t -> State.t list
+(** Convert a selection into a list of states.
+ @since Fluorine-20130401 *)
+val pretty: Format.formatter -> t -> unit
+(** Display a selection.
+ @since Carbon-20101201 *)
- (** {3 Iterators} *)
+val pretty_witness: Format.formatter -> t -> unit
+(** Display a selection in a more concise form. (Using the atomic operations
+ that were used to create it.)
+ @since Aluminium-20160501 *)
- val iter_succ: (State.t -> unit) -> t -> State.t -> unit
- (** Iterate over the successor of a state in a selection.
- The order is unspecified.
- @since Carbon-20101201 *)
- val fold_succ: (State.t -> 'a -> 'a) -> t -> State.t -> 'a -> 'a
- (** Iterate over the successor of a state in a selection.
- The order is unspecified.
- @since Carbon-20101201 *)
+(** {3 Iterators} *)
- val iter: (State.t -> unit) -> t -> unit
- (** Iterate over a selection. The order is unspecified.
- @since Carbon-20101201 *)
+val iter_succ: (State.t -> unit) -> t -> State.t -> unit
+(** Iterate over the successor of a state in a selection.
+ The order is unspecified.
+ @since Carbon-20101201 *)
- val fold: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
- (** Fold over a selection. The order is unspecified.
- @since Carbon-20101201 *)
+val fold_succ: (State.t -> 'a -> 'a) -> t -> State.t -> 'a -> 'a
+(** Iterate over the successor of a state in a selection.
+ The order is unspecified.
+ @since Carbon-20101201 *)
- val iter_in_order: (State.t -> unit) -> t -> unit
- (** Iterate over a selection in a topological ordering compliant with the
- State Dependency Graph. Less efficient that {!iter}.
- @since Carbon-20101201 *)
+val iter: (State.t -> unit) -> t -> unit
+(** Iterate over a selection. The order is unspecified.
+ @since Carbon-20101201 *)
- val fold_in_order: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
- (** Fold over a selection in a topological ordering compliant with the
- State Dependency Graph. Less efficient that {!iter}.
- @since Carbon-20101201 *)
+val fold: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
+(** Fold over a selection. The order is unspecified.
+ @since Carbon-20101201 *)
-end
+val iter_in_order: (State.t -> unit) -> t -> unit
+(** Iterate over a selection in a topological ordering compliant with the
+ State Dependency Graph. Less efficient that {!iter}.
+ @since Carbon-20101201 *)
-(** Operations over selections which depend on
- {!State_dependency_graph.graph}.
- @since Carbon-20101201
- @deprecated Oxygen-20120901 directly use equivalent top-level function
- instead. *)
-module Static: S
-include S
+val fold_in_order: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
+(** Fold over a selection in a topological ordering compliant with the
+ State Dependency Graph. Less efficient that {!iter}.
+ @since Carbon-20101201 *)
(*
Local Variables:
diff --git a/src/plugins/obfuscator/obfuscator_register.ml b/src/plugins/obfuscator/obfuscator_register.ml
index 732fc2a8dda516e517f5af573effc3c24ba56477..d51b878bd548fe63463c00e4e83a3438860d237f 100644
--- a/src/plugins/obfuscator/obfuscator_register.ml
+++ b/src/plugins/obfuscator/obfuscator_register.ml
@@ -23,14 +23,14 @@
let disable_other_analyzers () =
if Options.Run.get () then
let selection =
- State_selection.Static.diff
+ State_selection.diff
(Parameter_state.get_selection ())
- (State_selection.Static.union
+ (State_selection.union
(State_selection.of_list
(Kernel.CodeOutput.self :: Options.states))
(* The command-line options that govern the creation of the AST
must be preserved *)
- (State_selection.Static.with_codependencies Ast.self))
+ (State_selection.with_codependencies Ast.self))
in
Project.clear ~selection ()
diff --git a/src/plugins/report/tests/report/multi_emitters.ml b/src/plugins/report/tests/report/multi_emitters.ml
index c007c0b47fc2a7648c5f828ae1e8023ba97d564b..9680545a9181782f63276fbecd1d738d3c498784 100644
--- a/src/plugins/report/tests/report/multi_emitters.ml
+++ b/src/plugins/report/tests/report/multi_emitters.ml
@@ -1,28 +1,28 @@
-let emitter1 =
+let emitter1 =
Emitter.create "Test1" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
-let emitter2 =
+let emitter2 =
Emitter.create "Test2" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
let set_status e s =
- Kernel.feedback "%a SET STATUS TO %a"
+ Kernel.feedback "%a SET STATUS TO %a"
Emitter.pretty e Property_status.Emitted_status.pretty s;
Annotations.iter_all_code_annot
(fun stmt _ ca ->
- let kf = Kernel_function.find_englobing_kf stmt in
- let ps = Property.ip_of_code_annot kf stmt ca in
- List.iter (fun p -> Property_status.emit e p ~hyps:[] s) ps)
+ let kf = Kernel_function.find_englobing_kf stmt in
+ let ps = Property.ip_of_code_annot kf stmt ca in
+ List.iter (fun p -> Property_status.emit e p ~hyps:[] s) ps)
let print_status =
Dynamic.get
~plugin:"Report"
- "print"
+ "print"
(Datatype.func Datatype.unit Datatype.unit)
let clear () =
Kernel.feedback "CLEARING";
Project.clear
- ~selection:(State_selection.Static.with_dependencies Property_status.self)
+ ~selection:(State_selection.with_dependencies Property_status.self)
()
let main () =
@@ -31,7 +31,7 @@ let main () =
set_status emitter1 Property_status.Dont_know;
set_status emitter2 Property_status.Dont_know;
(* unknown /\ unknown *)
- print_status ();
+ print_status ();
(* unknown /\ true *)
set_status emitter1 Property_status.True;
print_status ();
diff --git a/src/plugins/report/tests/report/no_hyp.ml b/src/plugins/report/tests/report/no_hyp.ml
index a145963f447e8e630717bf5a0a162627a51bf43f..ecc7d9b45051bd034248a154eec671e6dcf52fd7 100644
--- a/src/plugins/report/tests/report/no_hyp.ml
+++ b/src/plugins/report/tests/report/no_hyp.ml
@@ -4,9 +4,9 @@ let emitter =
let set_status s =
Annotations.iter_all_code_annot
(fun stmt _ ca ->
- let kf = Kernel_function.find_englobing_kf stmt in
- let ps = Property.ip_of_code_annot kf stmt ca in
- List.iter (fun p -> Property_status.emit emitter p ~hyps:[] s) ps)
+ let kf = Kernel_function.find_englobing_kf stmt in
+ let ps = Property.ip_of_code_annot kf stmt ca in
+ List.iter (fun p -> Property_status.emit emitter p ~hyps:[] s) ps)
let print_status =
Dynamic.get
@@ -16,7 +16,7 @@ let print_status =
let clear () =
Project.clear
- ~selection:(State_selection.Static.with_dependencies Property_status.self)
+ ~selection:(State_selection.with_dependencies Property_status.self)
()
let main () =
diff --git a/src/plugins/report/tests/report/several_hyps.ml b/src/plugins/report/tests/report/several_hyps.ml
index 7f1d3da239dc2f9016de48c339745ac6c5f4f477..449f819dba78753b829f2139ba624e7554dcb2fb 100644
--- a/src/plugins/report/tests/report/several_hyps.ml
+++ b/src/plugins/report/tests/report/several_hyps.ml
@@ -1,13 +1,13 @@
open Cil_types
-let emitter =
+let emitter =
Emitter.create "Test" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
-let emitter2 =
+let emitter2 =
Emitter.create "Test2" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
let set_status ?(emitter=emitter) p hyps s =
- Kernel.feedback "SETTING STATUS OF %a TO %a"
+ Kernel.feedback "SETTING STATUS OF %a TO %a"
Property.pretty p
Property_status.Emitted_status.pretty s;
Property_status.emit emitter p ~hyps s
@@ -15,13 +15,13 @@ let set_status ?(emitter=emitter) p hyps s =
let print_status =
Dynamic.get
~plugin:"Report"
- "print"
+ "print"
(Datatype.func Datatype.unit Datatype.unit)
let clear () =
Kernel.feedback "CLEARING";
Project.clear
- ~selection:(State_selection.Static.with_dependencies Property_status.self)
+ ~selection:(State_selection.with_dependencies Property_status.self)
()
let main () =
@@ -30,13 +30,13 @@ let main () =
let main, j, i, h, g =
let l =
Annotations.fold_all_code_annot
- (fun stmt _ ca acc ->
- let kf = Kernel_function.find_englobing_kf stmt in
- let ps = Property.ip_of_code_annot kf stmt ca in
- match ps with
- | [ p ] -> p :: acc
- | _ -> assert false)
- []
+ (fun stmt _ ca acc ->
+ let kf = Kernel_function.find_englobing_kf stmt in
+ let ps = Property.ip_of_code_annot kf stmt ca in
+ match ps with
+ | [ p ] -> p :: acc
+ | _ -> assert false)
+ []
in
match l with
| [ p1; p2; p3; p4; p5 ] -> p1, p2, p3, p4, p5
@@ -57,7 +57,7 @@ let main () =
clear ();
f ()
in
- let test msg ?(hyps=hyps) set_status_hyps =
+ let test msg ?(hyps=hyps) set_status_hyps =
Kernel.feedback msg;
reset set_status_hyps;
(* unknown *)
@@ -72,33 +72,33 @@ let main () =
print_status ()
in
let nothing () = () in
- let valid ?(g=g) ?(i=i) () =
- let _i = i in set_status g [] Property_status.True
+ let valid ?(g=g) ?(i=i) () =
+ let _i = i in set_status g [] Property_status.True
in
- let valid_under_hyp ?(g=g) ?(i=i) () =
+ let valid_under_hyp ?(g=g) ?(i=i) () =
set_status g [ i ] Property_status.True in
- let unknown ?(g=g) ?(i=i) () =
- let _i = i in set_status g [] Property_status.Dont_know
+ let unknown ?(g=g) ?(i=i) () =
+ let _i = i in set_status g [] Property_status.Dont_know
in
- let invalid ?(g=g) ?(i=i) () =
- let _i = i in set_status g [] Property_status.False_and_reachable
+ let invalid ?(g=g) ?(i=i) () =
+ let _i = i in set_status g [] Property_status.False_and_reachable
in
- let invalid_under_hyp ?(g=g) ?i:_ () =
- set_status g [ ] Property_status.False_and_reachable
+ let invalid_under_hyp ?(g=g) ?i:_ () =
+ set_status g [ ] Property_status.False_and_reachable
in
let invalid_but_dead ?(g=g) ?(i=i) () =
set_status i [] Property_status.False_and_reachable;
- set_status g [ ] Property_status.False_and_reachable
+ set_status g [ ] Property_status.False_and_reachable
in
- let valid_but_dead ?(g=g) ?(i=i) () =
+ let valid_but_dead ?(g=g) ?(i=i) () =
set_status i [] Property_status.False_and_reachable;
- set_status g [ ] Property_status.True
+ set_status g [ ] Property_status.True
in
- let unknown_but_dead ?(g=g) ?(i=i) () =
+ let unknown_but_dead ?(g=g) ?(i=i) () =
set_status i [] Property_status.False_and_reachable;
- set_status g [ i ] Property_status.Dont_know
+ set_status g [ i ] Property_status.Dont_know
in
- let inconsistent ?(g=g) ?(i=i) () =
+ let inconsistent ?(g=g) ?(i=i) () =
let _i = i in
set_status g [ ] Property_status.True;
set_status ~emitter:emitter2 g [] Property_status.False_and_reachable
@@ -129,9 +129,9 @@ let main () =
test "CONSIDERED_VALID + INCONSISTENT" ~hyps inconsistent;
(***************************************************************************)
let set status_g status_h () =
-(* (status_h: ?g:Property.t -> ?i:Property.t -> unit -> unit) () =*)
+ (* (status_h: ?g:Property.t -> ?i:Property.t -> unit -> unit) () =*)
status_g ();
-(* status_h ~g:h ~i:j ()*)
+ (* status_h ~g:h ~i:j ()*)
status_h ?g:(Some h) ?i:(Some j) ()
in
test "VALID + VALID" (set valid valid);
@@ -144,16 +144,16 @@ let main () =
test "VALID + UNKNOWN_BUT_DEAD" (set valid unknown_but_dead);
test "VALID + INCONSISTENT" (set valid inconsistent);
(***************************************************************************)
- test "VALID_UNDER_HYP + VALID_UNDER_HYP"
+ test "VALID_UNDER_HYP + VALID_UNDER_HYP"
(set valid_under_hyp valid_under_hyp);
test "VALID_UNDER_HYP + UNKNOWN" (set valid_under_hyp unknown);
test "VALID_UNDER_HYP + INVALID" (set valid_under_hyp invalid);
- test "VALID_UNDER_HYP + INVALID_UNDER_HYP"
+ test "VALID_UNDER_HYP + INVALID_UNDER_HYP"
(set valid_under_hyp invalid_under_hyp);
- test "VALID_UNDER_HYP + INVALID_BUT_DEAD"
+ test "VALID_UNDER_HYP + INVALID_BUT_DEAD"
(set valid_under_hyp invalid_but_dead);
test "VALID_UNDER_HYP + VALID_BUT_DEAD" (set valid_under_hyp valid_but_dead);
- test "VALID_UNDER_HYP + UNKNOWN_BUT_DEAD"
+ test "VALID_UNDER_HYP + UNKNOWN_BUT_DEAD"
(set valid_under_hyp unknown_but_dead);
test "VALID_UNDER_HYP + INCONSISTENT" (set valid_under_hyp inconsistent);
(***************************************************************************)
@@ -172,24 +172,24 @@ let main () =
test "INVALID + UNKNOWN_BUT_DEAD" (set invalid unknown_but_dead);
test "INVALID + INCONSISTENT" (set invalid inconsistent);
(***************************************************************************)
- test "INVALID_UNDER_HYP + INVALID_UNDER_HYP"
+ test "INVALID_UNDER_HYP + INVALID_UNDER_HYP"
(set invalid_under_hyp invalid_under_hyp);
- test "INVALID_UNDER_HYP + INVALID_BUT_DEAD"
+ test "INVALID_UNDER_HYP + INVALID_BUT_DEAD"
(set invalid_under_hyp invalid_but_dead);
- test "INVALID_UNDER_HYP + VALID_BUT_DEAD"
+ test "INVALID_UNDER_HYP + VALID_BUT_DEAD"
(set invalid_under_hyp valid_but_dead);
test "INVALID_UNDER_HYP + UNKNOWN_BUT_DEAD"
(set invalid_under_hyp unknown_but_dead);
- test "INVALID_UNDER_HYP + INCONSISTENT"
+ test "INVALID_UNDER_HYP + INCONSISTENT"
(set invalid_under_hyp inconsistent);
(***************************************************************************)
- test "INVALID_BUT_DEAD + INVALID_BUT_DEAD"
+ test "INVALID_BUT_DEAD + INVALID_BUT_DEAD"
(set invalid_but_dead invalid_but_dead);
- test "INVALID_BUT_DEAD + VALID_BUT_DEAD"
+ test "INVALID_BUT_DEAD + VALID_BUT_DEAD"
(set invalid_but_dead valid_but_dead);
test "INVALID_BUT_DEAD + UNKNOWN_BUT_DEAD"
(set invalid_but_dead unknown_but_dead);
- test "INVALID_BUT_DEAD + INCONSISTENT"
+ test "INVALID_BUT_DEAD + INCONSISTENT"
(set invalid_but_dead inconsistent);
(***************************************************************************)
test "VALID_BUT_DEAD + VALID_BUT_DEAD" (set valid_but_dead valid_but_dead);
@@ -204,4 +204,3 @@ let main () =
test "INCONSISTENT + INCONSISTENT" (set inconsistent inconsistent)
let () = Db.Main.extend main
-
diff --git a/tests/misc/my_visitor.ml b/tests/misc/my_visitor.ml
index 4afb3e92f0862a5bc4e3b28f8b1023022a933cb6..250f4fead95f446e45aee9828a6e8dc9caba91c1 100644
--- a/tests/misc/my_visitor.ml
+++ b/tests/misc/my_visitor.ml
@@ -76,7 +76,7 @@ let main () =
print ();
Kernel.SafeArrays.set false;
Project.clear
- ~selection:(State_selection.Static.with_dependencies S.self) ();
+ ~selection:(State_selection.with_dependencies S.self) ();
(* The AST with 1/2 asserts *)
print ()
end