mbeddr/mbeddr.formal

Errors in Spin Module

BentleyJOakes opened this issue · 1 comments

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.

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 ...