Bug 471 - typechecker does not check ranges of constant expressions
Summary: typechecker does not check ranges of constant expressions
Status: CLOSED DUPLICATE of bug 488
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: libutap (show other bugs)
Version: unspecified
Hardware: All All
: P2 minor
Assignee: Alexandre David
Depends on: 488
  Show dependency treegraph
Reported: 2009-05-22 22:25 CEST by Marius Mikučionis
Modified: 2010-05-25 17:10 CEST (History)
0 users

See Also:


Note You need to log in before you can comment on or make changes to this bug.
Description Marius Mikučionis 2009-05-22 22:25:42 CEST
the constants and ranges should also be range-checked, for example expressions like the following are asking for trouble but accepted:
const int x = 1000000000000000000;
int[0,5000000000000000000000000] x = 1000000000000000000;

(strange how this goes through scanner, does it expect 64bit integers?)

typechecker should also issue errors on meaningless expressions like "x=-1" where x is a clock and "-1" is arbitrary constant expression evaluating to negative value. Currently this is not checked and shows up only during simulation/verification.

typechecker could also issue a warning if the estimated range of non-const expression contains negative values in the clock assignment -- that would encourage better style of declaring explicit ranges, but may become annoyance, so this is debatable.
Comment 1 Marius Mikučionis 2010-04-30 19:44:30 CEST
now I've found a case where range checker is too restrictive when dealing with clocks:

typedef int[0, 10000000] time_t;
const int MULT = 4;
const int CYCLE = 250*1000/MULT;
const int CYCLELIMIT = 12*MULT;

time_t counter=1;
clock global;

then put expression "global<=counter*CYCLE" into invariant or guard.
For MULT=4 Uppaal says "clock constraint is out of range", but it is fine with MULT=1 or MULT=2.
Comment 2 Marius Mikučionis 2010-04-30 20:06:14 CEST
please ignore my last comment: my fault, the issue can be fixed by the following declaration:
int[0, CYCLELIMIT] counter=1;
Comment 3 Marius Mikučionis 2010-05-25 17:06:03 CEST
the fix for this bug seems to depend on the fix for bug 488.

*** This bug has been marked as a duplicate of bug 488 ***
Comment 4 Alexandre David 2010-05-25 17:10:44 CEST
Actually it's not a duplicate of bug 488.
It's similar but not the same. The lexer was
not able to recognize INT_MIN due to overflow
on positive integers even though it should have
done it. This comes from the rule (unary not) natural.
There's a special case for that now. The real
overflow issue has been fixed in the same revision
but it's a different fix.