From 366f071c874834f51fdae58aaba0faee1349fb52 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 11 Dec 2024 20:30:00 -0800
Subject: [PATCH] ok to NOT have const-attr/info for integral consts

---
 crates/flux-desugar/src/resolver.rs     | 14 ++++++++------
 crates/flux-driver/src/collector/mod.rs |  8 +++-----
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/crates/flux-desugar/src/resolver.rs b/crates/flux-desugar/src/resolver.rs
index b3188b70f4..15c7832c93 100644
--- a/crates/flux-desugar/src/resolver.rs
+++ b/crates/flux-desugar/src/resolver.rs
@@ -251,13 +251,15 @@ impl<'genv, 'tcx> CrateResolver<'genv, 'tcx> {
     }
 
     fn resolve_constant(&mut self, owner_id: MaybeExternId<OwnerId>) -> Result {
-        let constant = &self.specs.constants[&owner_id.local_id()];
-        ItemResolver::run(self, owner_id, |item_resolver| {
-            item_resolver.visit_constant(constant);
-        })?;
-        RefinementResolver::resolve_constant(self, constant)
+        if let Some(constant) = self.specs.constants.get(&owner_id.local_id()) {
+            ItemResolver::run(self, owner_id, |item_resolver| {
+                item_resolver.visit_constant(constant);
+            })?;
+            RefinementResolver::resolve_constant(self, constant)?;
+        }
+        Ok(())
     }
-    
+
     fn resolve_fn_sig(&mut self, owner_id: MaybeExternId<OwnerId>) -> Result {
         if let Some(fn_sig) = &self.specs.fn_sigs[&owner_id.local_id()].fn_sig {
             ItemResolver::run(self, owner_id, |item_resolver| {
diff --git a/crates/flux-driver/src/collector/mod.rs b/crates/flux-driver/src/collector/mod.rs
index 150b443aa5..eacbbf248a 100644
--- a/crates/flux-driver/src/collector/mod.rs
+++ b/crates/flux-driver/src/collector/mod.rs
@@ -239,11 +239,9 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
     }
 
     fn parse_constant_spec(&mut self, owner_id: OwnerId, mut attrs: FluxAttrs) -> Result {
-        let span = self.tcx.source_span(owner_id);
-        let constant = attrs
-            .constant()
-            .ok_or_else(|| self.errors.emit(errors::InvalidAttr { span }))?;
-        self.specs.constants.insert(owner_id, constant);
+        if let Some(constant) = attrs.constant() {
+            self.specs.constants.insert(owner_id, constant);
+        }
         Ok(())
     }