Commit 25de48d
committed
Move regression tests of the C front-end to a suitable folder
There is no bounded model checking expected or required by these tests, and also
they use GCC-specific built-ins. There is still work left to be done, so most
remain KNOWNBUG (but now the reason thereof is explained).1 parent 99659b3 commit 25de48d
File tree
19 files changed
+52
-37
lines changed- regression
- cbmc
- builtin_is
- builtin_va_copy_lvalue
- builtin_va_end_lvalue
- builtin_va_start_lvalue
- builtin_va_start_two
- goto-gcc
- builtin_is
- builtin_va_copy_lvalue
- builtin_va_copy_two
- builtin_va_end_lvalue
- builtin_va_end_one
- builtin_va_start_lvalue
- builtin_va_start_two
19 files changed
+52
-37
lines changedThis file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
File renamed without changes.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
File renamed without changes.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
File renamed without changes.
0 commit comments