Use mangled name for intrinsic symbols

src/printer.rs

@@ -412,8 +412,8 @@ fn fn_inst_sym<'tcx>(
             let internal_inst = rustc_internal::internal(tcx, inst);
             let sym_type = if inst.is_empty_shim() {
                 NoOpSym(String::from(""))
-            } else if let Some(intrinsic_name) = inst.intrinsic_name() {
-                IntrinsicSym(intrinsic_name)
+            } else if let Some(_intrinsic_name) = inst.intrinsic_name() {
+                IntrinsicSym(inst.mangled_name())
             } else {
                 NormalSym(inst.mangled_name())
             };

tests/integration/programs/assert_eq.smir.json.expected

@@ -23,7 +23,7 @@
     ],
     [
       {
-        "IntrinsicSym": "black_box"
+        "IntrinsicSym": "_ZN4core10intrinsics9black_box17h422cafb34137ccebE"
       }
     ],
     [

tests/integration/programs/binop.smir.json.expected

@@ -1127,7 +1127,7 @@
     ],
     [
       {
-        "IntrinsicSym": "black_box"
+        "IntrinsicSym": "_ZN4core10intrinsics9black_box17h241585995e0a474bE"
       }
     ],
     [

tests/integration/programs/char-trivial.smir.json.expected

@@ -63,7 +63,7 @@
     ],
     [
       {
-        "IntrinsicSym": "black_box"
+        "IntrinsicSym": "_ZN4core10intrinsics9black_box17ha16ea91007d49fe5E"
       }
     ],
     [

tests/integration/programs/checked_arithmetic.rs

@@ -0,0 +1,21 @@
+fn main() {
+    checked_add_i32(1,2);
+}
+
+/// If the precondition is not met, the program is not executed (exits cleanly, ex falso quodlibet)
+macro_rules! precondition {
+    ($pre:expr, $block:expr) => {
+        if $pre { $block }
+    };
+}
+
+fn checked_add_i32(a: i32, b: i32) {
+
+    precondition!(
+        a.checked_add(b).is_some(),
+         unsafe {
+            let result = a.unchecked_add(b);
+            assert!(result as i64 == a as i64 + b as i64)
+        }
+    );
+}