Skip to content

#1225 BddUtils.valuationToStates no longer crashes due to initializing a list with negative initial size

  • End-user visible change for the CIF controller properties checker:
    • The bounded response check no longer crashes in certain cases where bounded response doesn't hold and there are very many possible states where there is no bounded response. There was already a limit on the number of states to print, but the calculation could result in integer overflow, which could lead to crashes. Some of such cases where already fixed in release v7.0, and the remaining cases have now been fixed as well (issue #1138 (closed)).
    • The 'Maximum number of printed cycle states' option now accepts 2,147,483,639 as the largest number of cycle states to print, instead of 2,147,483,637.
  • Internal changes:
    • Introduced Lists.MAX_SAFE_LIST_SIZE.
    • BddUtils.valuationToStates now limits the maximum length of the list of valuations to Lists.MAX_SAFE_LIST_SIZE.
    • BddUtils.valuationToStates no longer crashes due to initializing a list with a negative initial size.
    • MaxPrintedCycleStatesOption adapted to consistently match Lists.MAX_SAFE_LIST_SIZE.

Closes #1225 (closed)

Edited by Dennis Hendriks

Merge request reports

Loading