source not set for sub-expressions of array subscript expressions

[Stephen Siegel]

If you take the following model simpleArray3.mmp:

int[2][3] a;

void main() {
  a[2][1] = 7;
}

when you verify, it correctly throws an array out of bounds exception for the expression "a[2]". However the source information associated to the expression "a[2]" is null.

Verifying simpleArray3...
               model : simpleArray3 (numProcs = 1)
          sourceFile : examples/simpleArray/simpleArray3.mmp
                mode : VERIFY
              prover : CVC3
            deadlock : ABSOLUTE
           reduction : STANDARD
            simplify : false
             verbose : true
         loop method : false
          repository : examples/simpleArray/TASSREP

Creating dynamic factory 0
Pushed initial state onto stack simpleArray3:

begin State 0
  onStack = true;
  seen = true;
  pathCondition : true
  begin model state
    begin shared variables
    end shared variables;
    begin process 0
      begin global variables
        a = m0v0 (int[2][3]);
      end global variables;
      begin stack frame 0
        function : main;
        location : 0;
      end stack frame 0;
    end process 0;
  end model state
end State 0

Predicate does not hold at current state of simpleArray3.
edu.udel.cis.vsl.minimp.util.ExecutionException: Execution error encountered at null
Possible array out of bounds error:
  array expression = a
  index expression = 2
       index value = 2
      array extent = 2
             query = false
    path condition = true
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.arrayElementReferenceValue(Evaluator.java:173)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.referenceValue(Evaluator.java:223)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.arrayElementReferenceValue(Evaluator.java:159)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.referenceValue(Evaluator.java:223)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.assignValue(Executor.java:236)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.executeAssignment(Executor.java:243)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.execute(Executor.java:99)
	at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:74)
	at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.proceedToNewState(DfsSearcher.java:145)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:107)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:93)
	at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:82)
	at simpleArray.SimpleArray3Test.testOutOfBounds(SimpleArray3Test.java:37)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:44)
	at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:15)
	at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:41)
	at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:20)
	at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:28)
	at org.junit.internal.runners.statements.RunAfters.evaluate(RunAfters.java:31)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:73)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:46)
	at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:180)
	at org.junit.runners.ParentRunner.access$000(ParentRunner.java:41)
	at org.junit.runners.ParentRunner$1.evaluate(ParentRunner.java:173)
	at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:28)
	at org.junit.internal.runners.statements.RunAfters.evaluate(RunAfters.java:31)
	at org.junit.runners.ParentRunner.run(ParentRunner.java:220)
	at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:46)
	at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:467)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:683)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:390)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:197)
edu.udel.cis.vsl.minimp.util.ExecutionException: Execution error encountered at null
Possible array out of bounds error:
  array expression = a
  index expression = 2
       index value = 2
      array extent = 2
             query = false
    path condition = true
No deadlock possible at this state.
Writing counterexample to simpleArray3.trace...done.
Writing model to simpleArray3.model...done.
STATS:
   statesSeen    : 1
   statesMatched : 0
   statesSaved   : 1
   transitions   : 0
   time          : 0.097s.

RESULT: Some safety properties MAY NOT hold: counterexample found.

Destroying dynamic factory 0

[ywei]

Fixed. The sub-expressions of an array subscript expression now have source information properly set.