search

prismmodelchecker / prism

The main development version of the PRISM model checker.
http://www.prismmodelchecker.org/
GNU General Public License v2.0
156 stars 71 forks source link

Silent cast errors. #92

Open merkste opened 6 years ago

merkste commented 6 years ago

Currently, integer overflows and underflows are silent errors during expression evaluation. This may lead to models that are broken without a chance for the author to recognise the error. See PR #91 .

merkste commented 6 years ago

I had another look at the code and I suggest to fix this for pure integer-vector operations as well. As far as I can see, they are not that often used. Hence, I expect no major performance penalty during the computations. (And I like prioritizing correctness over speed.)