Commit f4f01cd
committed
Test the
To ensure the fields of the `this` argument to the a constructor are not
incorrectly nondet initialised before entering the constructor.this argument used when checking a constructor1 parent cfeade5 commit f4f01cd
File tree
3 files changed
+16
-0
lines changed- jbmc/regression/jbmc/constructor2
3 files changed
+16
-0
lines changedBinary file not shown.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
0 commit comments