Skip to content

Commit

Permalink
Merge branch 'master' into install-opam
Browse files Browse the repository at this point in the history
  • Loading branch information
Lysxia authored Feb 20, 2025
2 parents 4fd7881 + 11089ea commit 5a319e8
Showing 1 changed file with 69 additions and 31 deletions.
100 changes: 69 additions & 31 deletions creusot/tests/ui.rs
Original file line number Diff line number Diff line change
Expand Up @@ -69,22 +69,58 @@ fn main() {
temp_file.push("libcreusot_contracts.cmeta");
let temp_file = temp_file.to_string_lossy();

translate_creusot_contracts(&args, creusot_rustc, &base_path, &temp_file);

should_fail("tests/should_fail/**/*.rs", &args, |p| run_creusot(creusot_rustc, p, &temp_file));
should_succeed("tests/should_succeed/**/*.rs", &args, |p| {
let mut test_creusot_contracts = true;
if let Some(ref filter) = args.filter {
if !"creusot/tests/creusot-contracts/creusot-contracts.rs".contains(filter) {
test_creusot_contracts = false;
}
}
let contracts_success = translate_creusot_contracts(
&args,
creusot_rustc,
&base_path,
&temp_file,
test_creusot_contracts,
);

let (mut failed, mut total) =
(if contracts_success { 0 } else { 1 }, if test_creusot_contracts { 1 } else { 0 });

let (fail1, total1) = should_fail("tests/should_fail/**/*.rs", &args, |p| {
run_creusot(creusot_rustc, p, &temp_file)
});
let (fail2, total2) = should_succeed("tests/should_succeed/**/*.rs", &args, |p| {
run_creusot(creusot_rustc, p, &temp_file)
});

total += total1 + total2;
failed += fail1 + fail2;
if failed > 0 {
let mut out =
StandardStream::stdout(if args.force_color || std::io::stdout().is_terminal() {
ColorChoice::Always
} else {
ColorChoice::Never
});
out.set_color(ColorSpec::new().set_fg(Some(Color::Red))).unwrap();
writeln!(&mut out, "{failed} failures out of {total} tests").unwrap();
drop(out);
std::process::exit(1);
}

println!("All tests passed!");
}

/// Returns `false` if the translation changed
///
/// This will only check the output of `creusot-contracts` if `test_creusot_contracts` is true.
fn translate_creusot_contracts(
args: &Args,
creusot_rustc: &Path,
base_path: &PathBuf,
temp_file: &str,
) {
test_creusot_contracts: bool,
) -> bool {
println! {"Building cargo-creusot..."};
let cargo_creusot = escargot::CargoBuild::new()
.bin("cargo-creusot")
Expand All @@ -95,13 +131,15 @@ fn translate_creusot_contracts(
.unwrap()
.command();

print! {"Translating creusot-contracts... "};
std::io::stdout().flush().unwrap();
std::process::Command::new("touch")
.current_dir(&base_path)
.args(["creusot-contracts/src/lib.rs"])
.status()
.unwrap();
if test_creusot_contracts {
print!("Translating creusot-contracts... ");
std::io::stdout().flush().unwrap();
std::process::Command::new("touch")
.current_dir(&base_path)
.args(["creusot-contracts/src/lib.rs"])
.status()
.unwrap();
}
let mut creusot_contracts = cargo_creusot;
creusot_contracts.current_dir(base_path);
creusot_contracts
Expand All @@ -121,16 +159,24 @@ fn translate_creusot_contracts(
.env("CREUSOT_CONTINUE", "true");

let output = creusot_contracts.output().expect("could not translate `creusot_contracts`");
let expect = PathBuf::from("tests/creusot-contracts/creusot-contracts.coma");
if !output.status.success() {
eprintln!("Translation of creusot-contracts failed");
std::process::exit(1);
}

if !test_creusot_contracts {
return true;
}

let expect = PathBuf::from("tests/creusot-contracts/creusot-contracts.coma");
let is_tty = std::io::stdout().is_terminal();
let mut out = StandardStream::stdout(if args.force_color || is_tty {
ColorChoice::Always
} else {
ColorChoice::Never
});
let mut succeeded = true;

let mut failed = false;
if args.bless {
if output.stdout.is_empty() {
panic!(
Expand Down Expand Up @@ -160,7 +206,7 @@ fn translate_creusot_contracts(
out.set_color(ColorSpec::new().set_fg(Some(Color::Red))).unwrap();
writeln!(&mut out, "failure").unwrap();

failed = true;
succeeded = false;
};
out.reset().unwrap();

Expand All @@ -169,10 +215,7 @@ fn translate_creusot_contracts(
out.flush().unwrap();
}

if !output.status.success() || failed {
eprintln!("Translation of creusot-contracts failed");
std::process::exit(1);
}
succeeded
}

fn run_creusot(
Expand Down Expand Up @@ -242,18 +285,18 @@ fn run_creusot(
Some(cmd)
}

fn should_succeed<B>(s: &str, args: &Args, b: B)
fn should_succeed<B>(s: &str, args: &Args, b: B) -> (usize, usize)
where
B: Fn(&Path) -> Option<std::process::Command> + Send + Sync,
{
glob_runner(s, args, b, true);
glob_runner(s, args, b, true)
}

fn should_fail<B>(s: &str, args: &Args, b: B)
fn should_fail<B>(s: &str, args: &Args, b: B) -> (usize, usize)
where
B: Fn(&Path) -> Option<std::process::Command> + Send + Sync,
{
glob_runner(s, args, b, false);
glob_runner(s, args, b, false)
}

/// Replace global paths in `s` with ".", provided `s` is in fact a string.
Expand All @@ -269,7 +312,8 @@ fn erase_global_paths(s: &mut Vec<u8>) {
}
}

fn glob_runner<B>(s: &str, args: &Args, command_builder: B, should_succeed: bool)
/// Returns `(tests failed, total tests)`
fn glob_runner<B>(s: &str, args: &Args, command_builder: B, should_succeed: bool) -> (usize, usize)
where
B: Fn(&Path) -> Option<std::process::Command> + Send + Sync,
{
Expand Down Expand Up @@ -420,12 +464,6 @@ where

let test_count = test_count.load(atomic::Ordering::SeqCst);
let test_failures = test_failures.load(atomic::Ordering::SeqCst);
let (_, mut out) = out.into_inner().unwrap();

if test_failures > 0 {
out.set_color(ColorSpec::new().set_fg(Some(Color::Red))).unwrap();
writeln!(&mut out, "{test_failures} failures out of {test_count} tests").unwrap();
drop(out);
std::process::exit(1);
}
(test_failures, test_count)
}

0 comments on commit 5a319e8

Please sign in to comment.