Bug 71 - Engine crash because of missing range check
Summary: Engine crash because of missing range check
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.4.2
Hardware: All All
: P1 major
Assignee: Gerd Behrmann
URL: http://www.cs.auc.dk/~ulrikl/uppaal/i...
Depends on:
Reported: 2003-12-04 09:16 CET by Ulrik Nyman
Modified: 2004-03-15 07:43 CET (History)
0 users

See Also:


Note You need to log in before you can comment on or make changes to this bug.
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
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.