diff options
| -rw-r--r-- | toplevel/obligations.ml | 29 |
1 files changed, 16 insertions, 13 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 00ea2ffb84..665926922f 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -463,19 +463,6 @@ let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m) let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] -let map_cardinal m = - let i = ref 0 in - ProgMap.iter (fun _ _ -> incr i) m; - !i - -exception Found of program_info - -let map_first m = - try - ProgMap.iter (fun _ v -> raise (Found v)) m; - assert(false) - with Found x -> x - let from_prg : program_info ProgMap.t ref = Summary.ref ProgMap.empty ~name:"program-tcc-table" @@ -680,6 +667,22 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls prg_hook = hook; prg_opaque = opaque; } +let map_cardinal m = + let i = ref 0 in + ProgMap.iter (fun _ v -> + if snd (Ephemeron.get v).prg_obligations > 0 then incr i) m; + !i + +exception Found of program_info + +let map_first m = + try + ProgMap.iter (fun _ v -> + if snd (Ephemeron.get v).prg_obligations > 0 then + raise (Found v)) m; + assert(false) + with Found x -> x + let get_prog name = let prg_infos = !from_prg in match name with |