Bug #7998
closedseq_operations specification: Invalid scenario
0%
Description
Current state:
"start_step": { "process": "[start].(<start_success>.{next_step} | <start_failed>.[stop].(deregister))" }, "next_step": { "process": "[next].[show].(<next_success>.{next_step} | <next_fail>.[stop].{start_step})" },
while it should be something like this:
struct seq_file *m = %seq_file%; loff_t index = 0; void *p; p = op->start(m, &index); check_res_and_show: if ((p == NULL) || IS_ERR(p)) goto stop; int error = op->show(m, p); if (error < 0) goto stop; if (nondet_int()) goto stop; p = op->next(m, &index); goto check_res_and_show; stop: op->stop(m, p);
Updated by Evgeny Novikov about 7 years ago
- Assignee set to Ilja Zakharov
It is unclear why it is so important in terms of, say, false alarms or/and missed bugs. Any way we have the only developer who can fix this well.
Updated by Ilja Zakharov about 7 years ago
Fixed in seq-ops-fix branch.
To make fixing a bit more straightforward it would be nice to have an example of a false positive to test my fix. Otherwise I do testing using my tests but they contain not many specific checks.
Updated by Alexey Khoroshilov about 7 years ago
net/packet/af_packet.ko, generic:memory
Updated by Ilja Zakharov about 7 years ago
- Status changed from Resolved to Verified
After an additional fix the false positive is gone.
The fixed merged in master in 637453e.
Updated by Ilja Zakharov about 7 years ago
- Status changed from Verified to Closed
Updated by Alexey Khoroshilov about 7 years ago
- Status changed from Closed to Open
I have a couple of questions about the implementation.
"index": { "signature": "loff_t *a" } "start": { "callback": "%ops.start%", "parameters": [ "%seq_file%", "%index%" ], }, "stop": { "callback": "%ops.stop%", "pre-call": [ "%seq_file%->index = %index%;" ], "post-call": [ "%seq_file%->index = %index%;" ], },
1. Does index passed as argument mean a pointer to exactly one integer?
2. "%seq_file%->index = index;" looks like loff_t* to loff_t assignment. Is it?
Updated by Ilja Zakharov about 7 years ago
- Status changed from Open to Resolved
1. Does index passed as argument mean a pointer to exactly one integer?
EMG for each label and interface type pair generates a variable. In this case it generates a variable ldv_$num$_index_index which is passed to start and next callbacks. So if it is not changed by callbacks, then the integer is always the same.
2. "%seq_file%->index = index;" looks like loff_t* to loff_t assignment. Is it?
Yes, this is a bug. I have corrected the specification in 'seq-index-fix' branch.
Updated by Ilja Zakharov about 7 years ago
- Status changed from Resolved to Verified
Merged to master in 4fc472bf.
Updated by Ilja Zakharov about 7 years ago
- Status changed from Verified to Closed