From 35a8e310367a95a74eeef709d7ecb0ae2287c6d0 Mon Sep 17 00:00:00 2001 From: Sergei Zimmerman <145775305+xokdvium@users.noreply.github.com> Date: Mon, 6 Jan 2025 15:55:43 +0300 Subject: [PATCH 1/6] cbmc: drop unused fetchurl --- pkgs/by-name/cb/cbmc/package.nix | 1 - 1 file changed, 1 deletion(-) diff --git a/pkgs/by-name/cb/cbmc/package.nix b/pkgs/by-name/cb/cbmc/package.nix index 730449c04de29..59c59c031f2cd 100644 --- a/pkgs/by-name/cb/cbmc/package.nix +++ b/pkgs/by-name/cb/cbmc/package.nix @@ -12,7 +12,6 @@ perl, substituteAll, cudd, - fetchurl, nix-update-script, }: From d22cf684708bb4d835ae2384a14cd5ab5c1b065b Mon Sep 17 00:00:00 2001 From: Sergei Zimmerman <145775305+xokdvium@users.noreply.github.com> Date: Mon, 6 Jan 2025 17:06:43 +0300 Subject: [PATCH 2/6] cbmc: drop unused cadical from build inputs This is cruft left over from , which got rid of the patch to use compiled cadical instead of building from source. --- pkgs/by-name/cb/cbmc/package.nix | 5 ----- 1 file changed, 5 deletions(-) diff --git a/pkgs/by-name/cb/cbmc/package.nix b/pkgs/by-name/cb/cbmc/package.nix index 59c59c031f2cd..eb8697b8927b8 100644 --- a/pkgs/by-name/cb/cbmc/package.nix +++ b/pkgs/by-name/cb/cbmc/package.nix @@ -46,10 +46,6 @@ stdenv.mkDerivation (finalAttrs: { makeWrapper ]; - buildInputs = [ cadical ]; - - # do not download sources - # link existing cadical instead patches = [ (substituteAll { src = ./0001-Do-not-download-sources-in-cmake.patch; @@ -104,7 +100,6 @@ stdenv.mkDerivation (finalAttrs: { cmakeFlags = [ "-DWITH_JBMC=OFF" "-Dsat_impl=cadical" - "-Dcadical_INCLUDE_DIR=${cadical.dev}/include" ]; passthru.tests.version = testers.testVersion { From 5ee632beb872e6e22e2caa35613b1728739558fa Mon Sep 17 00:00:00 2001 From: Sergei Zimmerman <145775305+xokdvium@users.noreply.github.com> Date: Mon, 6 Jan 2025 17:55:17 +0300 Subject: [PATCH 3/6] cbmc: fix update script --- pkgs/by-name/cb/cbmc/package.nix | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/pkgs/by-name/cb/cbmc/package.nix b/pkgs/by-name/cb/cbmc/package.nix index eb8697b8927b8..87672e901312e 100644 --- a/pkgs/by-name/cb/cbmc/package.nix +++ b/pkgs/by-name/cb/cbmc/package.nix @@ -107,7 +107,12 @@ stdenv.mkDerivation (finalAttrs: { command = "cbmc --version"; }; - passthru.updateScript = nix-update-script { }; + passthru.updateScript = nix-update-script { + extraArgs = [ + "--version-regex" + "cbmc-(.*)" + ]; + }; meta = { description = "CBMC is a Bounded Model Checker for C and C++ programs"; From 168f304da69e892523151d3ccd8baefad5fede65 Mon Sep 17 00:00:00 2001 From: Sergei Zimmerman <145775305+xokdvium@users.noreply.github.com> Date: Mon, 6 Jan 2025 18:01:39 +0300 Subject: [PATCH 4/6] cbmc: 6.4.0 -> 6.4.1 --- pkgs/by-name/cb/cbmc/package.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pkgs/by-name/cb/cbmc/package.nix b/pkgs/by-name/cb/cbmc/package.nix index 87672e901312e..93f103c34134c 100644 --- a/pkgs/by-name/cb/cbmc/package.nix +++ b/pkgs/by-name/cb/cbmc/package.nix @@ -17,13 +17,13 @@ stdenv.mkDerivation (finalAttrs: { pname = "cbmc"; - version = "6.4.0"; + version = "6.4.1"; src = fetchFromGitHub { owner = "diffblue"; repo = "cbmc"; tag = "cbmc-${finalAttrs.version}"; - hash = "sha256-PZZnseOE3nodE0zwyG+82gm55BO4rsCcP4T+fZq7L6I="; + hash = "sha256-O8aZTW+Eylshl9bmm9GzbljWB0+cj2liZHs2uScERkM="; }; srcglucose = fetchFromGitHub { From 8d5481aecd86ebdbdc6dc1cfc44e8c933908ce5b Mon Sep 17 00:00:00 2001 From: Sergei Zimmerman <145775305+xokdvium@users.noreply.github.com> Date: Mon, 6 Jan 2025 22:11:05 +0300 Subject: [PATCH 5/6] cbmc: fix darwin, drop stale clags for gnu Apply portability patch for darwin (makes sense for linux as well). NIX_CFLAGS_COMPILE for GNU don't seem to be necessary anymore. --- pkgs/by-name/cb/cbmc/package.nix | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/pkgs/by-name/cb/cbmc/package.nix b/pkgs/by-name/cb/cbmc/package.nix index 93f103c34134c..70eb5fa01871a 100644 --- a/pkgs/by-name/cb/cbmc/package.nix +++ b/pkgs/by-name/cb/cbmc/package.nix @@ -13,6 +13,7 @@ substituteAll, cudd, nix-update-script, + fetchpatch, }: stdenv.mkDerivation (finalAttrs: { @@ -52,6 +53,12 @@ stdenv.mkDerivation (finalAttrs: { inherit cudd; }) ./0002-Do-not-download-sources-in-cmake.patch + # Fixes build with libc++ >= 19 due to the removal of std::char_traits. + # Remove for versions > 6.4.1. + (fetchpatch { + url = "https://github.com/diffblue/cbmc/commit/684bf4221c8737952e6469304f5a360dc3d5439d.patch"; + hash = "sha256-3hHu6FcyHjfeFjNxhyhxxk7I/SK98BXT+xy7NgtEt50="; + }) ]; postPatch = @@ -86,13 +93,13 @@ stdenv.mkDerivation (finalAttrs: { ''; env.NIX_CFLAGS_COMPILE = toString ( - lib.optionals stdenv.cc.isGNU [ - # Needed with GCC 12 but breaks on darwin (with clang) - "-Wno-error=maybe-uninitialized" - ] - ++ lib.optionals stdenv.cc.isClang [ + lib.optionals stdenv.cc.isClang [ # fix "argument unused during compilation" "-Wno-unused-command-line-argument" + # fix "variable 'plus_overflow' set but not used" + "-Wno-error=unused-but-set-variable" + # fix "passing no argument for the '...' parameter of a variadic macro is a C++20 extension" + "-Wno-error=c++20-extensions" ] ); From f75cb3c5d52a7cae7ad849660b495966bb07baac Mon Sep 17 00:00:00 2001 From: Sergei Zimmerman <145775305+xokdvium@users.noreply.github.com> Date: Wed, 8 Jan 2025 19:18:22 +0300 Subject: [PATCH 6/6] cbmc: use versionCheckHook instead of testers.testVersion There's no reason to use passthru.tests for this and manual recommends to do this by default. --- pkgs/by-name/cb/cbmc/package.nix | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/pkgs/by-name/cb/cbmc/package.nix b/pkgs/by-name/cb/cbmc/package.nix index 70eb5fa01871a..fe86380d9b6fc 100644 --- a/pkgs/by-name/cb/cbmc/package.nix +++ b/pkgs/by-name/cb/cbmc/package.nix @@ -2,10 +2,8 @@ lib, stdenv, fetchFromGitHub, - testers, bison, cadical, - cbmc, cmake, flex, makeWrapper, @@ -14,6 +12,7 @@ cudd, nix-update-script, fetchpatch, + versionCheckHook, }: stdenv.mkDerivation (finalAttrs: { @@ -109,10 +108,12 @@ stdenv.mkDerivation (finalAttrs: { "-Dsat_impl=cadical" ]; - passthru.tests.version = testers.testVersion { - package = cbmc; - command = "cbmc --version"; - }; + nativeInstallCheckInputs = [ + versionCheckHook + ]; + doInstallCheck = true; + versionCheckProgram = "${placeholder "out"}/bin/cbmc"; + versionCheckProgramArg = "--version"; passthru.updateScript = nix-update-script { extraArgs = [