GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-24 08:53:12 +03:00
Code Issues Projects Releases Wiki Activity

[refinement] add note to sample input for refinement tests.

Browse Source
This commit is contained in:
Kevin Quick 2019-02-07 16:43:11 -08:00
parent 3c6492b6fb
commit e47887a9f1
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
refinement/tests/samples/switching.c
View File

@ -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()