Spinroot

This report relates the topic which is  "Line number of the statement by sk".
(I'm sorry long report.)

The following is a other inconvenient line number example by reporting from sk to me.
=== ex.pml ===
1: int g;
2:
3: inline test(a)
4: {
5:  int b;
6:  int c = 1;
7:  // comment
8:  // comment
9:  // comment
10:  // comment
11:  // comment
12:  // comment
13:  // comment
14:
15:  b = a + c;
16:  a = b + 1;
17: }
18: 
19: init
20: {
21:   g = 5;
22:   test(g)
23: }
==============

The following is the output " gcc -E -x c ex.pml " which is input of yyparse() in main.c.
=== gcc's preprocess ===
# 1 "linenum2.pml"
# 1 "<comandline>"
# 1 "linenum2.pml"
int g;

inline test(a)
{
  int b;
  int c = 1;
# 15 "linenum2.pml"
  b = a + c;
  a = b + 1;
}

init
{
  g = 5;
  test(g)
}
=======================

The following is the result after applying my patch in the topic which is
"Line number of the statement by sk".
=== result ===
> spin -p -s -r -v -g -u1000 ex.pml
  0:    proc  - (:root:) creates proc  0 (:init:)
  1:    proc  0 (:init::1) linenum2.pml:21 (state 1)    [g = 5]
        g = 5
  2:    proc  0 (:init::1) linenum2.pml:6 (state 2)    [b = 0]    <- 5 is correct.(problem1)
  3:    proc  0 (:init::1) linenum2.pml:7 (state 3)    [c = 1]    <- 6 is correct.(problem1)
  4:    proc  0 (:init::1) linenum2.pml:7 (state 4)    [b = (g+c)] <- 15 is correct.(problem2)
  5:    proc  0 (:init::1) linenum2.pml:8 (state 5)    [g = (b+1)] <- 16 is correct.(problem2)
        g = 7
  5:    proc  0 (:init::1)       terminates
1 process created

==============

I make 2 patches for this problems.
Patch 1 relates problem1. Patch 2 relates problem2.
I attach my 2 patches this report at last.
Could you please confirm it ?

<About patch 1>
The problem1 relates around spin.y grammar,
  ivar    : vardcl
          | vardcl ASGN expr
I think we should pay attention that yacc generates LALR(1) type parser.
You know, here "(1)" means "1 token Look-ahead". And we should pay attention
that the parser sometimes pre-reads 1 token when the parser decides to
select one grammar, if it exists multiple candidate grammars for acceptable.
It looks this problem causes for "one token Look-ahead".
So, I think you should get line number from grammar element's values $N as far as possible.
I checked parts in spin.y which parts are around caller "nn(ZN, ..., ZN, ZN)".

<About patch 2>
As gcc's preprocess output, you can see some number of comment and empty lines are deleted and
added one "# line-number file-name" line.
So, I think you should insert "# line-number" to inline function buffer also.

== patch 1 =====
--- spin.y    2014-03-08 18:16:14.866997149 +0900
+++ spin_mod.y    2014-03-08 18:14:35.510504467 +0900
@@ -26,6 +26,9 @@

static    Lextok *ltl_to_string(Lextok *);

+/* A.Tanaka, 2012.2.14 */
+static void modify_ln_fn(Lextok *, Lextok *);
+
extern  Symbol    *context, *owner;
extern    Lextok *for_body(Lextok *, int);
extern    void for_setup(Lextok *, Lextok *, Lextok *);
@@ -154,16 +157,22 @@
            }
    ;

-proctype: PROCTYPE    { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0; }
-    | D_PROCTYPE    { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
+proctype: PROCTYPE    { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0;
+                      modify_ln_fn($$, $1);}        /* A.Tanaka, 2012.2.18 */
+    | D_PROCTYPE    { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1;
+                      modify_ln_fn($$, $1);}        /* A.Tanaka, 2012.2.18 */
    ;

inst    : /* empty */    { $$ = ZN; }
-    | ACTIVE    { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
+    | ACTIVE    { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1;
+                      modify_ln_fn($$, $1);}        /* A.Tanaka, 2012.2.18 */
+
    | ACTIVE '[' const_expr ']' {
              $$ = nn(ZN,CONST,ZN,ZN); $$->val = $3->val;
              if ($3->val > 255)
                non_fatal("max nr of processes is 255\n", "");
+
+              modify_ln_fn($$, $3);        /* A.Tanaka, 2012.2.18 */
            }
    | ACTIVE '[' NAME ']' {
              $$ = nn(ZN,CONST,ZN,ZN);
@@ -176,6 +185,7 @@
                    $3->sym->name);
              else
                $$->val = $3->sym->ini->val;
+              modify_ln_fn($$, $3);        /* A.Tanaka, 2012.2.18 */
            }
    ;

@@ -218,7 +228,7 @@
              memset(tb, 0, 32);
              sprintf(tb, "never_%d", nclaims);
              $$ = nn(ZN, NAME, ZN, ZN);
-              $$->sym = lookup(tb);
+              $$->sym = lookup(tb);           /* A.Tanaka, 2012.2.18, check later */
            }
    | NAME        { $$ = $1; }
    ;
@@ -227,7 +237,7 @@
              memset(tb, 0, 32);
              sprintf(tb, "ltl_%d", nltl++);
              $$ = nn(ZN, NAME, ZN, ZN);
-              $$->sym = lookup(tb);
+              $$->sym = lookup(tb);           /* A.Tanaka, 2012.2.18, check later */
            }
    | NAME        { $$ = $1; }
    ;
@@ -302,6 +312,7 @@
                  $$ = nn(ZN, C_CODE, ZN, ZN);
                  $$->sym = s;
                  has_code = 1;
+                  modify_ln_fn($$, $1);        /* A.Tanaka, 2012.2.18 */
                }
    | C_DECL        { Symbol *s;
                  NamesNotAdded++;
@@ -311,6 +322,7 @@
                  $$ = nn(ZN, C_CODE, ZN, ZN);
                  $$->sym = s;
                  has_code = 1;
+                  modify_ln_fn($$, $1);        /* A.Tanaka, 2012.2.18 */
                }
    ;
cexpr    : C_EXPR        { Symbol *s;
@@ -321,11 +333,13 @@
                  $$->sym = s;
                  no_side_effects(s->name);
                  has_code = 1;
+                  modify_ln_fn($$, $1);        /* A.Tanaka, 2012.2.18 */
                }
    ;

body    : '{'            { open_seq(1); }
-          sequence OS        { add_seq(Stop); }
+          sequence OS        { add_seq(Stop);
+                              /* A.Tanaka, 2012.2.18, maybe ok. check later */ } 
           '}'            { $$->sq = close_seq(0);
                  if (scope_level != 0)
                  {    non_fatal("missing '}' ?", 0);
@@ -402,6 +416,9 @@
                    zx = nn(ZN, NAME, ZN, ZN);
                    zx->sym = $1->sym;
                    xz = nn(zx, ASGN, zx, $1->sym->ini);
+
+                    modify_ln_fn(xz, $1);  /* A.Tanaka, 2014.2.14*/
+
                    keep_track_off(xz);
                    /* make sure zx doesnt turn out to be a STRUCT later */
                    add_seq(xz);
@@ -421,6 +438,9 @@
                  if (!initialization_ok)
                  {    Lextok *zx = nn(ZN, NAME, ZN, ZN);
                    zx->sym = $1->sym;
+                   
+                    modify_ln_fn(zx, $1);  /* A.Tanaka, 2014.2.14*/
+                   
                    add_seq(nn(zx, ASGN, zx, $3));
                  }
                }
@@ -541,6 +561,7 @@
                     }
    | BREAK          { $$ = nn(ZN, GOTO, ZN, ZN);
                  $$->sym = break_dest();
+                  modify_ln_fn($$, $1);        /* A.Tanaka, 2012.2.18 */
                }
    | GOTO NAME        { $$ = nn($2, GOTO, ZN, ZN);
                  if ($2->sym->type != 0
@@ -567,6 +588,7 @@
                  $$->lft = nn(ZN, 'c', nn(ZN,CONST,ZN,ZN), ZN);
                  $$->lft->lft->val = 1; /* skip */
                  $1->sym->type = LABEL;
+                              modify_ln_fn($$, $1);        /* A.Tanaka, 2012.2.18 */
                }
    ;

@@ -625,7 +647,7 @@
                }
    | full_expr        { $$ = nn(ZN, 'c', $1, ZN); count_runs($$); }
    | ELSE          { $$ = nn(ZN,ELSE,ZN,ZN);
-                }
+                              modify_ln_fn($$, $1);}        /* A.Tanaka, 2012.2.18 */
    | ATOMIC   '{'       { open_seq(0); }
           sequence OS '}'       { $$ = nn($1, ATOMIC, ZN, ZN);
                       $$->sl = seqlist(close_seq(3), 0);
@@ -665,7 +687,8 @@

option  : SEP           { open_seq(0); }
           sequence OS        { $$ = nn(ZN,0,ZN,ZN);
-                  $$->sq = close_seq(6); }
+                  $$->sq = close_seq(6);
+                  modify_ln_fn($$, $2);}        /* A.Tanaka, 2012.2.18 */
    ;

OS    : /* empty */
@@ -750,10 +773,14 @@
    | CONST         { $$ = nn(ZN,CONST,ZN,ZN);
                  $$->ismtyp = $1->ismtyp;
                  $$->val = $1->val;
+                              modify_ln_fn($$, $1);        /* A.Tanaka, 2012.2.18 */
                }
-    | TIMEOUT        { $$ = nn(ZN,TIMEOUT, ZN, ZN); }
+    | TIMEOUT        { $$ = nn(ZN,TIMEOUT, ZN, ZN);
+                              modify_ln_fn($$, $1);        /* A.Tanaka, 2012.2.18 */
+                                }
    | NONPROGRESS        { $$ = nn(ZN,NONPROGRESS, ZN, ZN);
                  has_np++;
+                              modify_ln_fn($$, $1);        /* A.Tanaka, 2012.2.18 */
                }
    | PC_VAL '(' expr ')'    { $$ = nn(ZN, PC_VAL, $3, ZN);
                  has_pcvalue++;
@@ -874,9 +901,11 @@
    | CONST         { $$ = nn(ZN,CONST,ZN,ZN);
                  $$->ismtyp = $1->ismtyp;
                  $$->val = $1->val;
+                              modify_ln_fn($$, $1);        /* A.Tanaka, 2012.2.18 */
                }
    | '-' CONST %prec UMIN    { $$ = nn(ZN,CONST,ZN,ZN);
                  $$->val = - ($2->val);
+                              modify_ln_fn($$, $2);        /* A.Tanaka, 2012.2.18 */
                }
    ;

@@ -997,11 +1026,28 @@

    m->sym = lookup(ltl_formula);

+    modify_ln_fn(m, n);    /* A.Tanaka, 2012.2.18 */
+
    return m;
}

+
+/* A.Tanaka, 2012.2.14 */
+static void
+modify_ln_fn(Lextok *s, Lextok *n)
+{
+  if(n) {
+    if(n->ln)
+      s->ln = n->ln;
+    if(n->fn)
+      s->fn = n->fn;
+  }
+}
+
void
yyerror(char *fmt, ...)
{
    non_fatal(fmt, (char *) 0);
}
+
+
== to here =====

== patch 2 =====
--- spinlex.c    2014-03-08 18:15:59.010918523 +0900
+++ spinlex_mod.c    2014-03-08 18:39:22.889879983 +0900
@@ -999,7 +999,7 @@
static void
do_directive(int first)
{    int c = first;    /* handles lines starting with pound */
-
+ 
    getword(c, isalpha_);

    if (strcmp(yytext, "#ident") == 0)
@@ -1151,8 +1151,30 @@
        break;
    case '#':
        if (cnr == 0)
-        {    p--;
+        {
+            /* A.Tanaka 2014.3.8 */
+                        #define LINENO_BUF_SIZE 10    
+                char lineno_buf[LINENO_BUF_SIZE]; 
+                  /* LINENO_BUF_SIZE is decided that ceiling(log10(SOMETHINGBIG)) + 3('#', SCACE,''\0') + 2(margin)*/
+                int before_lineno = lineno;
+                p--;
            do_directive(c); /* reads to newline */
+            if(before_lineno < lineno){
+              /* get ceiling(log10(lineno)) and check lineno_buf's buffer overflow */
+              int n;
+              int ln = lineno;
+              for(n = 0; ln > 0; n++) ln /= 10;
+              n += 3;  /*  3('#', SCACE,''\0') */
+              if (n > LINENO_BUF_SIZE)
+                fatal("inline text too long", 0);
+              /* check Buf1's buffer overflow */
+              if ((p+n) - Buf1 >= SOMETHINGBIG)
+                fatal("inline text too long", 0);
+              sprintf(lineno_buf, "# %d\n", lineno);
+              strcpy(p, lineno_buf);
+              p += strlen(lineno_buf);
+            }
+
        } else
        {    firstchar = 0;
            cnr++;
== to here =====