Bump CBMC version to 5.59.0 (rust-lang#1270)

* Enable `maxnumf32` test

* Bump CBMC version to 5.59.0

* Change expected output for failing tests and link issue

Author: adpaco-aws

docs/src/install-guide.md

@@ -37,7 +37,7 @@ In general, the following dependencies are required.
 > OS.
 
 1. Cargo installed via [rustup](https://rustup.rs/)
-2. [CBMC](https://github.com/diffblue/cbmc) (>= 5.58.1)
+2. [CBMC](https://github.com/diffblue/cbmc) (>= 5.59.0)
 3. [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc) (>= 2.10)
 
 Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms.

scripts/kani-regression.sh

@@ -19,7 +19,7 @@ KANI_DIR=$SCRIPT_DIR/..
 export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true"
 
 # Required dependencies
-check-cbmc-version.py --major 5 --minor 58
+check-cbmc-version.py --major 5 --minor 59
 check-cbmc-viewer-version.py --major 2 --minor 10
 
 # Formatting check

scripts/setup/ubuntu/install_cbmc.sh

@@ -5,7 +5,7 @@
 set -eu
 
 UBUNTU_VERSION=$(lsb_release -rs)
-CBMC_VERSION=5.58.1
+CBMC_VERSION=5.59.0
 FILE="ubuntu-${UBUNTU_VERSION}-cbmc-${CBMC_VERSION}-Linux.deb"
 URL="https://github.com/diffblue/cbmc/releases/download/cbmc-${CBMC_VERSION}/$FILE"
 

tests/kani/Intrinsics/MaxNum/maxnumf32_fixme.rs renamed to tests/kani/Intrinsics/MaxNum/maxnumf32.rs

@@ -7,18 +7,6 @@
 //  * If both arguments are NaN, NaN is returned.
 #![feature(core_intrinsics)]
 
-// Note: All test cases are failing with the following error:
-// ```
-// Check X: fmaxf.assertion.1
-//          - Status: FAILURE
-//          - Description: "Function with missing definition is unreachable"
-//          - Location: <builtin-library-fmaxf> in function fmaxf
-// ```
-// This is because the `fmaxf` definition is not being found, either because
-// Kani does not produce the right expression (which is strange, because it's
-// doing the same for similar expressions and they work) or CBMC is not picking
-// it for some reason.
-// Tracked in https://github.com/model-checking/kani/issues/1025
 #[kani::proof]
 fn test_general() {
     let x: f32 = kani::any();

tests/ui/missing-function/extern_c/expected

@@ -1,4 +1,4 @@
-Status: UNDETERMINED\
+Status: UNREACHABLE\
 Description: "assertion failed: x == 5"
 
 VERIFICATION:- FAILED

tests/ui/missing-function/extern_c/extern_c.rs

@@ -7,7 +7,8 @@
 // TODO: Verify that this prints a compiler warning:
 //  - https://github.com/model-checking/kani/issues/576
 
-
+// TODO: Missing functions produce non-informative property descriptions
+// https://github.com/model-checking/kani/issues/1271
 extern "C" {
     fn missing_function() -> u32;
 }

tests/ui/missing-function/replaced-description/expected

@@ -1,3 +1,2 @@
-.assertion.1\
 Status: FAILURE\
-Description: "Function with missing definition is unreachable"
+Description: "assertion"

tests/ui/missing-function/replaced-description/main.rs

@@ -3,6 +3,8 @@
 
 // This test is to check if the description for undefined functions has been updated to "Function with missing definition is unreachable"
 
+// TODO: Missing functions produce non-informative property descriptions
+// https://github.com/model-checking/kani/issues/1271
 #[kani::proof]
 fn main() {
     let x = String::from("foo");

tests/ui/missing-function/rust-by-example-description/expected

@@ -1,3 +1,2 @@
-.assertion.1\
 Status: FAILURE\
-Description: "Function with missing definition is unreachable"
+Description: "assertion"

tests/ui/missing-function/rust-by-example-description/main.rs

@@ -4,6 +4,8 @@
 // kani-flags: --enable-unstable --cbmc-args --unwind 4 --object-bits 9
 // This test is to check if the description for undefined functions has been updated to "Function with missing definition is unreachable"
 
+// TODO: Missing functions produce non-informative property descriptions
+// https://github.com/model-checking/kani/issues/1271
 #![allow(unused)]
 #[kani::proof]
 pub fn main() {