Basic fix for model-checking#2121

JustusAdam · Jun 1, 2023 · 5226169 · 5226169
1 parent caec631
commit 5226169
Showing 1 changed file with 12 additions and 1 deletion.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -15,6 +15,7 @@ use rustc_middle::ty::{Instance, InstanceDef};
 use rustc_span::Span;
 use tracing::debug;
 
+
 struct SizeAlign {
     size: Expr,
     align: Expr,
@@ -445,7 +446,17 @@ impl<'tcx> GotocCtx<'tcx> {
             "cosf64" => codegen_simple_intrinsic!(Cos),
             "ctlz" => codegen_count_intrinsic!(ctlz, true),
             "ctlz_nonzero" => codegen_count_intrinsic!(ctlz, false),
-            "ctpop" => self.codegen_expr_to_place(p, fargs.remove(0).popcount()),
+            "ctpop" => {
+                let arg = fargs.remove(0);
+                let atype = arg.typ();
+                if !atype.is_integer() {
+                    self.tcx.sess.span_err(span.into_iter().collect::<Vec<_>>(), format!("Type Check Failure: Expected integer type for call to `ctpop`, found {atype:?}"));
+                    Stmt::skip(loc)
+                } else {
+
+                    self.codegen_expr_to_place(p, arg.popcount())
+                }
+            }
             "cttz" => codegen_count_intrinsic!(cttz, true),
             "cttz_nonzero" => codegen_count_intrinsic!(cttz, false),
             "discriminant_value" => {