search

viperproject / silver

Definition of the Viper intermediate verification language.
Mozilla Public License 2.0
78 stars 43 forks source link

Add information required for LSP features to Parse AST #764

Closed JonasAlaif closed 8 months ago

JonasAlaif commented 9 months ago

There are still some failing tests

marcoeilers commented 9 months ago

I really feel like the code is mixing things that should not be mixed. IMO most of the lsp package should not be in Silver, and the ParseAST should not extend LSP-related classes or traits. Couldn't you define the connection between the ParseAST classes and the LSP classes separately? Or, if that would be a problem for plugins or extensions or something like that: Can't we define a couple of classes that provide general, high-level semantic information about PAST nodes, which plugins or extensions could then also use, and which one could then translate into LST concepts?

JonasAlaif commented 8 months ago

Alright @marcoeilers this is pretty much final and ready to be merged (will require some small changes of tests in the silicon repo)

JonasAlaif commented 8 months ago

@marcoeilers baring any bugs this is now final

JonasAlaif commented 8 months ago

I really don't understand why the carbon tests are failing though...

[info] - all/issues/silver/0165.vpr [carbon-Silver] *** FAILED *** (2 milliseconds)
[info]   2 errors
[info]   
[info]   The following output occurred during testing, but should not have according to the test annotations:
[info]     [parser.error] Parse error: Expected (annotation | fail | StringIn("import", "define", "field", "method", "domain", "function", "predicate") | adtDecl):4:21, found "b () { }". Occurred while parsing: annotated:4:21 (0165.vpr@5.21)
[info]   
[info]   The following outputs were expected according to the test annotations, but did not occur during testing:
[info]     parser.error (0165.vpr:5) (AnnotationBasedTestSuite.scala:63)
[info]   + Verifier used: carbon 1.0. 
[info]   + Time required: 1 msec (Parsing), 0 msec (Semantic Analysis), 0 msec (Translation), 0 msec (Consistency Check), 0 msec (Verification).

Like expected parser.error (0165.vpr:5) and got [parser.error] ... (0165.vpr@5.21) why do these two no longer match...?

marcoeilers commented 8 months ago

The problem seems to be that the reported error has a FilePosition but the code (isSameLine in SilOutput) that compares positions expects a SourcePosition.