diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cEphemeron.ml | 4 | ||||
| -rw-r--r-- | lib/cEphemeron.mli | 2 | ||||
| -rw-r--r-- | lib/cErrors.ml | 2 | ||||
| -rw-r--r-- | lib/flags.ml | 1 | ||||
| -rw-r--r-- | lib/flags.mli | 4 | ||||
| -rw-r--r-- | lib/future.ml | 6 | ||||
| -rw-r--r-- | lib/genarg.ml | 6 | ||||
| -rw-r--r-- | lib/remoteCounter.ml | 4 | ||||
| -rw-r--r-- | lib/spawn.ml | 4 |
9 files changed, 16 insertions, 17 deletions
diff --git a/lib/cEphemeron.ml b/lib/cEphemeron.ml index a38ea11e10..890e02dc4e 100644 --- a/lib/cEphemeron.ml +++ b/lib/cEphemeron.ml @@ -35,10 +35,10 @@ end) would make the key always reachable) *) let values : Obj.t HT.t = HT.create 1001 -(* To avoid a race contidion between the finalization function and +(* To avoid a race condition between the finalization function and get/create on the values hashtable, the finalization function just enqueues in an imperative list the item to be collected. Being the list - imperative, even if the Gc enqueue an item while run_collection is operating, + imperative, even if the Gc enqueues an item while run_collection is operating, the tail of the list is eventually set to Empty on completion. Kudos to the authors of Why3 that came up with this solution for their implementation of weak hash tables! *) diff --git a/lib/cEphemeron.mli b/lib/cEphemeron.mli index 1200e4e208..76cd7a5a8a 100644 --- a/lib/cEphemeron.mli +++ b/lib/cEphemeron.mli @@ -26,7 +26,7 @@ Proposed solution: Turn all occurrences of [bad] into [bad key] in your data structure. - Use [crate bad_val] to obtain a unique key [k] for [bad_val], and store + Use [create bad_val] to obtain a unique key [k] for [bad_val], and store [k] in the data structure. Use [get k] to obtain [bad_val]. An ['a key] can always be marshalled. When marshalled, a key loses its diff --git a/lib/cErrors.ml b/lib/cErrors.ml index b0e77a4c90..8ef11a2cdd 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -77,7 +77,7 @@ let where = function if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt () let raw_anomaly e = match e with - | Anomaly (s, pps) -> where s ++ pps ++ str "." + | Anomaly (s, pps) -> where s ++ pps | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "." | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." diff --git a/lib/flags.ml b/lib/flags.ml index b2671e5b60..6a3b7a4261 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -87,7 +87,6 @@ let in_toplevel = ref false let profile = false -let print_emacs = ref false let xml_export = ref false let ide_slave = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 7ce808041a..e2cf09474e 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -13,7 +13,9 @@ val boot : bool ref val load_init : bool ref +(* Will affect STM caching *) val batch_mode : bool ref + type compilation_mode = BuildVo | BuildVio | Vio2Vo val compilation_mode : compilation_mode ref val compilation_output_name : string option ref @@ -56,8 +58,6 @@ val profile : bool (* Legacy flags *) -(* -emacs option: printing includes emacs tags, will affect stm caching. *) -val print_emacs : bool ref (* -xml option: xml hooks will be called *) val xml_export : bool ref diff --git a/lib/future.ml b/lib/future.ml index 1360b7ac4a..8bef1e58e1 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -157,7 +157,7 @@ let chain ~pure ck f = | Val (v, None) -> match !ck with | Finished _ -> CErrors.anomaly(Pp.str - "Future.chain ~pure:false call on an already joined computation") + "Future.chain ~pure:false call on an already joined computation.") | Ongoing _ -> CErrors.anomaly(Pp.strbrk( "Future.chain ~pure:false call on a pure computation. "^ "This can happen if the computation was initial created with "^ @@ -171,7 +171,7 @@ let replace kx y = match !x with | Exn _ -> x := Closure (fun () -> force ~pure:false y) | _ -> CErrors.anomaly - (Pp.str "A computation can be replaced only if is_exn holds") + (Pp.str "A computation can be replaced only if is_exn holds.") let purify f x = let state = !freeze () in @@ -213,7 +213,7 @@ let map2 f x l = let xi = chain ~pure:true x (fun x -> try List.nth x i with Failure _ | Invalid_argument _ -> - CErrors.anomaly (Pp.str "Future.map2 length mismatch")) in + CErrors.anomaly (Pp.str "Future.map2 length mismatch.")) in f xi y) 0 l let print f kx = diff --git a/lib/genarg.ml b/lib/genarg.ml index 05c828d5f9..377ff81827 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -159,7 +159,7 @@ let create_arg name = match ArgT.name name with | None -> ExtraArg (ArgT.create name) | Some _ -> - CErrors.anomaly (str "generic argument already declared: " ++ str name) + CErrors.anomaly (str "generic argument already declared: " ++ str name ++ str ".") let make0 = create_arg @@ -180,7 +180,7 @@ struct let register0 arg f = match arg with | ExtraArg s -> if GenMap.mem s !arg0_map then - let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in + let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in CErrors.anomaly msg else arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map @@ -192,7 +192,7 @@ struct with Not_found -> match M.default (ExtraArg name) with | None -> - CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name)) + CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name) ++ str ".") | Some obj -> obj (** For now, the following function is quite dummy and should only be applied diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index e7646fb796..11f151a609 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -25,7 +25,7 @@ let new_counter ~name a ~incr ~build = (* - in the main process there is a race condition between slave managers (that are threads) and the main thread, hence the mutex *) if Flags.async_proofs_is_worker () then - CErrors.anomaly(Pp.str"Slave processes must install remote counters"); + CErrors.anomaly(Pp.str"Slave processes must install remote counters."); Mutex.lock m; let x = f () in Mutex.unlock m; build x in let mk_thsafe_remote_getter f () = @@ -33,7 +33,7 @@ let new_counter ~name a ~incr ~build = let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in let installer f = if not (Flags.async_proofs_is_worker ()) then - CErrors.anomaly(Pp.str"Only slave processes can install a remote counter"); + CErrors.anomaly(Pp.str"Only slave processes can install a remote counter."); getter := mk_thsafe_remote_getter f in (fun () -> !getter ()), installer diff --git a/lib/spawn.ml b/lib/spawn.ml index 4791769735..4d7e78d861 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -200,7 +200,7 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) p, cout let stats { oob_req; oob_resp; alive } = - assert_ alive "This process is dead"; + assert_ alive "This process is dead."; output_value oob_req ReqStats; flush oob_req; input_value oob_resp @@ -251,7 +251,7 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) = with e -> prerr_endline ("kill: "^Printexc.to_string e) end let stats { oob_req; oob_resp; alive } = - assert_ alive "This process is dead"; + assert_ alive "This process is dead."; output_value oob_req ReqStats; flush oob_req; let RespStats g = input_value oob_resp in g |