Project

General

Profile

Actions

Bug #7998

closed

seq_operations specification: Invalid scenario

Added by Alexey Khoroshilov about 7 years ago. Updated about 7 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Environment models
Target version:
-
Start date:
02/24/2017
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

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);

Actions

Also available in: Atom PDF