boogie: 2.15.7 -> 3.0.4

Also add install check to verify all dependencies (ie. z3) work

2 files changed, 74 insertions, 5 deletions

diff --git a/pkgs/by-name/bo/boogie/install-check-file.bpl b/pkgs/by-name/bo/boogie/install-check-file.bpl
new file mode 100644
index 0000000000000..8548c612d06e2
--- /dev/null
+++ b/pkgs/by-name/bo/boogie/install-check-file.bpl
@@ -0,0 +1,61 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+
+function {:builtin "MapAdd"} mapadd([X]int, [X]int) : [X]int;
+function {:builtin "MapSub"} mapsub([X]int, [X]int) : [X]int;
+function {:builtin "MapMul"} mapmul([X]int, [X]int) : [X]int;
+function {:builtin "MapDiv"} mapdiv([X]int, [X]int) : [X]int;
+function {:builtin "MapMod"} mapmod([X]int, [X]int) : [X]int;
+function {:builtin "MapConst"} mapconstint(int) : [X]int;
+function {:builtin "MapConst"} mapconstbool(bool) : [X]bool;
+function {:builtin "MapAnd"} mapand([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapOr"} mapor([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapNot"} mapnot([X]bool) : [X]bool;
+function {:builtin "MapIte"} mapiteint([X]bool, [X]int, [X]int) : [X]int;
+function {:builtin "MapIte"} mapitebool([X]bool, [X]bool, [X]bool) : [X]bool;
+function {:builtin "MapLe"} maple([X]int, [X]int) : [X]bool;
+function {:builtin "MapLt"} maplt([X]int, [X]int) : [X]bool;
+function {:builtin "MapGe"} mapge([X]int, [X]int) : [X]bool;
+function {:builtin "MapGt"} mapgt([X]int, [X]int) : [X]bool;
+function {:builtin "MapEq"} mapeq([X]int, [X]int) : [X]bool;
+function {:builtin "MapIff"} mapiff([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapImp"} mapimp([X]bool, [X]bool) : [X]bool;
+
+
+
+const FF: [X]bool;
+axiom FF == mapconstbool(false);
+
+const TT: [X]bool;
+axiom TT == mapconstbool(true);
+
+const MultisetEmpty: [X]int;
+axiom MultisetEmpty == mapconstint(0);
+
+function {:inline} MultisetSingleton(x: X) : [X]int
+{
+  MultisetEmpty[x := 1]
+}
+
+function {:inline} MultisetPlus(a: [X]int, b: [X]int) : [X]int
+{
+  mapadd(a, b)
+}
+
+function {:inline} MultisetMinus(a: [X]int, b: [X]int)  : [X]int
+{
+  mapiteint(mapgt(a, b), mapsub(a, b), mapconstint(0))
+}
+
+procedure foo() {
+  var x: X;
+
+  assert FF != TT;
+  assert mapnot(FF) == TT;
+
+  assert MultisetSingleton(x) != MultisetEmpty;
+  assert MultisetPlus(MultisetEmpty, MultisetSingleton(x)) == MultisetSingleton(x);
+  assert MultisetMinus(MultisetPlus(MultisetEmpty, MultisetSingleton(x)), MultisetSingleton(x)) == MultisetEmpty;
+  assert MultisetMinus(MultisetEmpty, MultisetSingleton(x)) == MultisetEmpty;
+}
diff --git a/pkgs/by-name/bo/boogie/package.nix b/pkgs/by-name/bo/boogie/package.nix
index 8f15c0631256a..44811a33b6371 100644
--- a/pkgs/by-name/bo/boogie/package.nix
+++ b/pkgs/by-name/bo/boogie/package.nix
@@ -2,22 +2,25 @@
 
 buildDotnetModule rec {
   pname = "Boogie";
-  version = "2.15.7";
+  version = "3.0.4";
 
   src = fetchFromGitHub {
     owner = "boogie-org";
     repo = "boogie";
     rev = "v${version}";
-    sha256 = "16kdvkbx2zwj7m43cra12vhczbpj23wyrdnj0ygxf7np7c2aassp";
+    sha256 = "sha256-yebThnIOpZ5crYsSZtbDj8Gn6DznTNJ4T/TsFR3gWvs=";
   };
 
   projectFile = [ "Source/Boogie.sln" ];
   nugetDeps = ./deps.nix;
 
-  postInstall = ''
-      mkdir -pv "$out/lib/dotnet/${pname}"
-      ln -sv "${z3}/bin/z3" "$out/lib/dotnet/${pname}/z3.exe"
+  executables = [ "BoogieDriver" ];
+
+  makeWrapperArgs = [
+    "--prefix PATH : ${z3}/bin"
+  ];
 
+  postInstall = ''
       # so that this derivation can be used as a vim plugin to install syntax highlighting
       vimdir=$out/share/vim-plugins/boogie
       install -Dt $vimdir/syntax/ Util/vim/syntax/boogie.vim
@@ -32,6 +35,11 @@ buildDotnetModule rec {
       rm -f $out/bin/{Microsoft,NUnit3,System}.* "$out/bin"/*Tests
   '';
 
+  doInstallCheck = true;
+  installCheckPhase = ''
+    $out/bin/boogie ${./install-check-file.bpl}
+  '';
+
   meta = with lib; {
     description = "An intermediate verification language";
     homepage = "https://github.com/boogie-org/boogie";