Home My Page Projects Why3
Summary Activity Tracker Lists SCM Files

[#14221] sessions: filename incorrectly interpreted on windows

2012-05-03 14:06
Submitted by:
Johannes Kanig (kanig)
Assigned to:
Claude Marché (marche)
Operating System:
Windows NT
sessions: filename incorrectly interpreted on windows

Detailed description
I am hunting down a problem with spaces in directory names on windows (more on that in another bug report probably), and I came across the following issue. I have a directory called "natural", in which I have a Why3ML file f.mlw. Running our tool gnatwhy3 the first time is fine (except for my problem with spaces), but when it is run the second time (and hence reads the session file in), it does not manage to find the Why3ML file. The reason seems to be that the file name has been stored in the session.xml as


and the '\n' is interpreted as a newline by somebody (Why3? the xml library?).

I suggest one of the two solutions should be applied:

1) encode the filename in the XML file, e.g. by doubling the '\'
2) not interpret '\' as escaping character in the XML

It's difficult to provide a reproducer, because right now the only binary on windows that I have that generates session files is gnatwhy3 (our tool using the Why3 library). I have not tried yet to install Gtk and the like to have why3ide ...

gnatwhy3 only uses the API to deal with session files, such as create_session, read_session, save_session from the Session module.

Let me know if you need more information.

Message  ↓
Date: 2012-05-11 12:45
Sender: Johannes Kanig

Yes, the problem went away. The ticket can be closed.


Date: 2012-05-11 11:23
Sender: Claude Marché

I made a few modification related to this problem. These are available in the current git.
Johannes, could you check that you don't have this problem anymore ?

Date: 2012-05-10 16:02
Sender: Johannes Kanig

Thank you for your answer.

It seems that your points 2) and 3) are contradictory, is the XML supposed to be compliant or not, and if it is, how can '\' still be interpreted as escape character?

When I tried out latest Why3 sources (which I did not previously), the error was different actually, it said "Lexing: empty token", which made me aware of the fact that the function "string_val" in xml.mll is not complete, it does not cover the character '\' on its own.

So I simply removed '\' from the last pattern, said otherwise, I did the following:

- | [^ '\\' '"'] as c
+ | [^ '"'] as c

and this seems to fix the problem we have on our side, the paths are parsed correctly now.

Is this solution not enough in the general case?

Thanks for your help,


Date: 2012-05-04 15:56
Sender: Claude Marché

Three remarks:

1) the file names stored in the session should always be relative, so it seems
the "relativization" does not work with backslashes, so a first bug to fix

2) Indeed, the current implementation of XML output and input in Why3 is not fully
conformant to XML standard, because \ is interpreted as an escape char as it is
e.g. in Ocaml. However, there is another bug here since the \ in file names should have been escaped

3) Finally, the current git of Why3 aims at producing fully compliant XML files,
that is where characters like quote (") are wriitten as ", in other words
where the escape char is '&' and not '\'. the interpretation of '\' is still present to preserve compatibility.

Field Old Value Date By
status_idOpen2012-05-11 13:34marche
close_dateNone2012-05-11 13:34marche
ResolutionAccepted As Bug2012-05-11 13:34marche
assigned_tonone2012-05-04 15:56marche
ResolutionNone2012-05-04 15:56marche