Bug #8044
closedTemporary variables within cycles were removed incorrectly
Added by Evgeny Novikov about 7 years ago. Updated about 7 years ago.
0%
Description
The same temporary variables can be used in several edges (statements) within cycles, but the witnesses preprocessor doesn't care.
Files
| error_trace.zip (278 KB) error_trace.zip | Evgeny Novikov, 03/21/2017 08:09 PM | ||
| error_trace 2.zip (311 KB) error_trace 2.zip | Evgeny Novikov, 03/22/2017 12:51 PM |
Updated by Evgeny Novikov about 7 years ago
- File error_trace.zip added
I attached one more example that isn't similar to the original one.
Updated by Vladimir Gratinskiy about 7 years ago
Evgeny Novikov wrote:
I attached one more example that isn't similar to the original one.
First error trace has one enter to function 'ldv_malloc_unknown_size':"enter": 39
but two returns"return": 39
So I'm sure the second error trace has similar problem too.
Updated by Evgeny Novikov about 7 years ago
Vladimir Gratinskiy wrote:
Evgeny Novikov wrote:
I attached one more example that isn't similar to the original one.
First error trace has one enter to function 'ldv_malloc_unknown_size':
"enter": 39
but two returns"return": 39So I'm sure the second error trace has similar problem too.
Please, inspect the second error trace.
Updated by Vladimir Gratinskiy about 7 years ago
Evgeny Novikov wrote:
Please, inspect the second error trace.
You've attached one error trace twice.
Updated by Evgeny Novikov about 7 years ago
- File error_trace.zip added
Vladimir Gratinskiy wrote:
Evgeny Novikov wrote:
Please, inspect the second error trace.
You've attached one error trace twice.
Let's try so.
Updated by Evgeny Novikov about 7 years ago
- File error_trace 2.zip error_trace 2.zip added
Evgeny Novikov wrote:
Vladimir Gratinskiy wrote:
Evgeny Novikov wrote:
Please, inspect the second error trace.
You've attached one error trace twice.
Let's try so.
And this is a correct file at last.
Updated by Vladimir Gratinskiy about 7 years ago
- Assignee deleted (
Vladimir Gratinskiy)
Evgeny Novikov wrote:
Evgeny Novikov wrote:
Vladimir Gratinskiy wrote:
Evgeny Novikov wrote:
Please, inspect the second error trace.
You've attached one error trace twice.
Let's try so.
And this is a correct file at last.
The second error trace contains one return from function "ldv_post_probe":"return": 34
but it doesn't have enter to it.
So the problem is in generating error traces, not in visualization.
Updated by Evgeny Novikov about 7 years ago
- Category changed from Bridge to Tasks generation
- Assignee set to Evgeny Novikov
- Priority changed from Immediate to Urgent
Thank you. I will take care of this later.
Updated by Evgeny Novikov about 7 years ago
- Priority changed from Urgent to Immediate
This issue makes quite many results worse while it can be likely trivially fixed.
Updated by Evgeny Novikov about 7 years ago
- Subject changed from Bridge could not visualize some error traces to Temporary variables within cycles were removed incorrectly
- Description updated (diff)
- Status changed from New to Closed
I fixed this in 346fb598 to master.
BTW, this was likely the last issue during witnesses preprocessing regarding all rules except generic:memory and sync:race but may be even regarding them as well.