(c2rust-analyze) Move and fully implement the post-typeck const ref permission check.

Author: kkysen

c2rust-analyze/src/dataflow/type_check.rs

@@ -489,11 +489,5 @@ pub fn visit<'tcx>(
         );
     }
 
-    for (&constant, const_lty) in &acx.const_ref_tys {
-        let _ptr_id = const_lty.label;
-        let _expected_perms = PermissionSet::for_const(constant);
-        // TODO: check that perms match the expected ones
-    }
-
     (tc.constraints, tc.equiv_constraints)
 }

c2rust-analyze/src/main.rs

@@ -625,6 +625,13 @@ fn run(tcx: TyCtxt) {
         let mut asn = gasn.and(&mut info.lasn);
         info.dataflow.propagate_cell(&mut asn);
 
+        for (&constant, const_lty) in &acx.const_ref_tys {
+            let ptr_id = const_lty.label;
+            let expected_perms = PermissionSet::for_const(constant);
+            let actual_perms = asn.perms()[ptr_id];
+            assert_eq!(expected_perms, actual_perms);
+        }
+
         // Print labeling and rewrites for the current function.
 
         eprintln!("\nfinal labeling for {:?}:", name);