Bug 448 - Crash when generating trace
Summary: Crash when generating trace
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.6
Hardware: Macintosh Mac OS
: P2 critical
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2008-10-26 17:26 CET by Christopher A. Stone
Modified: 2008-11-13 15:53 CET (History)
0 users

See Also:
Architecture:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Christopher A. Stone 2008-10-26 17:26:13 CET
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;
Comment 1 Alexandre David 2008-10-27 15:23:55 CET
Is it a crash (segfault) or a thrown exception?
Comment 2 Christopher A. Stone 2008-10-27 15:40:15 CET
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
Comment 3 Alexandre David 2008-10-27 16:33:05 CET
Revision 4054 fixed the reason of the exception but the exception crash on MacOS is still not fixed.
Comment 4 Alexandre David 2008-11-13 15:53:49 CET
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.