diff --git a/flux_support/Cargo.toml b/flux_support/Cargo.toml new file mode 100644 index 0000000000..8b742e7064 --- /dev/null +++ b/flux_support/Cargo.toml @@ -0,0 +1,10 @@ +[package] +name = "flux_support" +version.workspace = true +authors.workspace = true +edition.workspace = true + +[package.metadata.flux] +enabled = true + +[dependencies] diff --git a/flux_support/src/lib.rs b/flux_support/src/lib.rs new file mode 100644 index 0000000000..b52357bb8a --- /dev/null +++ b/flux_support/src/lib.rs @@ -0,0 +1,11 @@ +#[allow(dead_code)] +#[flux::sig(fn(x: bool[true]))] +pub fn assert(_x: bool) {} + +#[flux::sig(fn(b:bool) ensures b)] +pub fn assume(b: bool) { + if !b { + panic!("assume fails") + } +} +