Escape string attributes in session files (!15) · Merge requests · Why3 / why3

When a goal contains characters such as & or <, the session file becomes corrupted and cannot be opened any more. For example here:

Module Test
  use int.Int
  let function (&) (n: int): int
    ensures { result = n + 1 }
  = n + 1
end

The corruption is due to unescaped characters in the expl attribute of the goal:

<goal name="VC infix &amp;" expl="VC for infix &" proved="true">

This patch escapes string attributes including expl.

Escape string attributes in session files