From 1bff09f2ff137c5fe35199bd0f77ce7506c3bfb5 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 21 May 2019 16:26:20 -0700 Subject: [PATCH 1/3] Fix warning --- frontends/aiger/aigerparse.cc | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 2e4774dfd..566825ece 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -55,9 +55,8 @@ void AigerReader::parse_aiger() // Optional values B = C = J = F = 0; - for (auto &i : std::array,4>{B, C, J, F}) { - if (f.peek() != ' ') break; - if (!(f >> i)) + if (f.peek() == ' ') { + if (!(f >> B >> C >> J >> F)) log_error("Invalid AIGER header\n"); } From b5a29460b9328fe86739039b05daaf70355502fa Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 21 May 2019 17:20:19 -0700 Subject: [PATCH 2/3] Try again --- frontends/aiger/aigerparse.cc | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 566825ece..e5ec475d1 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -55,10 +55,16 @@ void AigerReader::parse_aiger() // Optional values B = C = J = F = 0; - if (f.peek() == ' ') { - if (!(f >> B >> C >> J >> F)) - log_error("Invalid AIGER header\n"); - } + if (f.peek() != ' ') goto parse_body; + if (!(f >> B)) log_error("Invalid AIGER header\n"); + if (f.peek() != ' ') goto parse_body; + if (!(f >> C)) log_error("Invalid AIGER header\n"); + if (f.peek() != ' ') goto parse_body; + if (!(f >> J)) log_error("Invalid AIGER header\n"); + if (f.peek() != ' ') goto parse_body; + if (!(f >> F)) log_error("Invalid AIGER header\n"); + +parse_body: std::string line; std::getline(f, line); // Ignore up to start of next line, as standard From 705775342774cff735ba13d2c3216680ae98b7a0 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 21 May 2019 18:20:31 -0700 Subject: [PATCH 3/3] Rename label --- frontends/aiger/aigerparse.cc | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index e5ec475d1..38348cd65 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -55,16 +55,15 @@ void AigerReader::parse_aiger() // Optional values B = C = J = F = 0; - if (f.peek() != ' ') goto parse_body; + if (f.peek() != ' ') goto end_of_header; if (!(f >> B)) log_error("Invalid AIGER header\n"); - if (f.peek() != ' ') goto parse_body; + if (f.peek() != ' ') goto end_of_header; if (!(f >> C)) log_error("Invalid AIGER header\n"); - if (f.peek() != ' ') goto parse_body; + if (f.peek() != ' ') goto end_of_header; if (!(f >> J)) log_error("Invalid AIGER header\n"); - if (f.peek() != ' ') goto parse_body; + if (f.peek() != ' ') goto end_of_header; if (!(f >> F)) log_error("Invalid AIGER header\n"); - -parse_body: +end_of_header: std::string line; std::getline(f, line); // Ignore up to start of next line, as standard