aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Regalloc.ml
diff options
context:
space:
mode:
authorMichael Schmidt <github@mschmidt.me>2018-06-04 14:47:16 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2018-08-02 10:29:44 +0200
commitd13f1e243ff5ac94ecfc64f2bd81ae5d1c33bfcc (patch)
treee01d30310ccddee46fb854f7dc69e001447b91f6 /backend/Regalloc.ml
parenta2064197c9dc5578e6f0155b8d0cc9cb3eecef90 (diff)
downloadcompcert-kvx-d13f1e243ff5ac94ecfc64f2bd81ae5d1c33bfcc.tar.gz
compcert-kvx-d13f1e243ff5ac94ecfc64f2bd81ae5d1c33bfcc.zip
Various improvements in the wording of diagnostics.
Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
Diffstat (limited to 'backend/Regalloc.ml')
-rw-r--r--backend/Regalloc.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index d4d7362d..19aba4f6 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -644,7 +644,7 @@ let add_interfs_instr g instr live =
(* Reloads from incoming slots can occur when some 64-bit
parameters are split and passed as two 32-bit stack locations. *)
begin match src with
- | L(Locations.S(Incoming, _, _)) ->
+ | L(Locations.S(Incoming, _, _)) ->
add_interfs_def g (vmreg temp_for_parent_frame) live
| _ -> ()
end
@@ -1210,9 +1210,9 @@ let regalloc f =
Errors.OK(first_round f3 liveness)
with
| Timeout ->
- Errors.Error(Errors.msg (coqstring_of_camlstring "Spilling fails to converge"))
+ Errors.Error(Errors.msg (coqstring_of_camlstring "spilling fails to converge"))
| Type_error_at pc ->
- Errors.Error [Errors.MSG(coqstring_of_camlstring "Ill-typed XTL code at PC ");
+ Errors.Error [Errors.MSG(coqstring_of_camlstring "ill-typed XTL code at PC ");
Errors.POS pc]
| Bad_LTL ->
- Errors.Error(Errors.msg (coqstring_of_camlstring "Bad LTL after spilling"))
+ Errors.Error(Errors.msg (coqstring_of_camlstring "bad LTL after spilling"))