Enable to type unit via ZeroSized

Author: coord-e

src/analyze/basic_block.rs

@@ -213,6 +213,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                     chc::Term::bool(val.try_to_bool().unwrap()),
                 )
             }
+            (mir_ty::TyKind::Tuple(tys), _) if tys.is_empty() => {
+                PlaceType::with_ty_and_term(rty::Type::unit(), chc::Term::tuple(vec![]))
+            }
+            (mir_ty::TyKind::Closure(_, args), _) if args.as_closure().upvar_tys().is_empty() => {
+                PlaceType::with_ty_and_term(rty::Type::unit(), chc::Term::tuple(vec![]))
+            }
             (
                 mir_ty::TyKind::Ref(_, elem, Mutability::Not),
                 ConstValue::Scalar(Scalar::Ptr(ptr, _)),

tests/ui/fail/closure_mut_0.rs

@@ -0,0 +1,12 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut x = 1;
+    x += 1;
+    let mut incr = || {
+        x += 1;
+    };
+    incr();
+    assert!(x == 2);
+}

tests/ui/fail/closure_param.rs

@@ -0,0 +1,14 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+fn take_fn<T, F: Fn(i32) -> T>(f: F) -> T {
+    f(42)
+}
+
+fn main() {
+    let y = take_fn(|x| {
+        assert!(x == 41);
+        x + 1
+    });
+    assert!(y == 42);
+}

tests/ui/pass/closure_mut_0.rs

@@ -0,0 +1,11 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn main() {
+    let mut x = 1;
+    let mut incr = || {
+        x += 1;
+    };
+    incr();
+    assert!(x == 2);
+}

tests/ui/pass/closure_param.rs

@@ -0,0 +1,14 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+fn take_fn<T, F: Fn(i32) -> T>(f: F) -> T {
+    f(41)
+}
+
+fn main() {
+    let y = take_fn(|x| {
+        assert!(x == 41);
+        x + 1
+    });
+    assert!(y == 42);
+}