Fix passing of warnings

[wadoon]

No warning was shown if a name collision happens in the signature of a problem. Program variables take preceding on the evaluation. The check was present in the code, but the generated warning did not bubble up to the ProblemInitializer.

For example, consider following input file:

\functions        { int f; }
\programVariables { int f; }
\problem          { f = f  }

that loading ends up into a warning message now:

[codecov]

Codecov Report

Attention: 14 lines in your changes are missing coverage. Please review.

Comparison is base (c430e35) 37.98% compared to head (44087c2) 37.98%.
Report is 19 commits behind head on main.

Files	Patch %	Lines
...va/de/uka/ilkd/key/util/parsing/BuildingIssue.java	25.00%	7 Missing and 2 partials ⚠️
.../key/nparser/builder/FunctionPredicateBuilder.java	62.50%	2 Missing and 1 partial ⚠️
...e/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java	83.33%	1 Missing ⚠️
...rc/main/java/de/uka/ilkd/key/proof/io/KeYFile.java	85.71%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3302      +/-   ##
============================================
- Coverage     37.98%   37.98%   -0.01%     
+ Complexity    17024    17019       -5     
============================================
  Files          2059     2059              
  Lines        126029   126045      +16     
  Branches      21282    21283       +1     
============================================
+ Hits          47874    47875       +1     
- Misses        72272    72284      +12     
- Partials       5883     5886       +3     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[FliegendeWurst]

Why does the example

\functions        { int f; }
\programVariables { int f; }
\problem          { f = f  }

generate >9 warnings? I would expect at most 4.

[wadoon]

Why does the example

\functions        { int f; }
\programVariables { int f; }
\problem          { f = f  }

generate >9 warnings? I would expect at most 4.

The line is produced here:

https://github.com/KeYProject/key/blob/c9ba634a4e03e44abc8b5703570f17bf03fa9978/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java#L160C1-L160C1

I guess we declare the sort multiple times.

[unp1]

Hi,

I get an NPE with the example:

IssueDialog - Failed to update previewjava.lang.NullPointerException: Cannot invoke "String.endsWith(String)" because "fileName" is null at de.uka.ilkd.key.gui.IssueDialog.isJava(IssueDialog.java:732) at de.uka.ilkd.key.gui.IssueDialog.updatePreview(IssueDialog.java:670) at de.uka.ilkd.key.gui.IssueDialog.lambda$createWarningsPane$4(IssueDialog.java:325)

Best regards,
Richard

[unp1]

Why does the example

\functions        { int f; }
\programVariables { int f; }
\problem          { f = f  }

generate >9 warnings? I would expect at most 4.

The line is produced here:

https://github.com/KeYProject/key/blob/c9ba634a4e03e44abc8b5703570f17bf03fa9978/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java#L160C1-L160C1

I guess we declare the sort multiple times.

The problem is that generic sorts of the same name are declared several times.

I think we should do something about it as otherwise one could rely on '\generic G extends X' but has actually '\generic G extends Y;' or '\generic G;' which would introduce subtle soundness problems.

This means we should either use a different name in each file or limit the scope of generic sorts to the file itself.

[wadoon]

@unp1 Maybe we should solve this at a larger scale. We had sometimes the discussion for theory support in KeY. I copied my old notes but I need to sort them, then we would have local namespace by default.

[github-actions]

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

[unp1]

@unp1 Maybe we should solve this at a larger scale. We had sometimes the discussion for theory support in KeY. I copied my old notes but I need to sort them, then we would have local namespace by default.

Thanks. I agree that we should introduce proper theories with local namespaces.

[wadoon]

@unp1 @mattulbrich
Should we just disable the warning for sorts for now (It had no impact earlier.), so this PR can fly into main?

[unp1]

@unp1 @mattulbrich Should we just disable the warning for sorts for now (It had no impact earlier.), so this PR can fly into main?

Hi, yes I would say so. Otherwise can one just not collect the warnings in the parser for sorts with the generic modifier, for now?

But I am also fine with not showing warnings for sorts for the moment.

[mattulbrich]

After discussion in KeY meeting: Program variable and function of same name should not only be a warning but an actual error.

[wadoon]

@unp1 @mattulbrich The discussion of the KaKeY meeting is implemented. Error on shadowing of functions, and no warning on sort duplication. Both places are commented in the source code.

[unp1]

Thanks. The code changes look good. I assume the failing tests is because of the stricter check for duplicate function names and we need to fix our test suite?

[wadoon]

Thanks. The code changes look good. I assume the failing tests is because of the stricter check for duplicate function names and we need to fix our test suite?

Surprisingly yes,

Function 'head' is already defined! at <unknown>:3:3 (<unknown>:3:3)

in TestTermParser.

[unp1]

@wadoon @mattulbrich:
Should we also consider duplicate predicates as errors? At the moment that is not considered to be an error, e.g., geq in the example below:

// Input file for KeY standalone prover version 0.497
\sorts {
s;
}

\predicates {
p;
q;
geq(int,int);
}

\problem {
((p -> q) -> !q -> !p) & geq(0,1)

}
contraposition.key.zip

[mattulbrich]

@wadoon @mattulbrich: Should we also consider duplicate predicates as errors? At the moment that is not considered to be an error, e.g., geq in the example below:

// Input file for KeY standalone prover version 0.497 \sorts { s; }

\predicates { p; q; geq(int,int); }

\problem { ((p -> q) -> !q -> !p) & geq(0,1)

} contraposition.key.zip

I too would say that function and predicate symbols are to be treated equally here.

[unp1]

The PR seems to be ready to go now and I approved it. @wadoon: I did not click on "Merge when ready" in case you have some commits pending. Thanks a lot!