Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ASCII NUL in path specifications

view this post on Zulip Email Gateway (Aug 22 2022 at 18:49):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi,

paths in Isabelle/ML, as observed in Isabelle2018, may contain ASCII NUL
characters.

ML_val ‹Path.basic (chr 0)›

That is not valid in POSIX. I'm uncertain whether this issue is critical.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 18:50):

From: Makarius <makarius@sketis.net>
Did this show up in a practical application?

Strings in Isabelle/ML and Isabelle/Scala may contain ASCII NUL, but the
C/C++ world out there usually excludes that.

The ultimate interpretation of Path.T is up to the underlying
file-system: Path.T cannot protect against arbitrary non-sense there.
E.g. I've occasionally seen corner cases with national "code pages" and
arbitrary Unicode file names. It is normal and to be expected that file
names are not 100% reliable.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC