- let before = Unix.gettimeofday () in
- ignore (CicTypeChecker.typecheck uri);
- let after = Unix.gettimeofday () in
- let diff = after -. before in
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ ignore (Unix.alarm deadline);
+ CicTypeChecker.typecheck_obj uri obj;
+ ignore (Unix.alarm 0);
+ CicEnvironment.remove_obj uri;
+ let before = Unix.times () in
+ ignore (Unix.alarm deadline);
+ ignore (CicTypeChecker.typecheck_obj uri obj);
+ ignore (Unix.alarm 0);
+ let memusage = (Gc.stat ()).Gc.live_words * 4 / 1024 / 1024 in
+ if memusage > 500 then
+ begin
+ prerr_endline ("MEMORIA ALLOCATA: " ^ string_of_int memusage ^ "Mb");
+ CicEnvironment.empty ();
+ Gc.compact ();
+ let memusage = (Gc.stat ()).Gc.live_words * 4 / 1024 / 1024 in
+ prerr_endline ("DOPO CicEnvironment.empty: " ^ string_of_int memusage ^ "Mb");
+ end;
+ let after = Unix.times () in
+ let diff = after.Unix.tms_utime +. after.Unix.tms_stime -. before.Unix.tms_utime -. before.Unix.tms_stime in