Commit 302d06a
committed
C front-end/KnR: generate nondet for missing arguments
The back-end does not know how to handle `nil`, and symex would also
generate nondet in such cases, so do the same in the front-end.1 parent d932d6f commit 302d06a
File tree
3 files changed
+23
-4
lines changed- regression/cbmc/KnR1
- src/ansi-c
3 files changed
+23
-4
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
3698 | 3698 | | |
3699 | 3699 | | |
3700 | 3700 | | |
3701 | | - | |
3702 | | - | |
3703 | | - | |
3704 | | - | |
| 3701 | + | |
| 3702 | + | |
| 3703 | + | |
| 3704 | + | |
| 3705 | + | |
| 3706 | + | |
3705 | 3707 | | |
3706 | 3708 | | |
3707 | 3709 | | |
| |||
0 commit comments