diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index c1aab6ced..863e1198e 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -83,6 +83,11 @@ storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_f separator[3] = '\t'; separator[4] = '\0'; break; + default: + case SupportedLineEndingsEnum::Unsupported: + // This Line will never be reached as the Parser would have thrown already. + throw; + break; } bool foundDecl = false, foundEnd = false; diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index 0b84a339d..304720f12 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -108,32 +108,7 @@ class AutoParser { // parse hint char hint[128]; // %20s => The Input Hint can be AT MOST 120 chars long - switch (lineEndings) { - case storm::parser::SupportedLineEndingsEnum::SlashN: -#ifdef WINDOWS - sscanf_s(buf, "%120s\n", hint, sizeof(hint)); -#else - sscanf(buf, "%120s\n", hint); -#endif - break; - case storm::parser::SupportedLineEndingsEnum::SlashR: -#ifdef WINDOWS - sscanf_s(buf, "%120s\r", hint, sizeof(hint)); -#else - sscanf(buf, "%120s\r", hint); -#endif - break; - case storm::parser::SupportedLineEndingsEnum::SlashRN: -#ifdef WINDOWS - sscanf_s(buf, "%120s\r\n", hint, sizeof(hint)); -#else - sscanf(buf, "%120s\r\n", hint); -#endif - break; - default: - LOG4CPLUS_ERROR(logger, "The given input file \"" << filename << "\" has no or unsupported line endings. Please use either \\r, \\n or \\r\\n."); - throw storm::exceptions::WrongFormatException() << "The given input file \"" << filename << "\" has no or unsupported line endings. Please use either \\r, \\n or \\r\\n."; - } + storm::parser::scanForModelHint(hint, sizeof(hint), buf, lineEndings); for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 9b2ee51cd..6e3f99630 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -54,17 +54,7 @@ uint_fast64_t firstPass(char* buf, SupportedLineEndingsEnum lineEndings, uint_fa */ if (!isRewardMatrix) { // skip format hint - switch (lineEndings) { - case SupportedLineEndingsEnum::SlashN: - buf = strchr(buf, '\n') + 1; - break; - case SupportedLineEndingsEnum::SlashR: - buf = strchr(buf, '\r') + 1; - break; - case SupportedLineEndingsEnum::SlashRN: - buf = strchr(buf, '\r') + 2; - break; - } + buf = storm::parser::forwardToNextLine(buf, lineEndings); } /* @@ -192,17 +182,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st */ if (!isRewardMatrix) { // skip format hint - switch (lineEndings) { - case SupportedLineEndingsEnum::SlashN: - buf = strchr(buf, '\n') + 1; - break; - case SupportedLineEndingsEnum::SlashR: - buf = strchr(buf, '\r') + 1; - break; - case SupportedLineEndingsEnum::SlashRN: - buf = strchr(buf, '\r') + 2; - break; - } + buf = storm::parser::forwardToNextLine(buf, lineEndings); } // If the matrix that is being parsed is a reward matrix, it should match the size of the diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 2ff9eade5..fdedd3766 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -57,17 +57,7 @@ uint_fast64_t firstPass(char* buf, SupportedLineEndingsEnum lineEndings, uint_fa */ if (!isRewardFile) { // skip format hint - switch (lineEndings) { - case SupportedLineEndingsEnum::SlashN: - buf = strchr(buf, '\n') + 1; - break; - case SupportedLineEndingsEnum::SlashR: - buf = strchr(buf, '\r') + 1; - break; - case SupportedLineEndingsEnum::SlashRN: - buf = strchr(buf, '\r') + 2; - break; - } + buf = storm::parser::forwardToNextLine(buf, lineEndings); } /* @@ -170,6 +160,11 @@ uint_fast64_t firstPass(char* buf, SupportedLineEndingsEnum lineEndings, uint_fa case SupportedLineEndingsEnum::SlashRN: buf += strcspn(buf, " \t\r\n"); break; + default: + case storm::parser::SupportedLineEndingsEnum::Unsupported: + // This Line will never be reached as the Parser would have thrown already. + throw; + break; } buf = trimWhitespaces(buf); } @@ -248,17 +243,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP */ if (!isRewardFile) { // skip format hint - switch (lineEndings) { - case SupportedLineEndingsEnum::SlashN: - buf = strchr(buf, '\n') + 1; - break; - case SupportedLineEndingsEnum::SlashR: - buf = strchr(buf, '\r') + 1; - break; - case SupportedLineEndingsEnum::SlashRN: - buf = strchr(buf, '\r') + 2; - break; - } + buf = storm::parser::forwardToNextLine(buf, lineEndings); } if (isRewardFile) { @@ -385,6 +370,11 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP case SupportedLineEndingsEnum::SlashRN: buf += strcspn(buf, " \t\r\n"); break; + default: + case storm::parser::SupportedLineEndingsEnum::Unsupported: + // This Line will never be reached as the Parser would have thrown already. + throw; + break; } buf = trimWhitespaces(buf); } diff --git a/src/parser/Parser.cpp b/src/parser/Parser.cpp index dbc2849c5..36fd4483d 100644 --- a/src/parser/Parser.cpp +++ b/src/parser/Parser.cpp @@ -99,6 +99,68 @@ storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std:: return storm::parser::SupportedLineEndingsEnum::Unsupported; } +/*! + * @brief Encapsulates the usage of function @strchr to forward to the next line + */ +char* forwardToNextLine(char* buffer, storm::parser::SupportedLineEndingsEnum lineEndings) { + switch (lineEndings) { + case storm::parser::SupportedLineEndingsEnum::SlashN: + return strchr(buffer, '\n') + 1; + break; + case storm::parser::SupportedLineEndingsEnum::SlashR: + return strchr(buffer, '\r') + 1; + break; + case storm::parser::SupportedLineEndingsEnum::SlashRN: + return strchr(buffer, '\r') + 2; + break; + default: + case storm::parser::SupportedLineEndingsEnum::Unsupported: + // This Line will never be reached as the Parser would have thrown already. + throw; + break; + } + return nullptr; +} + +/*! + * @brief Encapsulates the usage of function @sscanf to scan for the model type hint + * @param targetBuffer The Target for the hint, must be at least 64 bytes long + * @param buffer The Source Buffer from which the Model Hint will be read + */ +void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, storm::parser::SupportedLineEndingsEnum lineEndings) { + if (targetBufferSize <= 4) { + throw; + } + switch (lineEndings) { + case storm::parser::SupportedLineEndingsEnum::SlashN: +#ifdef WINDOWS + sscanf_s(buffer, "%60s\n", targetBuffer, targetBufferSize); +#else + sscanf(buffer, "%60s\n", targetBuffer); +#endif + break; + case storm::parser::SupportedLineEndingsEnum::SlashR: +#ifdef WINDOWS + sscanf_s(buffer, "%60s\r", targetBuffer, sizeof(targetBufferSize)); +#else + sscanf(buffer, "%60s\r", targetBuffer); +#endif + break; + case storm::parser::SupportedLineEndingsEnum::SlashRN: +#ifdef WINDOWS + sscanf_s(buffer, "%60s\r\n", targetBuffer, sizeof(targetBufferSize)); +#else + sscanf(buffer, "%60s\r\n", targetBuffer); +#endif + break; + default: + case storm::parser::SupportedLineEndingsEnum::Unsupported: + // This Line will never be reached as the Parser would have thrown already. + throw; + break; + } +} + /*! * Will stat the given file, open it and map it to memory. * If anything of this fails, an appropriate exception is raised diff --git a/src/parser/Parser.h b/src/parser/Parser.h index 62dc75d1f..29c6073de 100644 --- a/src/parser/Parser.h +++ b/src/parser/Parser.h @@ -150,6 +150,19 @@ namespace parser { */ storm::parser::SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported = false); + /*! + * @brief Encapsulates the usage of function @strchr to forward to the next line + */ + char* forwardToNextLine(char* buffer, storm::parser::SupportedLineEndingsEnum lineEndings); + + /*! + * @brief Encapsulates the usage of function @sscanf to scan for the model type hint + * @param targetBuffer The Target for the hint, should be at least 64 bytes long + * @param buffer The Source Buffer from which the Model Hint will be read + + */ + void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, storm::parser::SupportedLineEndingsEnum lineEndings); + } // namespace parser } // namespace storm