|Summary:||verifyta segfaults on an array with dimension >32x32|
|Product:||UPPAAL||Reporter:||Juhan Ernits <juhan>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
|Version:||3.6 Alpha 4|
|Attachments:||A tiny model containing an array with dimension 33|
Description Juhan Ernits 2006-02-15 00:41:16 CET
The backend segfaults when one feeds an array of constants to it that has dimension larger than 32. To get the segfault run model checking from the GUI or by invoking verifyta -N array_of_constants.xml array_of_constants.q
Comment 1 Juhan Ernits 2006-02-15 00:43:54 CET
Created attachment 90 [details] A tiny model containing an array with dimension 33
Comment 2 Gerd Behrmann 2006-02-15 09:39:05 CET
I can confirm the segfault on the attached model. However, it does not segfault with an array of dimension > 32, but with an array bigger than 32x32 (multi-dimensional array) - which is what the attached model contains.
Comment 3 Gerd Behrmann 2006-02-15 09:46:55 CET
Further clarification: It also crashes with array of non-constants.
Comment 4 Gerd Behrmann 2006-02-15 09:55:02 CET
A multidimensional array is not necessary to trigger the problem. An array of integers of size 1021 is enough. It also turns out that an initialiser is not required to cause the crash.
Comment 5 Gerd Behrmann 2006-02-15 10:25:02 CET
More info: Only on the latest versions on the trunk, does a model with a large array of integers without an initialiser cause a crash. The problem seems to be a stack overflow of the virtual machine: The initialiser (either given by the user or auto generated) is evaluated and the result stored on the VM stack. Two things should be done: 1. The stack should be enlarged to cope with larger arrays (1020 is too small). 2. Detection of stack overflow must be added.
Comment 6 Gerd Behrmann 2006-03-10 15:09:36 CET
I have added code to estimate the correct stack size. This should solve the problem.