From af8d9b0ad8a6977f9f538556719a75ce4c3ae8ef Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 23 Sep 2016 10:54:47 +0200 Subject: [PATCH] added underflow check in PRISM next-state generator Former-commit-id: dc7f0ea3c7f88936c0d02bb44379b12e5c7f667e --- src/generator/PrismNextStateGenerator.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 7eb2291c5..ab1311076 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -305,6 +305,7 @@ namespace storm { } int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getExpression()); STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); + STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); }