overturetool
"Add VDM Run Configuration" gives wrong defaultName
The "Add VDM Run Configuration" menu option builds a launch entry with an incorrectly set defaultName (and the wrong title, though that is harmless). For example:
{
"name": "Launch VDM Debug from f[nat](1,2,3)`DEFAULT",
"type": "vdm",
"request": "launch",
"noDebug": false,
"defaultName": "f[nat](1,2,3)",
"command": "print f[nat](1,2,3)"
}
The "command" is correct, but the defaultName is set to the launch expression and the "name" has the module name and expression the wrong way round. There's a similar problem in VDM++ specs.
Incidentally, the was something my students were experiencing as well: this "name" with the expression was leading to an XDebug print out of the VDM SL file without starting the interpreter.
@leouk That's very strange. I just get the following, when trying to run f: set of bool -> nat, passing {true, false}
Module f({true, false}) not loaded
Init terminated.
Session disconnected.