This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 71

Summary: Engine crash because of missing range check
Product: UPPAAL Reporter: Ulrik Nyman <ulrik>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: CLOSED FIXED    
Severity: major    
Priority: P1    
Version: 3.4.2   
Hardware: All   
OS: All   
URL: http://www.cs.auc.dk/~ulrikl/uppaal/invalidchanrange.xml
Architecture:

Description Ulrik Nyman 2003-12-04 09:16:18 CET 
If one declares an array of channels and uses these as arguments for
instantiating process templates the engine crashes if this is out of range. The
link above has a very simple model that demonstrates the problem. The model can
be sytax checked without errors but when one tries to enter the simulator or
verifier or when opening the model (perhaps when building the location vector?)
the server crashes.
 
Global declarations:
  const N 1;
  chan c[N];
Process assignments:
  P1 := P(c[0]);
  P2 := P(c[1]);
System definition:
  system P1, P2;
Comment 1 Gerd Behrmann 2003-12-05 23:02:04 CET 
Problem confirmed. I could not reproduce the crash on Linux, but the parser
should create an error message in this case (which it doesn't at the moment).
Comment 2 Gerd Behrmann 2003-12-09 14:56:03 CET 
Turns out that the problem is not caused by the use of the array arguments on
template channel parameters. 

The problem is that Transition::getSync() is used without catching the
CannotEvaluateExpression exception which might be thrown as a consequence of
evaluating the synchronisation expression. This will happen in the situation
described in the bug report, but can be trigered in a number of different ways
(e.g. doing something like c[i >> j] for j==-1 directly on the edge would also
crash the engine). I will work on a fix for this problem.

Unfortunately, we cannot give an error message in the editor for this problem.
This requires static range checking in the parser, which we cannot do at the
moment. The command line tool will print warnings for these problems during
verification.
Comment 3 Gerd Behrmann 2003-12-09 15:46:28 CET 
A fix has been checked into CVS. As mentioned above, we cannot at the moment
produce a range check error during syntax checking. For the example linked to in
the URL field, the 'failing' edge (the one which causes the out-of-bounds error)
is simply disabled. This is consistent with how similar problems with guards and
assignments are handled. The command line tools will issue a warning.