Commit 79485d6
C nondet factory: Ensure parameter initialisers use unique symbol names
The nondet symbol factory uses "tmp" as a default basename prefix, and
in all other places already generated unique names using
`get_fresh_aux_symbol`. This function, however, will happily use exactly
that basename when there wouldn't be a conflict. The code fixed in this
commit, however, did not yet use this facility, and just assumed that
each parameter of the target function would result in a unique local
name. A parameter named "tmp," then, resulted in a conflict.
Consistently using `get_fresh_aux_symbol` addresses this problem.
Fixes: #6566
Co-authored-by: Matthias Güdemann <matthias.guedemann@hm.edu>1 parent 169dc18 commit 79485d6
File tree
3 files changed
+20
-16
lines changed- regression/cbmc/pointer-function-parameters
- src/ansi-c
3 files changed
+20
-16
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 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 | |
|---|---|---|---|
| |||
15 | 15 | | |
16 | 16 | | |
17 | 17 | | |
| 18 | + | |
18 | 19 | | |
19 | 20 | | |
20 | 21 | | |
| |||
204 | 205 | | |
205 | 206 | | |
206 | 207 | | |
207 | | - | |
208 | | - | |
209 | | - | |
210 | | - | |
211 | | - | |
212 | | - | |
213 | | - | |
214 | | - | |
215 | | - | |
216 | | - | |
217 | | - | |
| 208 | + | |
| 209 | + | |
| 210 | + | |
| 211 | + | |
| 212 | + | |
| 213 | + | |
| 214 | + | |
218 | 215 | | |
219 | 216 | | |
220 | | - | |
221 | | - | |
222 | | - | |
223 | | - | |
224 | 217 | | |
225 | 218 | | |
226 | 219 | | |
| |||
231 | 224 | | |
232 | 225 | | |
233 | 226 | | |
234 | | - | |
| 227 | + | |
235 | 228 | | |
236 | 229 | | |
237 | 230 | | |
| |||
0 commit comments