diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-09-21 13:58:45 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-09-21 17:01:18 +0200 |
| commit | 0e4186b8f4597801cbd18278d139edbd930bb3ec (patch) | |
| tree | 0df7f6620dd1aa5e494b3cfd897d9caded8b54e6 /lib | |
| parent | 8389b8b73dde919de4f242b022a03c0ddaf44658 (diff) | |
| download | compcert-kvx-0e4186b8f4597801cbd18278d139edbd930bb3ec.tar.gz compcert-kvx-0e4186b8f4597801cbd18278d139edbd930bb3ec.zip | |
fix issue 210 in simu_check
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Impure/ocaml/ImpHConsOracles.ml | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/lib/Impure/ocaml/ImpHConsOracles.ml b/lib/Impure/ocaml/ImpHConsOracles.ml index 2b66899b..68a33a91 100644 --- a/lib/Impure/ocaml/ImpHConsOracles.ml +++ b/lib/Impure/ocaml/ImpHConsOracles.ml @@ -38,12 +38,18 @@ let xhCons (type a) (hp:a hashP) = let t = MyHashtbl.create 1000 in let logs = ref [] in { - hC = (fun (k:a hashinfo) -> + hC = (fun (k:a hashinfo) -> + (* DEBUG: + Printf.printf "*in %d -- look for hcodes= " (Obj.magic t); + List.iter (fun i -> Printf.printf "%d " i) k.hcodes; + print_newline(); + *) match MyHashtbl.find_opt t k with | Some d -> d - | None -> (*print_string "+";*) - let d = hp.set_hid k.hdata (MyHashtbl.length t) in - MyHashtbl.add t {k with hdata = d } d; d); + | None -> + (* DEBUG: Printf.printf "*in %d -- new hid:%d" (Obj.magic t) (MyHashtbl.length t); print_newline(); *) + let d = hp.set_hid k.hdata (MyHashtbl.length t) in + MyHashtbl.add t {k with hdata = d } d; d); next_log = (fun info -> logs := (MyHashtbl.length t, info)::(!logs)); next_hid = (fun () -> MyHashtbl.length t); remove = (fun (x:a hashinfo) -> MyHashtbl.remove t x); |