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

Bug 237 - Missing type check of array index
Summary: Missing type check of array index
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: GUI (show other bugs)
Version: 3.6 Alpha 2
Hardware: PC All
: P1 normal
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2005-12-06 17:00 CET by Paul
Modified: 2005-12-07 14:42 CET (History)
0 users

See Also:
Architecture:


Attachments
Example System (801 bytes, text/xml)
2005-12-07 13:15 CET, Paul
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Paul 2005-12-06 17:00:00 CET
When using a global const and a local variable with the same name, trying to 
read its value in the process (when trying to simulate or model check) only 
leads to a "Server connection lost" error. 
I think it would have cost me not so much time to figure my fault out, if 
there would have been a "better" error reporting (well, I know that it's not a 
syntax error)
Comment 1 Gerd Behrmann 2005-12-07 11:00:24 CET
The behaviour you describe is a server crash due to some internal fault. I have not been able to reproduce 
the error from your description. Could you please attach the model triggering this bug to the bug report 
or email it to me directly. Thanks.
Comment 2 Paul 2005-12-07 13:15:06 CET
Created attachment 81 [details]
Example System

When (incorrectly) using a clock as an index for an array, syntax check is ok,
but using the model leads to "Server connection lost". It's not a bug, but
better error reporting would be great.
(My fault was, i forgot to delete a (local) clock and introduced a global const
with that name, so when i tried to use the const as array index, uppaal tried
to use the clock, which obviously couldn't work)
Comment 3 Gerd Behrmann 2005-12-07 14:17:01 CET
Thanks, I see the problem now. It is most certainly a bug: The "error message" you describe means the 
verification server crashed and that should never ever happen. The fact that the crash was triggered by a 
type error in the input model does not change this. Will be fixed before the release of alpha 3.

It seems that the type of array indices is not checked at all.
Comment 4 Gerd Behrmann 2005-12-07 14:42:34 CET
Fixed on the trunk (revision 1334).