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

Bug 165

Summary:	verifyta crashes on non-existing model file name
Product:	UPPAAL	Reporter:	Ferdy Hanssen <hanssen>
Component:	Engine	Assignee:	Gerd Behrmann <behrmann>
Status:	RESOLVED FIXED
Severity:	normal
Priority:	P2
Version:	3.5.7
Hardware:	PC
OS:	Linux
Architecture:

Description Ferdy Hanssen 2005-06-24 13:43:08 CEST

verifyta crashes with a segmentation fault if it is given two arguments: the
model and a query file, where the model is a nonexisting file name, but the
query file does exist.

Comment 1 Gerd Behrmann 2005-06-29 17:51:10 CEST

I have not been able to reproduce this. I tried with UPPAAL 3.4.10, 3.5.6 and 3.5.7. Running something 
like

verifyta foo fischer.q

where foo does not exist but fischer.q does exist produces:

behrmann@bugsy:/tmp/uppaal-3.5.6/bin-Linux$ ls          
fischer.q  server  socketserver  verifyta

behrmann@bugsy:/tmp/uppaal-3.5.6/bin-Linux$ ./verifyta bla fischer.q 
UPPAAL version 3.5.6, Apr 2005 -- verifyta.
Compiled with g++-3.4 -O2 -march=pentiumpro -mtune=pentiumpro.
Copyright (c) 1995 - 2005, Uppsala University and Aalborg University.
All rights reserved.
Options for the verification:
  Diagnostic trace is OFF
  Search order is breadth first
  Using conservative space optimisation
  State space representation uses minimal constraint systems
Could not open file to check: No such file or directory

Comment 2 Ferdy Hanssen 2005-06-29 22:10:43 CEST

Ah, sorry, I was not clear enough.  The extension of the non-existing model 
seems to be important.  Try:

  verifyta foo.xml fischer.q

For me this produces:

UPPAAL version 3.5.6, Apr 2005 -- verifyta.
Compiled with g++-3.4 -O2 -march=pentiumpro -mtune=pentiumpro.
Copyright (c) 1995 - 2005, Uppsala University and Aalborg University.
All rights reserved.
Options for the verification:
  Diagnostic trace is OFF
  Search order is breadth first
  Using conservative space optimisation
  State space representation uses minimal constraint systems

Verifying property 1 at line 6
zsh: segmentation fault  verifyta foo.xml fischer.q

Incidentally, it seems verifyta from Uppaal 3.5.7 reports itself as version 
3.5.6.

Comment 3 Gerd Behrmann 2005-06-30 07:48:58 CEST

Thanks for the extra information. It is also important that the .q file is "correct without a model", i.e. does 
not refer to any variables - otherwise verifyta simply complains about syntax errors in .q.

Will be fixed for 3.5.8.

Comment 4 Gerd Behrmann 2005-07-04 15:54:09 CEST

A fix has been checked into CVS.