| Summary: | Crash when generating trace | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Christopher A. Stone <stone> |
| Component: | Engine | Assignee: | Alexandre David <adavid> |
| Status: | RESOLVED FIXED | ||
| Severity: | critical | ||
| Priority: | P2 | ||
| Version: | 4.0.6 | ||
| Hardware: | Macintosh | ||
| OS: | Mac OS | ||
| Architecture: | |||
Is it a crash (segfault) or a thrown exception? On my x86 mac, I'm getting an exception, followed by a segfault (A<> count >= 2) or a double free warning (A<> false). On other machines (definitely 4.1.0 under linux, possibly 4.0.6 on an older powerpc mac) it just reports the exception and exits. ========= % verifyta -t 0 crash.xta crash1.q Options for the verification: Generating some trace Search order is breadth first Using conservative space optimisation Seed is 1225117830 State space representation uses minimal constraint systems Verifying property 1 at line 4 -- Property is NOT satisfied. -- Aborted. EXCEPTION: Cannot generate the trace zsh: segmentation fault verifyta -t 0 crash.xta crash1.q =============== verifyta -t 0 crash.xta crash2.q Options for the verification: Generating some trace Search order is breadth first Using conservative space optimisation Seed is 1225117954 State space representation uses minimal constraint systems Verifying property 1 at line 1 -- Property is NOT satisfied. -- Aborted. EXCEPTION: Cannot generate the trace verifyta(802) malloc: *** error for object 0x202130: double free *** set a breakpoint in malloc_error_break to debug Revision 4054 fixed the reason of the exception but the exception crash on MacOS is still not fixed. Experiments on MacOS X 10.5 generated the exception without the segfault. It may be related to a specific version of MacOS X. This bug is fixed but if segfaults occur again when exceptions are thrown please open a new bug. |
There appears to be a problem involving (potentially) large integers. The query A<> count >= 2 or even A<> false crashes verifyta on the following system when you ask for a trace (-t 0). If the potential range specified for threshold is significantly smaller, a trace is created with no problems. ============== urgent chan ch; int count = 0; clock clk; process main () { int[-2147483648,2147483647] threshold = 0; state s1, s2, s3; urgent s2, s3; init s1; trans s1 -> s2 {sync ch?; }, s2 -> s3 {guard 1000 - threshold >= clk; }, -> s3 {guard 1000 - threshold < clk; }; } process startup () { state s1; init s1; trans s1 -> s1 {sync ch!; }; } system startup, main;