From f169931eac1e7ee0bf24ed02c443d474620c108c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Fri, 29 May 2020 18:53:42 +0200
Subject: [PATCH] Accept more than one specification file

---
 src/commands/verify_program.rs | 38 +++++++++++++++++++---------------
 src/main.rs                    |  8 +++----
 2 files changed, 25 insertions(+), 21 deletions(-)

diff --git a/src/commands/verify_program.rs b/src/commands/verify_program.rs
index 9054b9e..ee853d7 100644
--- a/src/commands/verify_program.rs
+++ b/src/commands/verify_program.rs
@@ -1,32 +1,36 @@
-pub fn run<P>(program_path: P, specification_path: P,
+pub fn run<P1, P2>(program_path: P1, specification_paths: &[P2],
 	proof_direction: crate::problem::ProofDirection, no_simplify: bool,
 	color_choice: crate::output::ColorChoice)
 where
-	P: AsRef<std::path::Path>,
+	P1: AsRef<std::path::Path>,
+	P2: AsRef<std::path::Path>,
 {
 	let mut problem = crate::Problem::new(color_choice);
 
-	log::info!("reading specification “{}”", specification_path.as_ref().display());
-
-	let specification_content = match std::fs::read_to_string(specification_path.as_ref())
+	for specification_path in specification_paths
 	{
-		Ok(specification_content) => specification_content,
-		Err(error) =>
+		log::info!("reading specification file “{}”", specification_path.as_ref().display());
+
+		let specification_content = match std::fs::read_to_string(specification_path.as_ref())
 		{
-			log::error!("could not access specification file: {}", error);
+			Ok(specification_content) => specification_content,
+			Err(error) =>
+			{
+				log::error!("could not access specification file: {}", error);
+				std::process::exit(1)
+			},
+		};
+
+		// TODO: rename to read_specification
+		if let Err(error) = crate::input::parse_specification(&specification_content, &mut problem)
+		{
+			log::error!("could not read specification file: {}", error);
 			std::process::exit(1)
-		},
-	};
+		}
 
-	// TODO: rename to read_specification
-	if let Err(error) = crate::input::parse_specification(&specification_content, &mut problem)
-	{
-		log::error!("could not read specification: {}", error);
-		std::process::exit(1)
+		log::info!("read specification “{}”", specification_path.as_ref().display());
 	}
 
-	log::info!("read specification “{}”", specification_path.as_ref().display());
-
 	problem.process_output_predicates();
 
 	log::info!("reading input program “{}”", program_path.as_ref().display());
diff --git a/src/main.rs b/src/main.rs
index ff4c514..edf9dd5 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -13,8 +13,8 @@ enum Command
 		program_path: std::path::PathBuf,
 
 		#[structopt(name = "specification", parse(from_os_str), required(true))]
-		/// Specification file path
-		specification_path: std::path::PathBuf,
+		/// One or more specification file paths
+		specification_paths: Vec<std::path::PathBuf>,
 
 		/// Proof direction (forward, backward, both)
 		#[structopt(long, default_value = "forward")]
@@ -41,12 +41,12 @@ fn main()
 		Command::VerifyProgram
 		{
 			program_path,
-			specification_path,
+			specification_paths,
 			proof_direction,
 			no_simplify,
 			color_choice,
 		}
-			=> anthem::commands::verify_program::run(&program_path, &specification_path,
+			=> anthem::commands::verify_program::run(&program_path, specification_paths.as_slice(),
 				proof_direction, no_simplify, color_choice),
 	}
 }