Update to CBMC version 6.0.0

Updates to match changes to the GOTO binary format.

Resolves: model-checking#2972

cprover_bindings/src/irep/goto_binary_serde.rs

@@ -11,7 +11,7 @@ use std::io::{self, BufReader};
 use std::io::{BufWriter, Bytes, Error, ErrorKind, Read, Write};
 use std::path::Path;
 
-/// Writes a symbol table to a file in goto binary format in version 5.
+/// Writes a symbol table to a file in goto binary format in version 6.
 ///
 /// In CBMC, the serialization rules are defined in :
 /// - src/goto-programs/write_goto_binary.h
@@ -26,7 +26,7 @@ pub fn write_goto_binary_file(filename: &Path, source: &crate::goto_program::Sym
     serializer.write_file(irep_symbol_table);
 }
 
-/// Reads a symbol table from a file expected to be in goto binary format in version 5.
+/// Reads a symbol table from a file expected to be in goto binary format in version 6.
 //
 /// In CBMC, the deserialization rules are defined in :
 /// - src/goto-programs/read_goto_binary.h
@@ -542,7 +542,7 @@ where
         assert!(written == 4);
 
         // Write goto binary version
-        self.write_usize_varenc(5);
+        self.write_usize_varenc(6);
     }
 
     /// Writes the symbol table using the GOTO binary file format to the byte stream.
@@ -923,12 +923,12 @@ where
 
         // Read goto binary version
         let goto_binary_version = self.read_usize_varenc()?;
-        if goto_binary_version != 5 {
+        if goto_binary_version != 6 {
             return Err(Error::new(
                 ErrorKind::Other,
                 format!(
                     "Unsupported GOTO binary version: {}. Supported version: {}",
-                    goto_binary_version, 5
+                    goto_binary_version, 6
                 ),
             ));
         }

cprover_bindings/src/irep/irep_id.rs

@@ -362,7 +362,7 @@ pub enum IrepId {
     Div,
     Power,
     FactorialPower,
-    PrettyName,
+    CPrettyName,
     CClass,
     CField,
     CInterface,
@@ -1232,7 +1232,7 @@ impl ToString for IrepId {
             IrepId::Div => "/",
             IrepId::Power => "**",
             IrepId::FactorialPower => "factorial_power",
-            IrepId::PrettyName => "pretty_name",
+            IrepId::CPrettyName => "#pretty_name",
             IrepId::CClass => "#class",
             IrepId::CField => "#field",
             IrepId::CInterface => "#interface",

cprover_bindings/src/irep/to_irep.rs

@@ -132,7 +132,7 @@ impl ToIrep for DatatypeComponent {
         match self {
             DatatypeComponent::Field { name, typ } => Irep::just_named_sub(linear_map![
                 (IrepId::Name, Irep::just_string_id(name.to_string())),
-                (IrepId::PrettyName, Irep::just_string_id(name.to_string())),
+                (IrepId::CPrettyName, Irep::just_string_id(name.to_string())),
                 (IrepId::Type, typ.to_irep(mm)),
             ]),
             DatatypeComponent::Padding { name, bits } => Irep::just_named_sub(linear_map![

kani-dependencies

@@ -1,6 +1,6 @@
-CBMC_MAJOR="5"
-CBMC_MINOR="95"
-CBMC_VERSION="5.95.1"
+CBMC_MAJOR="6"
+CBMC_MINOR="0"
+CBMC_VERSION="6.0.0"
 
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_MAJOR="3"