Let a switch arm end in a jump or an abort by nikswamy · Pull Request #235 · FStarLang/pal

nikswamy · 2026-08-19T04:10:07Z

Part of the upstreaming of nswamy/pal-c-project-integration (PR21 of 35 PRs) — see PR_PLAN.md on that branch for the whole plan and the dependency graph.

Base: nswamy/pal-pr20-switch-default-and-if-chain — a stacked PR. It depends on nswamy/pal-pr20-switch-default-and-if-chain, nswamy/pal-pr18-unreachable, so only the commits listed below are its own; it will be retargeted at main once its parents land.

It has more than one parent, so the diff against nswamy/pal-pr20-switch-default-and-if-chain also carries the commits from nswamy/pal-pr18-unreachable until those land.

The ordinary shape of a version dispatcher: two live arms and a default that raises a
fatal error and jumps to the function's single exit. An arm was taken to have no
fall-through only when it ended in a direct break, so an arm leaving by return, by a
goto out of the switch, or by a noreturn abort forced the general encoding. All three
are now admitted; abortsControlFlow propagates the claim the way control flow does (a
block aborts if any statement does, a do-while(0) wrapper if its body does, an if if
both arms do or its condition folds). This also needs the goto restructuring to look
inside match branches, which it did not. Separately, do { ... } while (0) is not a
loop — it is the single-statement-body idiom — and encoding it as one lost everything the
body established, including the claim that it cannot be reached at all.

Commits

Let a switch arm end in a jump, and stop encoding do-while(0) as a loop
Let a switch arm end in an abort with no jump after it

Testing

Verified: make rust lib, test/check-template.sh, cargo fmt --check, clang-format --dry-run --Werror, and F* verification of test/builtin_unreachable, test/switch_stmt.

An `_assert(false)` in a dead `default:` arm is a claim that control never reaches that point, not a proposition to carry forward. PAL emitted `assert (with_pure (0 <> 0))`, which is a proof obligation, so the arm kept its own resource footprint and the enclosing conditional's join came out as a `match` on the scrutinee that the frame prover could not reduce: - Cannot prove: match view.version = 1ul with | true -> ...union unfolded at the selected member... | false -> ...union still folded... An unreachable arm was thus the reason a proof failed. Recognize a condition that is syntactically `0` or `false` through any casts -- assertion bodies are C-preprocessed, so a source `false` is already a literal by the time PAL sees it -- and emit Pulse's `unreachable ()`. Its postcondition is `pure False`, so the arm absorbs whatever the join needs, and the obligation becomes the right one: prove the arm is dead, which follows from the negated branch condition. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 09b6b9e)

It is how a noreturn abort is spelled to the C compiler, and code that ends a switch's default arm with one relies on it: without it the compiler reports the fall-through as a use of an uninitialized variable, so a function whose default arm is dead cannot be translated at all. Pulse spells the same claim 'unreachable ()', which PAL already emits for _assert(false), so a call to the builtin is rewritten to exactly that. The claim is discharged rather than assumed: an arm PAL cannot show is dead is an error, which is the point. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit a88a3cd)

…h-jump-abort

Two encodings stood between the translator and the ordinary shape of a version dispatcher: a switch with two live arms and a default arm that raises a fatal error and jumps to the function's single exit. The switch encoding took an arm to have no fall-through only when it ended in a direct break, so an arm that leaves by 'return' or by a 'goto' out of the switch forced the general encoding, whose hit and break flags turn every case test into a compound condition over mutable state. The prover then cannot reduce the join, and the arms' postconditions are unusable. An arm that jumps away has nothing to fall through to either, so admit those as well; the statement stays where a terminal break is dropped. That in turn needs the goto restructuring to look inside match branches, which it did not, so a 'goto' from an arm left the label unbound. Separately, 'do { ... } while (0)' is not a loop; it is the idiom that gives a macro a single-statement body. Encoding it as one loses everything the body established, because a loop's postcondition is its invariant -- including the claim that it cannot be reached at all, which is exactly what an aborting macro makes. Emit the body where nothing in it breaks or continues out. The new test is the dispatcher itself: a default arm that asserts false inside the do-while wrapper and jumps to the exit. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit f9e2cdf)

An arm whose last statement is a noreturn abort does not fall through, and that is what makes the C legal: without the abort the compiler reports the fall-through as a use of an uninitialized variable. The fall-through check was syntactic -- break, return or goto -- so it did not agree, and forced the general hit/brk switch encoding, whose compound branch guard nothing can be proved under. Recognize the abort directly. abortsControlFlow is true for a call to __builtin_unreachable and propagates the claim the way control flow does: a block aborts if any statement does, a do-while(0) wrapper aborts if its body does, and an if aborts if both arms do or if its condition folds to a constant selecting an arm that does -- the shape '_assert(e); if (!(e)) __builtin_unreachable();' takes when e is literally false. The claim is still discharged, never assumed. dispatch_abort_no_jump in test/builtin_unreachable covers it. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 459eb94)

gebner · 2026-08-26T21:13:01Z

!diff

github-actions · 2026-08-26T21:34:24Z

Generated F* output diff

Effect of this pull request on the F* code pal generates for the test suite (d3123dc → 9b48cec).

Summary

 /dev/null => head/builtin_unreachable/Func_dispatch.fst                | 44 ++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/builtin_unreachable/Func_dispatch.fsti               | 13 +++++++++++++
 /dev/null => head/builtin_unreachable/Func_dispatch_abort_no_jump.fst  | 34 ++++++++++++++++++++++++++++++++++
 /dev/null => head/builtin_unreachable/Func_dispatch_abort_no_jump.fsti | 12 ++++++++++++
 /dev/null => head/builtin_unreachable/Func_halve.fst                   | 20 ++++++++++++++++++++
 /dev/null => head/builtin_unreachable/Func_halve.fsti                  | 11 +++++++++++
 /dev/null => head/builtin_unreachable/Func_pick.fst                    | 28 ++++++++++++++++++++++++++++
 /dev/null => head/builtin_unreachable/Func_pick.fsti                   | 12 ++++++++++++
 /dev/null => head/builtin_unreachable/TranslationErrors.fst            |  1 +
 /dev/null => head/builtin_unreachable/Typedef___int32_t.fst            | 12 ++++++++++++
 /dev/null => head/builtin_unreachable/Typedef___uint32_t.fst           | 13 +++++++++++++
 /dev/null => head/builtin_unreachable/Typedef_int32_t.fst              | 13 +++++++++++++
 /dev/null => head/builtin_unreachable/Typedef_uint32_t.fst             | 13 +++++++++++++
 /dev/null => head/builtin_unreachable/diagnostics.json                 |  1 +
 {base => head}/character_literals/Func_classify_char.fst               | 32 ++++++++++++--------------------
 {base => head}/do_while/Func_find_limit.fst                            | 12 ++++++------
 {base => head}/do_while/Func_nested_continue.fst                       | 12 ++++++------
 {base => head}/do_while/Func_run_once.fst                              | 15 +--------------
 {base => head}/switch_stmt/Func_classify_with_returns.fst              | 14 ++++----------
 19 files changed, 256 insertions(+), 56 deletions(-)

Full diff: full diff artifact

Diff

diff --git head/builtin_unreachable/Func_dispatch.fst head/builtin_unreachable/Func_dispatch.fst
new file mode 100644
index 0000000..0f85d60
--- /dev/null
+++ head/builtin_unreachable/Func_dispatch.fst
@@ -0,0 +1,44 @@
+module Func_dispatch
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_dispatch (var_version: Typedef_uint32_t.ty_uint32_t)
+  requires ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+  requires
+    (with_pure (((id #int (UInt32.v var_version)) = 1) || ((id #int (UInt32.v var_version)) = 2)))
+  returns return_1 : Typedef_int32_t.ty_int32_t
+  ensures ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+  ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+  ensures (with_pure (((id #int (Int32.v return_1)) = 10) || ((id #int (Int32.v return_1)) = 20)))
+{
+  let mut var_version = var_version;
+  let mut var_result : Typedef_int32_t.ty_int32_t;
+  let var___switch_scrut_1 : Typedef_uint32_t.ty_uint32_t = (!var_version);
+  {
+    {
+      match (var___switch_scrut_1) {
+          1ul -> {
+            var_result := 10l;
+          }
+          2ul -> {
+            var_result := 20l;
+          }
+        _ -> {
+          unreachable ();
+          unreachable ();
+          goto var_finally;
+        }
+      };
+    }
+    ensures (((live var_version) ** (live var_result)) **
+      (with_pure
+        (((id #int (Int32.v (!var_result))) = 10) || ((id #int (Int32.v (!var_result))) = 20))))
+    label __pal_match_join_0:;
+  }
+  ensures (((live var_version) ** (live var_result)) **
+    (with_pure
+      (((id #int (Int32.v (!var_result))) = 10) || ((id #int (Int32.v (!var_result))) = 20))))
+  label var_finally:;
+  return (!var_result);
+}
\ No newline at end of file
diff --git head/builtin_unreachable/Func_dispatch.fsti head/builtin_unreachable/Func_dispatch.fsti
new file mode 100644
index 0000000..fa42521
--- /dev/null
+++ head/builtin_unreachable/Func_dispatch.fsti
@@ -0,0 +1,13 @@
+module Func_dispatch
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_dispatch (var_version: Typedef_uint32_t.ty_uint32_t)
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+requires
+  (with_pure (((id #int (UInt32.v var_version)) = 1) || ((id #int (UInt32.v var_version)) = 2)))
+returns return_1 : Typedef_int32_t.ty_int32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+ensures (with_pure (((id #int (Int32.v return_1)) = 10) || ((id #int (Int32.v return_1)) = 20)))
\ No newline at end of file
diff --git head/builtin_unreachable/Func_dispatch_abort_no_jump.fst head/builtin_unreachable/Func_dispatch_abort_no_jump.fst
new file mode 100644
index 0000000..b3b528d
--- /dev/null
+++ head/builtin_unreachable/Func_dispatch_abort_no_jump.fst
@@ -0,0 +1,34 @@
+module Func_dispatch_abort_no_jump
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_dispatch_abort_no_jump (var_version: Typedef_uint32_t.ty_uint32_t)
+  requires ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+  requires (with_pure ((id #int (UInt32.v var_version)) = 2))
+  returns return_1 : Typedef_int32_t.ty_int32_t
+  ensures ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+  ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+  ensures (with_pure ((id #int (Int32.v return_1)) = 20))
+{
+  let mut var_version = var_version;
+  let mut var_result : Typedef_int32_t.ty_int32_t;
+  let var___switch_scrut_2 : Typedef_uint32_t.ty_uint32_t = (!var_version);
+  {
+    match (var___switch_scrut_2) {
+        2ul -> {
+          var_result := 20l;
+        }
+      _ -> {
+        unreachable ();
+        if ((not (int32_to_bool 0l))) {
+          unreachable ();
+        } else {};
+      }
+    };
+  }
+  ensures (((live var_version) ** (live var_result)) **
+    (with_pure ((id #int (Int32.v (!var_result))) = 20)))
+  label __pal_match_join_1:;
+  return (!var_result);
+}
\ No newline at end of file
diff --git head/builtin_unreachable/Func_dispatch_abort_no_jump.fsti head/builtin_unreachable/Func_dispatch_abort_no_jump.fsti
new file mode 100644
index 0000000..820b5db
--- /dev/null
+++ head/builtin_unreachable/Func_dispatch_abort_no_jump.fsti
@@ -0,0 +1,12 @@
+module Func_dispatch_abort_no_jump
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_dispatch_abort_no_jump (var_version: Typedef_uint32_t.ty_uint32_t)
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+requires (with_pure ((id #int (UInt32.v var_version)) = 2))
+returns return_1 : Typedef_int32_t.ty_int32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+ensures (with_pure ((id #int (Int32.v return_1)) = 20))
\ No newline at end of file
diff --git head/builtin_unreachable/Func_halve.fst head/builtin_unreachable/Func_halve.fst
new file mode 100644
index 0000000..a2ba161
--- /dev/null
+++ head/builtin_unreachable/Func_halve.fst
@@ -0,0 +1,20 @@
+module Func_halve
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_halve (var_n: Typedef_uint32_t.ty_uint32_t)
+  requires ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+  requires (with_pure (((id #int (UInt32.v var_n)) % 2) = 0))
+  returns return_1 : Typedef_uint32_t.ty_uint32_t
+  ensures ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+  ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+  let mut var_n = var_n;
+  if ((not
+        (((!var_n) `UInt32.rem` (id #UInt32.t (Int.Cast.int32_to_uint32 2l))) =
+          (id #UInt32.t (Int.Cast.int32_to_uint32 0l))))) {
+    unreachable ();
+  } else {};
+  return ((!var_n) `UInt32.div` (id #UInt32.t (Int.Cast.int32_to_uint32 2l)));
+}
\ No newline at end of file
diff --git head/builtin_unreachable/Func_halve.fsti head/builtin_unreachable/Func_halve.fsti
new file mode 100644
index 0000000..3453e7a
--- /dev/null
+++ head/builtin_unreachable/Func_halve.fsti
@@ -0,0 +1,11 @@
+module Func_halve
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_halve (var_n: Typedef_uint32_t.ty_uint32_t)
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+requires (with_pure (((id #int (UInt32.v var_n)) % 2) = 0))
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_n 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/builtin_unreachable/Func_pick.fst head/builtin_unreachable/Func_pick.fst
new file mode 100644
index 0000000..2db77f4
--- /dev/null
+++ head/builtin_unreachable/Func_pick.fst
@@ -0,0 +1,28 @@
+module Func_pick
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_pick (var_version: Typedef_uint32_t.ty_uint32_t)
+  requires ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+  requires
+    (with_pure (((id #int (UInt32.v var_version)) = 1) || ((id #int (UInt32.v var_version)) = 2)))
+  returns return_1 : Typedef_uint32_t.ty_uint32_t
+  ensures ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+  ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
+{
+  let mut var_version = var_version;
+  let mut var_result : Typedef_uint32_t.ty_uint32_t;
+  var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+  let var___switch_scrut_0 : Typedef_uint32_t.ty_uint32_t = (!var_version);
+  if ((var___switch_scrut_0 = (id #UInt32.t (Int.Cast.int32_to_uint32 1l)))) {
+    var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 10l));
+  } else {
+    if ((var___switch_scrut_0 = (id #UInt32.t (Int.Cast.int32_to_uint32 2l)))) {
+      var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 20l));
+    } else {
+      unreachable ();
+    };
+  };
+  return (!var_result);
+}
\ No newline at end of file
diff --git head/builtin_unreachable/Func_pick.fsti head/builtin_unreachable/Func_pick.fsti
new file mode 100644
index 0000000..dffbbae
--- /dev/null
+++ head/builtin_unreachable/Func_pick.fsti
@@ -0,0 +1,12 @@
+module Func_pick
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_pick (var_version: Typedef_uint32_t.ty_uint32_t)
+requires ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+requires
+  (with_pure (((id #int (UInt32.v var_version)) = 1) || ((id #int (UInt32.v var_version)) = 2)))
+returns return_1 : Typedef_uint32_t.ty_uint32_t
+ensures ((Typedef_uint32_t.ty_uint32_t__pred var_version 1.0R))
+ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
\ No newline at end of file
diff --git head/builtin_unreachable/TranslationErrors.fst head/builtin_unreachable/TranslationErrors.fst
new file mode 100644
index 0000000..bf62561
--- /dev/null
+++ head/builtin_unreachable/TranslationErrors.fst
@@ -0,0 +1 @@
+module TranslationErrors
diff --git head/builtin_unreachable/Typedef___int32_t.fst head/builtin_unreachable/Typedef___int32_t.fst
new file mode 100644
index 0000000..516285c
--- /dev/null
+++ head/builtin_unreachable/Typedef___int32_t.fst
@@ -0,0 +1,12 @@
+module Typedef___int32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___int32_t : Type = Int32.t
+[@@pulse_eager_unfold] let predicate ty___int32_t__pred ([@@@mkey] this: ty___int32_t) (p: perm) =
+  emp
+[@@pulse_eager_unfold] let predicate ty___int32_t__uninit_pred ([@@@mkey] this: ty___int32_t) = emp
+instance has_zero_default_ty___int32_t : (has_zero_default ty___int32_t) =
+  { zero_default = (Int32.int_to_t 0) }
\ No newline at end of file
diff --git head/builtin_unreachable/Typedef___uint32_t.fst head/builtin_unreachable/Typedef___uint32_t.fst
new file mode 100644
index 0000000..b9a5b44
--- /dev/null
+++ head/builtin_unreachable/Typedef___uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef___uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty___uint32_t : Type = UInt32.t
+[@@pulse_eager_unfold] let predicate ty___uint32_t__pred ([@@@mkey] this: ty___uint32_t) (p: perm) =
+  emp
+[@@pulse_eager_unfold] let predicate ty___uint32_t__uninit_pred ([@@@mkey] this: ty___uint32_t) =
+  emp
+instance has_zero_default_ty___uint32_t : (has_zero_default ty___uint32_t) =
+  { zero_default = (UInt32.uint_to_t 0) }
\ No newline at end of file
diff --git head/builtin_unreachable/Typedef_int32_t.fst head/builtin_unreachable/Typedef_int32_t.fst
new file mode 100644
index 0000000..6996081
--- /dev/null
+++ head/builtin_unreachable/Typedef_int32_t.fst
@@ -0,0 +1,13 @@
+module Typedef_int32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_int32_t : Type = Typedef___int32_t.ty___int32_t
+[@@pulse_eager_unfold] let predicate ty_int32_t__pred ([@@@mkey] this: ty_int32_t) (p: perm) =
+  ((Typedef___int32_t.ty___int32_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_int32_t__uninit_pred ([@@@mkey] this: ty_int32_t) =
+  ((Typedef___int32_t.ty___int32_t__uninit_pred this))
+instance has_zero_default_ty_int32_t : (has_zero_default ty_int32_t) =
+  { zero_default = zero_default }
\ No newline at end of file
diff --git head/builtin_unreachable/Typedef_uint32_t.fst head/builtin_unreachable/Typedef_uint32_t.fst
new file mode 100644
index 0000000..aa0f488
--- /dev/null
+++ head/builtin_unreachable/Typedef_uint32_t.fst
@@ -0,0 +1,13 @@
+module Typedef_uint32_t
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_uint32_t : Type = Typedef___uint32_t.ty___uint32_t
+[@@pulse_eager_unfold] let predicate ty_uint32_t__pred ([@@@mkey] this: ty_uint32_t) (p: perm) =
+  ((Typedef___uint32_t.ty___uint32_t__pred this p))
+[@@pulse_eager_unfold] let predicate ty_uint32_t__uninit_pred ([@@@mkey] this: ty_uint32_t) =
+  ((Typedef___uint32_t.ty___uint32_t__uninit_pred this))
+instance has_zero_default_ty_uint32_t : (has_zero_default ty_uint32_t) =
+  { zero_default = zero_default }
\ No newline at end of file
diff --git head/builtin_unreachable/diagnostics.json head/builtin_unreachable/diagnostics.json
new file mode 100644
index 0000000..9e26dfe
--- /dev/null
+++ head/builtin_unreachable/diagnostics.json
@@ -0,0 +1 @@
+{}
\ No newline at end of file
diff --git base/character_literals/Func_classify_char.fst head/character_literals/Func_classify_char.fst
index 2cbc610..a66c650 100644
--- base/character_literals/Func_classify_char.fst
+++ head/character_literals/Func_classify_char.fst
@@ -14,26 +14,18 @@ divergent fn func_classify_char (var_c: Typedef_int32_t.ty_int32_t)
 {
   let mut var_c = var_c;
   let var___switch_scrut_0 : Typedef_int32_t.ty_int32_t = (!var_c);
-  let mut var___switch_hit_0 : bool;
-  var___switch_hit_0 := false;
-  let mut var___switch_brk_0 : bool;
-  var___switch_brk_0 := false;
-  if (((not (!var___switch_brk_0)) &&
-        ((!var___switch_hit_0) || (false || (var___switch_scrut_0 = 65l))))) {
-    var___switch_hit_0 := true;
+  if ((var___switch_scrut_0 = 65l)) {
     return 1l;
-  } else {};
-  if (((not (!var___switch_brk_0)) &&
-        ((!var___switch_hit_0) || (false || (var___switch_scrut_0 = 10l))))) {
-    var___switch_hit_0 := true;
-    return 2l;
-  } else {};
-  if (((not (!var___switch_brk_0)) &&
-        ((!var___switch_hit_0) || (false || (var___switch_scrut_0 = 0l))))) {
-    var___switch_hit_0 := true;
-    return 3l;
-  } else {};
-  var___switch_hit_0 := true;
-  return 0l;
+  } else {
+    if ((var___switch_scrut_0 = 10l)) {
+      return 2l;
+    } else {
+      if ((var___switch_scrut_0 = 0l)) {
+        return 3l;
+      } else {
+        return 0l;
+      };
+    };
+  };
   return 0l;
 }
\ No newline at end of file
diff --git base/do_while/Func_find_limit.fst head/do_while/Func_find_limit.fst
index cba1cf5..499ec89 100644
--- base/do_while/Func_find_limit.fst
+++ head/do_while/Func_find_limit.fst
@@ -21,17 +21,17 @@ divergent fn func_find_limit
   let mut var_limit = var_limit;
   let mut var_i : Typedef_uint32_t.ty_uint32_t;
   var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
-  let mut var___do_cont_2 : bool;
-  var___do_cont_2 := true;
+  let mut var___do_cont_1 : bool;
+  var___do_cont_1 := true;
   let mut var_first : bool;
   var_first := true;
-  while ((!var___do_cont_2))
+  while ((!var___do_cont_1))
     invariant ((((live var_i) ** (live var_n)) ** (live var_limit)) ** (live var_first))
     invariant (with_pure
         ((!var_first) ==> ((id #int (UInt32.v (!var_i))) < (id #int (UInt32.v (!var_n))))))
     invariant (with_pure ((id #int (UInt32.v (!var_i))) <= (id #int (UInt32.v (!var_n)))))
-    invariant (live var___do_cont_2)
-    invariant (with_pure ((!var___do_cont_2) = ((!var_first) || ((!var_i) `UInt32.lt` (!var_n)))))
+    invariant (live var___do_cont_1)
+    invariant (with_pure ((!var___do_cont_1) = ((!var_first) || ((!var_i) `UInt32.lt` (!var_n)))))
     ensures ((id #int (UInt32.v (!var_i))) <= (id #int (UInt32.v (!var_n))))
   {
     if (((!var_i) = (!var_limit))) {
@@ -39,7 +39,7 @@ divergent fn func_find_limit
     } else {};
     var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
     var_first := false;
-    var___do_cont_2 := ((!var_i) `UInt32.lt` (!var_n));
+    var___do_cont_1 := ((!var_i) `UInt32.lt` (!var_n));
   };
   return (!var_i);
 }
\ No newline at end of file
diff --git base/do_while/Func_nested_continue.fst head/do_while/Func_nested_continue.fst
index 04a0385..8e7b5a2 100644
--- base/do_while/Func_nested_continue.fst
+++ head/do_while/Func_nested_continue.fst
@@ -13,17 +13,17 @@ divergent fn func_nested_continue (var_n: Typedef_uint32_t.ty_uint32_t)
   let mut var_n = var_n;
   let mut var_i : Typedef_uint32_t.ty_uint32_t;
   var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
-  let mut var___do_cont_4 : bool;
-  var___do_cont_4 := true;
+  let mut var___do_cont_3 : bool;
+  var___do_cont_3 := true;
   let mut var_first : bool;
   var_first := true;
-  while ((!var___do_cont_4))
+  while ((!var___do_cont_3))
     invariant (((live var_i) ** (live var_n)) ** (live var_first))
     invariant (with_pure
         ((!var_first) ==> ((id #int (UInt32.v (!var_i))) < (id #int (UInt32.v (!var_n))))))
     invariant (with_pure ((id #int (UInt32.v (!var_i))) <= (id #int (UInt32.v (!var_n)))))
-    invariant (live var___do_cont_4)
-    invariant (with_pure ((!var___do_cont_4) = ((!var_first) || ((!var_i) `UInt32.lt` (!var_n)))))
+    invariant (live var___do_cont_3)
+    invariant (with_pure ((!var___do_cont_3) = ((!var_first) || ((!var_i) `UInt32.lt` (!var_n)))))
   {
     let mut var_j : Typedef_uint32_t.ty_uint32_t;
     var_j := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
@@ -39,7 +39,7 @@ divergent fn func_nested_continue (var_n: Typedef_uint32_t.ty_uint32_t)
     };
     var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
     var_first := false;
-    var___do_cont_4 := ((!var_i) `UInt32.lt` (!var_n));
+    var___do_cont_3 := ((!var_i) `UInt32.lt` (!var_n));
   };
   return (!var_i);
 }
\ No newline at end of file
diff --git base/do_while/Func_run_once.fst head/do_while/Func_run_once.fst
index 3cb327b..de4f3c5 100644
--- base/do_while/Func_run_once.fst
+++ head/do_while/Func_run_once.fst
@@ -13,19 +13,6 @@ divergent fn func_run_once (var_x: Typedef_uint32_t.ty_uint32_t)
   let mut var_x = var_x;
   let mut var_r : Typedef_uint32_t.ty_uint32_t;
   var_r := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
-  let mut var___do_cont_1 : bool;
-  var___do_cont_1 := true;
-  let mut var___do_first_0 : bool;
-  var___do_first_0 := true;
-  while ((!var___do_cont_1))
-    invariant (live var_r)
-    invariant (live var___do_cont_1)
-    invariant (live var___do_first_0)
-    invariant (with_pure ((!var___do_cont_1) = ((!var___do_first_0) || (int32_to_bool 0l))))
-  {
-    var_r := (!var_x);
-    var___do_first_0 := false;
-    var___do_cont_1 := (int32_to_bool 0l);
-  };
+  var_r := (!var_x);
   return (!var_r);
 }
\ No newline at end of file
diff --git base/switch_stmt/Func_classify_with_returns.fst head/switch_stmt/Func_classify_with_returns.fst
index dbeccba..2c3bb3c 100644
--- base/switch_stmt/Func_classify_with_returns.fst
+++ head/switch_stmt/Func_classify_with_returns.fst
@@ -11,15 +11,9 @@ divergent fn func_classify_with_returns (var_x: Typedef_int32_t.ty_int32_t)
 {
   let mut var_x = var_x;
   let var___switch_scrut_8 : Typedef_int32_t.ty_int32_t = (!var_x);
-  let mut var___switch_hit_8 : bool;
-  var___switch_hit_8 := false;
-  let mut var___switch_brk_8 : bool;
-  var___switch_brk_8 := false;
-  if (((not (!var___switch_brk_8)) &&
-        ((!var___switch_hit_8) || (false || (var___switch_scrut_8 = 0l))))) {
-    var___switch_hit_8 := true;
+  if ((var___switch_scrut_8 = 0l)) {
     return 10l;
-  } else {};
-  var___switch_hit_8 := true;
-  return 20l;
+  } else {
+    return 20l;
+  };
 }
\ No newline at end of file

nikswamy and others added 5 commits August 18, 2026 15:27

Merge branch 'nswamy/pal-pr18-unreachable' into nswamy/pal-pr21-switc…

e6193e9

…h-jump-abort

Navigation Menu

Uh oh!

Let a switch arm end in a jump or an abort - #235

Let a switch arm end in a jump or an abort#235
nikswamy wants to merge 5 commits into
nswamy/pal-pr20-switch-default-and-if-chainfrom
nswamy/pal-pr21-switch-jump-abort

nikswamy commented Aug 19, 2026

Uh oh!

gebner commented Aug 26, 2026

Uh oh!

github-actions Bot commented Aug 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

nikswamy commented Aug 19, 2026

Commits

Testing

Uh oh!

gebner commented Aug 26, 2026

Uh oh!

github-actions Bot commented Aug 26, 2026

Generated F* output diff

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants