Slice.length

creusot-rs · Nov 29, 2024 · d90784e · d90784e
1 parent 60d4c77
commit d90784e
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 3 deletions.
diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs
@@ -1,4 +1,4 @@
-use self::ty::{concret_intty, concret_uintty, slice_create_qname};
+use self::ty::{concret_intty, concret_uintty, slice_create_qname, slice_length_qname};
 
 use crate::{
     backend::{
@@ -337,7 +337,7 @@ impl<'tcx> RValue<'tcx> {
                     // right operand must be converted to integer
                     BinOp::Shl | BinOp::ShlUnchecked | BinOp::Shr | BinOp::ShrUnchecked => {
                         let r_ty = r.ty(lower.ctx.tcx, lower.locals);
-
+                        
                         // rust allows shifting by a value of any integer type
                         // so we need to import the prelude for the right operand
                         let prelude: PreludeModule = match r_ty.kind() {
@@ -492,7 +492,7 @@ impl<'tcx> RValue<'tcx> {
             }
             RValue::Len(pl) => {
                 let len_call =
-                    Exp::qvar(QName::from_string("Slice.length")).app_to(pl.to_why(lower, istmts));
+                    Exp::qvar(slice_length_qname()).app_to(pl.to_why(lower, istmts));
                 len_call
             }
             RValue::Array(fields) => {

diff --git a/creusot/src/backend/ty.rs b/creusot/src/backend/ty.rs
@@ -574,4 +574,13 @@ pub(crate) fn slice_set_qname() -> QName {
     return QName::from_string("Slice32.set");
     #[cfg(target_pointer_width = "16")]
     return QName::from_string("Slice16.set");
+}
+
+pub(crate) fn slice_length_qname() -> QName {
+    #[cfg(target_pointer_width = "64")]
+    return QName::from_string("Slice64.length");
+    #[cfg(target_pointer_width = "32")]
+    return QName::from_string("Slice32.length");
+    #[cfg(target_pointer_width = "16")]
+    return QName::from_string("Slice16.length");
 }