Merge pull request #763 from Nadrieril/version

Add `charon version`

Author: Nadrieril

charon/src/ast/types_utils.rs

@@ -428,25 +428,6 @@ impl IntegerTy {
         !(self.is_signed())
     }
 
-    /// Return the size (in bytes) of an integer of the proper type
-    pub fn size(&self) -> usize {
-        use std::mem::size_of;
-        match self {
-            IntegerTy::Isize => size_of::<isize>(),
-            IntegerTy::I8 => size_of::<i8>(),
-            IntegerTy::I16 => size_of::<i16>(),
-            IntegerTy::I32 => size_of::<i32>(),
-            IntegerTy::I64 => size_of::<i64>(),
-            IntegerTy::I128 => size_of::<i128>(),
-            IntegerTy::Usize => size_of::<isize>(),
-            IntegerTy::U8 => size_of::<u8>(),
-            IntegerTy::U16 => size_of::<u16>(),
-            IntegerTy::U32 => size_of::<u32>(),
-            IntegerTy::U64 => size_of::<u64>(),
-            IntegerTy::U128 => size_of::<u128>(),
-        }
-    }
-
     pub fn to_unsigned(&self) -> Self {
         match self {
             IntegerTy::Isize => IntegerTy::Usize,

charon/src/bin/charon-driver/translate/translate_types.rs

@@ -485,10 +485,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
                         None
                     } else {
                         tcx.tag_for_variant(ty_env.as_query_input((ty, id)))
-                            .map(|s| {
-                                assert_eq!(s.size(), r_abi::Size::from_bytes(tag_ty.size()));
-                                ScalarValue::from_bits(tag_ty, s.to_bits(s.size()))
-                            })
+                            .map(|s| ScalarValue::from_bits(tag_ty, s.to_bits(s.size())))
                     };
                     variant_layouts.push(translate_variant_layout(variant_layout, tag));
                 }

charon/src/bin/charon/cli.rs

@@ -24,6 +24,8 @@ pub enum Charon {
     ToolchainPath(ToolchainPathArgs),
     /// Pretty-print the given llbc file.
     PrettyPrint(PrettyPrintArgs),
+    /// Print the version.
+    Version,
 }
 
 /// Read a llbc or ullbc file and pretty print it.

charon/src/bin/charon/main.rs

@@ -79,6 +79,10 @@ pub fn main() -> Result<()> {
             println!("{}", path.display());
             ExitStatus::default()
         }
+        Some(Charon::Version) => {
+            println!("{}", charon_lib::VERSION);
+            ExitStatus::default()
+        }
         // Legacy calling syntax.
         None => {
             let options = cli.opts;

charon/src/lib.rs

@@ -44,7 +44,7 @@ pub use pretty::formatter;
 pub use transform::{graphs, reorder_decls, ullbc_to_llbc};
 
 /// The version of the crate, as defined in `Cargo.toml`.
-const VERSION: &str = env!("CARGO_PKG_VERSION");
+pub const VERSION: &str = env!("CARGO_PKG_VERSION");
 
 /// Read a `.llbc` file.
 pub fn deserialize_llbc(path: &std::path::Path) -> anyhow::Result<ast::TranslatedCrate> {

charon/tests/cli.rs

@@ -48,6 +48,18 @@ fn charon_pretty_print() -> Result<()> {
     )
 }
 
+#[test]
+fn charon_version() -> Result<()> {
+    charon(&["version"], ".", |stdout, cmd| {
+        let version = charon_lib::VERSION;
+        ensure!(
+            stdout.trim() == version,
+            "Output of `{cmd}` is:\n{stdout:?}\nIt should be {version}."
+        );
+        Ok(())
+    })
+}
+
 #[test]
 fn charon_cargo_p_crate2() -> Result<()> {
     charon(