Keep an enum constant a contract still names

cpp/impl.cpp

@@ -1891,8 +1891,20 @@ class PALConsumer : public ASTConsumer {
 
       // Evaluate scrutinee
       auto scrutRval = trRValue(sw->getCond());
-      auto scrutTy =
-          trQualType(sw->getCond()->getType(), sw->getCond()->getSourceRange());
+      // Clang applies the integral promotions to the switch condition. An
+      // enumeration is modeled by its underlying integer type, so that
+      // promotion translates to the identity and is elided from the rvalue.
+      // Annotating the binding with the promoted type would then leave the
+      // declared type and the translated value syntactically distinct, which
+      // the Pulse dereference tactic rejects. Use the enumeration's own type
+      // so the two agree; other promotions are genuine casts that trRValue
+      // preserves, so their promoted type remains correct.
+      auto *scrutExpr = sw->getCond();
+      auto scrutQualTy = scrutExpr->getType();
+      if (scrutExpr->IgnoreImpCasts()->getType()->isEnumeralType()) {
+        scrutQualTy = scrutExpr->IgnoreImpCasts()->getType();
+      }
+      auto scrutTy = trQualType(scrutQualTy, scrutExpr->getSourceRange());
 
       // Bind the scrutinee once as an immutable value.
       static int switchCounter = 0;

src/pass/prune.rs

@@ -154,7 +154,12 @@ fn scan_inline_pulse_code(deps: &mut HashSet<DeclName>, code: &InlinePulseCode)
 
 fn scan_expr(deps: &mut HashSet<DeclName>, rv: &Expr) {
     match &rv.val {
-        ExprT::Var(_) => {}
+        // A bare name may refer to a global (an enum constant, say). Locals share the namespace,
+        // so this over-approximates -- which is the safe direction for a pruner: it can keep a
+        // declaration that is not needed, but must never drop one that is.
+        ExprT::Var(n) => {
+            deps.insert(DeclName::GlobalVar(n.val.clone()));
+        }
         ExprT::Deref(v) => scan_expr(deps, v),
         ExprT::Member(x, _a) => scan_expr(deps, x),
         ExprT::VAttr(_, x) => scan_expr(deps, x),

test/enum_const_in_contract/Makefile

@@ -0,0 +1 @@
+../_templates/Makefile

test/enum_const_in_contract/colors.h

@@ -0,0 +1,20 @@
+#pragma once
+#include "pal.h"
+
+// These enumerators live in a header, so the pruner sees them as non-root
+// declarations. The contract below is their only reference: the body uses a
+// switch, whose case labels the C frontend folds to integer constants.
+typedef enum _COLOR
+{
+    Color_Red = 0,
+    Color_Green = 1,
+    Color_Blue = 2,
+} COLOR;
+
+_Bool
+color_is_known(COLOR c)
+    _ensures(return == (c == Color_Red || c == Color_Green || c == Color_Blue));
+
+COLOR
+color_default(void)
+    _ensures(return == Color_Green);

test/enum_const_in_contract/enum_const_in_contract.c

@@ -0,0 +1,26 @@
+#include "colors.h"
+
+_Bool
+color_is_known(COLOR c)
+{
+    _Bool known = 0;
+
+    switch (c)
+    {
+    case Color_Red:
+    case Color_Green:
+    case Color_Blue:
+        known = 1;
+        break;
+    default:
+        break;
+    }
+
+    return known;
+}
+
+COLOR
+color_default(void)
+{
+    return Color_Green;
+}

test/enum_const_in_contract/fstar.fst.config.json

@@ -0,0 +1 @@
+../_templates/fstar.fst.config.json

test/enum_const_in_contract/pal.config.json

@@ -0,0 +1 @@
+../_templates/pal.config.json

test/enum_const_in_contract/pal.h

@@ -0,0 +1 @@
+../pal.h