Browse Source

added underflow check in PRISM next-state generator

Former-commit-id: dc7f0ea3c7
tempestpy_adaptions
dehnert 8 years ago
parent
commit
af8d9b0ad8
  1. 1
      src/generator/PrismNextStateGenerator.cpp

1
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<int_fast64_t>(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 << ").");
}

Loading…
Cancel
Save