You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
There are numerous errors in com.mbeddr.formal.spin, preventing its building from the Gradle file.
Edit: Building the module within MPS directly produces the two errors in SpinCexTableModel.
[generate] 22 errors during generation:
[generate] Compilation problems
[generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 38)
[generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 41)
[generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 43)
[generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 45)
[generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 52)
[generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileFullyQualifiedName may not have been initialized (line: 60)
[generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileName may not have been initialized (line: 70)
[generate] com/mbeddr/formal/spin/runner/SpinRunner.java : The local variable panFileName may not have been initialized (line: 78)
[generate] Compilation problems
[generate] com/mbeddr/formal/spin/ui/SpinCexTableModel.java : The type com.mbeddr.formal.base.tooling.results_model.IWhitnessEntry cannot be resolved. It is indirectly referenced from required .class files (line: 8)
[generate] com/mbeddr/formal/spin/ui/SpinCexTableModel.java : Bound mismatch: The type ISpinWitnessEntry is not a valid substitute for the bounded parameter <T extends IWhitnessEntry> of the type WhitnessTableModelBase<T> (line: 8)
[generate] Compilation problems
[generate] com/mbeddr/formal/spin/analyzer/SpinAssertionsAnalyzer.java : The local variable slr may not have been initialized (line: 39)
[generate] com/mbeddr/formal/spin/analyzer/SpinAssertionsAnalyzer.java : The local variable slr may not have been initialized (line: 40)
[generate] Compilation problems
[generate] com/mbeddr/formal/spin/testing_utils/SpinTestingUtils.java : The local variable aa may not have been initialized (line: 36)
[generate] com/mbeddr/formal/spin/testing_utils/SpinTestingUtils.java : The local variable sba may not have been initialized (line: 47)
These errors may come from a problem with text generation of safe read actions.
For example, in the SpinAssertionsAnalyzer:
safe read action with modelRepository : {
slr = SpinResultLifter.lift(srr, config, modelRepository);
} end action
There are numerous errors in com.mbeddr.formal.spin, preventing its building from the Gradle file.
Edit: Building the module within MPS directly produces the two errors in SpinCexTableModel.
These errors may come from a problem with text generation of safe read actions.
For example, in the
SpinAssertionsAnalyzer
:In the generated Java file:
Let me know if any other information is required.
The text was updated successfully, but these errors were encountered: