From e47887a9f1331a14d57eb62c08aff9cb6e9487b0 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Thu, 7 Feb 2019 16:43:11 -0800 Subject: [PATCH] [refinement] add note to sample input for refinement tests. --- refinement/tests/samples/switching.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/refinement/tests/samples/switching.c b/refinement/tests/samples/switching.c index 6bd5d77c..eeebdfd0 100644 --- a/refinement/tests/samples/switching.c +++ b/refinement/tests/samples/switching.c @@ -12,7 +12,11 @@ int64_t select(int64_t a, int64_t b) case 5: return b+5; default: return 0; } - // Has a "jmp rax", which is a classify failure "stmtsTerm = unknown transfer" + // Has a "jmp rax", which is a classify failure "stmtsTerm = + // unknown transfer". Note that it seems to require at least 6 + // case branch targets (for GCC 7.4.0 with -O0) to create a + // computed branch target; fewer case targets just implement + // explicit jumps. } void _start()