Bug 165 - verifyta crashes on non-existing model file name
Summary: verifyta crashes on non-existing model file name
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.5.7
Hardware: PC Linux
: P2 normal
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2005-06-24 13:43 CEST by Ferdy Hanssen
Modified: 2005-07-04 15:54 CEST (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 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.