diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml index 5c8a0efd9a921436990a0dc1a769b588d4d391f7..055cedeea1a352bad1fae4b51ee301bf9ce99943 100644 --- a/src/plugins/inout/operational_inputs.ml +++ b/src/plugins/inout/operational_inputs.ml @@ -207,13 +207,16 @@ module Internals = let size = 17 end) -module CallsiteHash = Value_types.Callsite.Hashtbl +module Callsite = + Datatype.Pair_with_collections (Kernel_function) (Cil_datatype.Kinstr) + (struct let module_name = "From.Callsite" end) +module CallsiteHash = Callsite.Hashtbl (* Results of an an entire call, represented by a pair (stmt, kernel_function). *) module CallwiseResults = State_builder.Hashtbl - (Value_types.Callsite.Hashtbl) + (Callsite.Hashtbl) (Inout_type) (struct let size = 17