-
Notifications
You must be signed in to change notification settings - Fork 25
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Incorrect Debug Exception Highlighting with Multiple Files of the Same Name #721
Comments
Thanks for reporting this. I can confirm that it is reproducible on the latest Overture 2.7.4 (on Linux, but it is unlikely to be a platform issue). It is the same whether launched from the console or a launcher. I'll take a look. But it looks like it's making a naive file lookup at some point. If it's causing a problem, an obvious workaround is to rename the file, though clearly this should work as expected. |
It is behaving correctly in the pure command line - that is, the stand alone Overture jar. This suggests the problem is with the IDE/VDM communication of the stack location.
|
I assumed this would be the case, apologies for not testing direct execution of the jar myself, I could have narrowed down the issue a little more for you. I only came across the issue as I was revising for an exam on VDM, and ended up with 2 different files named I'd love to suggest a solution myself, but I'm completely unfamiliar with the eclipse framework, and only know the very basics of Java File IO. |
I always test the stand-alone jar first, so I know whether it's the language engine or the IDE. If it's the language side, I'll know how to fix it :-) It definitely looks like the IDE though, because the comms between the IDE and language engine includes the qualified file information:
So now I need to find someone who understands the IDE... :-( |
Thanks Hugo! |
I think there may be a problem with this fix. I'm trying to do some "serious" debugging on the FMI spec, rather than the test example above. When it stops at a breakpoint and trying to open the source file concerned, it uses a bizarre paths like:
I'll re-open this issue, as it looks like this is linked to the fix above? |
(and those paths are not found, incidentally. So you get a blank editor pane with an invite to "Edit Source Path Lookup") |
Easiest way to reproduce this is to load the FMI2 model (https://github.com/INTO-CPS-Association/FMI-VDM-Model/tree/master/FMI2), and put a breakpoint on the start of the tests() function at the end of Tests.vdmsl:
Then just run DEFAULT'tests(). You'll see it stop on the line, but the file is reported (in my case) as ../../INTO-CPS-Association/FMI-VDM-Model/FMI2/Tests/Tests.vdmsl. This file is not found. |
Description
When an exception occurs, Overture attempts to highlight the line which the exception occurred on, however when a project contains multiple files with the same name in different directories, Overture displays the file in the first directory (alphabetically), and not the correct file.
Steps to Reproduce
dir1/
anddir2/
.dir1/type.vdmsl
anddir2/type.vdmsl
.dir1/type.vdmsl
.dir2/vdmsl
.Expected behavior: The debugger highlights the erroneous line in the file where the exception occurred.
Actual behavior: The debugger highlights the corresponding line in the first file it finds, matching the name of the erroneous file.
Reproduces how often: Always
Versions
Overture 2.7.2 Windows 10 x64
Additional Information
The issue was found when running the project as a console.
The exception chosen is one which occurs at runtime (
Error 4: Cannot get bind values for type nat in 'DEFAULT'
), although this is irrelavent for this bug.The text was updated successfully, but these errors were encountered: