diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2022-10-31 11:03:13 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-11-05 15:22:31 +0100 |
| commit | e637a49e7a963683a4337b742c0adc0e1f93f139 (patch) | |
| tree | 4e37506a73b3679c61189696c52d6150ae6c4580 | |
| parent | ccfeebf91784ab34f3aacaf495c59667b9ec98b6 (diff) | |
| download | compcert-e637a49e7a963683a4337b742c0adc0e1f93f139.tar.gz compcert-e637a49e7a963683a4337b742c0adc0e1f93f139.zip | |
Replace CR, FF and VT with whitespace.
We use Printlines to copy C code fragments to assembly comments.
While CR, FF and VT are treated like whitespace by C, they could
possibly mess up the assembly comments if copied verbatim.
Moreover, this avoids generating CR CR LF end-of-lines under Windows.
Bug 34075
| -rw-r--r-- | lib/Printlines.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/lib/Printlines.ml b/lib/Printlines.ml index b60fdf4a..b270e229 100644 --- a/lib/Printlines.ml +++ b/lib/Printlines.ml @@ -101,11 +101,13 @@ let copy oc pref b first last = try while b.lineno <= last do let c = input_char b.chan in - output_char oc c; - if c = '\n' then begin + match c with + | '\n' -> + output_char oc c; b.lineno <- b.lineno + 1; if b.lineno <= last then output_string oc pref - end + | '\r' | '\011' | '\012' -> output_char oc ' ' + | _ -> output_char oc c done with End_of_file -> output_char oc '\n' |