patrick/anthem-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Accept more than one specification file

Browse Source
This commit is contained in:
Patrick Lühne 2020-05-29 18:53:42 +02:00
parent 27fff47c91
commit f169931eac
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 25 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
src/commands/verify_program.rs
View File

@ -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, proof_direction: crate::problem::ProofDirection, no_simplify: bool,
color_choice: crate::output::ColorChoice) color_choice: crate::output::ColorChoice)
where where
P: AsRef<std::path::Path>, P1: AsRef<std::path::Path>,
P2: AsRef<std::path::Path>,
{ {
let mut problem = crate::Problem::new(color_choice); let mut problem = crate::Problem::new(color_choice);
log::info!("reading specification “{}”", specification_path.as_ref().display()); for specification_path in specification_paths
let specification_content = match std::fs::read_to_string(specification_path.as_ref())
{ {
Ok(specification_content) => specification_content, log::info!("reading specification file “{}”", specification_path.as_ref().display());
Err(error) =>
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) std::process::exit(1)
}, }
};
// TODO: rename to read_specification log::info!("read specification “{}”", specification_path.as_ref().display());
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());
problem.process_output_predicates(); problem.process_output_predicates();
log::info!("reading input program “{}”", program_path.as_ref().display()); log::info!("reading input program “{}”", program_path.as_ref().display());

8
src/main.rs
View File

@ -13,8 +13,8 @@ enum Command
program_path: std::path::PathBuf, program_path: std::path::PathBuf,
#[structopt(name = "specification", parse(from_os_str), required(true))] #[structopt(name = "specification", parse(from_os_str), required(true))]
/// Specification file path /// One or more specification file paths
specification_path: std::path::PathBuf, specification_paths: Vec<std::path::PathBuf>,
/// Proof direction (forward, backward, both) /// Proof direction (forward, backward, both)
#[structopt(long, default_value = "forward")] #[structopt(long, default_value = "forward")]
@ -41,12 +41,12 @@ fn main()
Command::VerifyProgram Command::VerifyProgram
{ {
program_path, program_path,
specification_path, specification_paths,
proof_direction, proof_direction,
no_simplify, no_simplify,
color_choice, 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), proof_direction, no_simplify, color_choice),
} }
} }