Errors in Spin Module
BentleyJOakes opened this issue · 1 comments
BentleyJOakes commented
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
In the generated Java file:
/* error: statement w/o textGen:safe read action */
Let me know if any other information is required.
danielratiu commented
I think that this is fixed - I could run a local cradle build, on the server it runs as well :-)
Please let me know if it still does not work ...