Loading nixos/tests/all-tests.nix +1 −0 Original line number Diff line number Diff line Loading @@ -1082,6 +1082,7 @@ in open-web-calendar = runTest ./web-apps/open-web-calendar.nix; ocsinventory-agent = handleTestOn [ "x86_64-linux" "aarch64-linux" ] ./ocsinventory-agent.nix { }; orthanc = runTest ./orthanc.nix; owi = runTest ./owi.nix; owncast = runTest ./owncast.nix; outline = runTest ./outline.nix; i18n = runTest ./i18n.nix; Loading nixos/tests/owi.nix 0 → 100644 +61 −0 Original line number Diff line number Diff line { lib, pkgs, ... }: { name = "owi"; meta.maintainers = with lib.maintainers; [ ethancedwards8 ]; nodes.machine = { environment.systemPackages = with pkgs; [ owi ]; environment.etc."owipass.rs".source = pkgs.writeText "owi.rs" '' use owi_sym::Symbolic; fn mean_one(x: i32, y: i32) -> i32 { (x + y)/2 } fn mean_two(x: i32, y: i32) -> i32 { (y + x)/2 } fn main() { let x = i32::symbol(); let y = i32::symbol(); // proving the commutative property of addition! owi_sym::assert(mean_one(x, y) == mean_two(x, y)) } ''; environment.etc."owifail.rs".source = pkgs.writeText "owi.rs" '' use owi_sym::Symbolic; fn mean_wrong(x: i32, y: i32) -> i32 { (x + y) / 2 } fn mean_correct(x: i32, y: i32) -> i32 { (x & y) + ((x ^ y) >> 1) } fn main() { let x = i32::symbol(); let y = i32::symbol(); owi_sym::assert(mean_wrong(x, y) == mean_correct(x, y)) } ''; }; testScript = { nodes, ... }: '' start_all() # testing machine.succeed("owi rust --fail-on-assertion-only /etc/owipass.rs") machine.fail("owi rust --fail-on-assertion-only /etc/owifail.rs") ''; } pkgs/by-name/ow/owi/package.nix +5 −1 Original line number Diff line number Diff line Loading @@ -7,6 +7,7 @@ zig, makeWrapper, unstableGitUpdater, nixosTests, }: let Loading Loading @@ -75,7 +76,10 @@ ocamlPackages.buildDunePackage rec { doCheck = false; passthru.updateScript = unstableGitUpdater { }; passthru = { updateScript = unstableGitUpdater { }; tests = { inherit (nixosTests) owi; }; }; meta = { description = "Symbolic execution for Wasm, C, C++, Rust and Zig"; Loading Loading
nixos/tests/all-tests.nix +1 −0 Original line number Diff line number Diff line Loading @@ -1082,6 +1082,7 @@ in open-web-calendar = runTest ./web-apps/open-web-calendar.nix; ocsinventory-agent = handleTestOn [ "x86_64-linux" "aarch64-linux" ] ./ocsinventory-agent.nix { }; orthanc = runTest ./orthanc.nix; owi = runTest ./owi.nix; owncast = runTest ./owncast.nix; outline = runTest ./outline.nix; i18n = runTest ./i18n.nix; Loading
nixos/tests/owi.nix 0 → 100644 +61 −0 Original line number Diff line number Diff line { lib, pkgs, ... }: { name = "owi"; meta.maintainers = with lib.maintainers; [ ethancedwards8 ]; nodes.machine = { environment.systemPackages = with pkgs; [ owi ]; environment.etc."owipass.rs".source = pkgs.writeText "owi.rs" '' use owi_sym::Symbolic; fn mean_one(x: i32, y: i32) -> i32 { (x + y)/2 } fn mean_two(x: i32, y: i32) -> i32 { (y + x)/2 } fn main() { let x = i32::symbol(); let y = i32::symbol(); // proving the commutative property of addition! owi_sym::assert(mean_one(x, y) == mean_two(x, y)) } ''; environment.etc."owifail.rs".source = pkgs.writeText "owi.rs" '' use owi_sym::Symbolic; fn mean_wrong(x: i32, y: i32) -> i32 { (x + y) / 2 } fn mean_correct(x: i32, y: i32) -> i32 { (x & y) + ((x ^ y) >> 1) } fn main() { let x = i32::symbol(); let y = i32::symbol(); owi_sym::assert(mean_wrong(x, y) == mean_correct(x, y)) } ''; }; testScript = { nodes, ... }: '' start_all() # testing machine.succeed("owi rust --fail-on-assertion-only /etc/owipass.rs") machine.fail("owi rust --fail-on-assertion-only /etc/owifail.rs") ''; }
pkgs/by-name/ow/owi/package.nix +5 −1 Original line number Diff line number Diff line Loading @@ -7,6 +7,7 @@ zig, makeWrapper, unstableGitUpdater, nixosTests, }: let Loading Loading @@ -75,7 +76,10 @@ ocamlPackages.buildDunePackage rec { doCheck = false; passthru.updateScript = unstableGitUpdater { }; passthru = { updateScript = unstableGitUpdater { }; tests = { inherit (nixosTests) owi; }; }; meta = { description = "Symbolic execution for Wasm, C, C++, Rust and Zig"; Loading