A forum for Spin users
You are not logged in.
Pages: 1
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 =====
Offline
I make simpler patch 2. This is better than previous patch.
== patch 2 =====
--- spinlex.c 2014-03-09 23:53:58.400411848 +0900
+++ spinlex_mod.c 2014-03-09 23:59:22.774061879 +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,24 @@
break;
case '#':
if (cnr == 0)
- { p--;
+ {
+ /* A.Tanaka 2014.3.9 */
+ int before_lineno = lineno;
+ p--;
do_directive(c); /* reads to newline */
+ if(before_lineno < lineno){
+ int n;
+ int ln = lineno;
+ /* get ceiling(log10(lineno)) */
+ for(n = 0; ln > 0; n++) ln /= 10;
+ /* check Buf1's buffer overflow */
+ n += 3; /* 3(SCACE '\n' '\0') */
+ if ((p+n) - Buf1 >= SOMETHINGBIG)
+ fatal("inline text too long", 0);
+ sprintf(p, "# %d\n", lineno);
+ p += n;
+ }
+
} else
{ firstchar = 0;
cnr++;
================
Offline
Patch files doesn't work by cut and paste.
So, I would like to re-post patch by using code-tag.
Patch 1:
--- spin.y 2014-03-10 09:56:54.131979930 +0900
+++ spin_mod.y 2014-03-10 09:54:23.382536160 +0900
@@ -26,6 +26,9 @@
static Lextok *ltl_to_string(Lextok *);
+/* A.Tanaka, 2014.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, 2014.2.18 */
+ | D_PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1;
+ modify_ln_fn($$, $1);} /* A.Tanaka, 2014.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, 2014.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, 2014.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, 2014.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, 2014.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, 2014.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, 2014.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, 2014.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, 2014.2.18 */
}
;
body : '{' { open_seq(1); }
- sequence OS { add_seq(Stop); }
+ sequence OS { add_seq(Stop);
+ /* A.Tanaka, 2014.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, 2014.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, 2014.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, 2014.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, 2014.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, 2014.2.18 */
}
- | TIMEOUT { $$ = nn(ZN,TIMEOUT, ZN, ZN); }
+ | TIMEOUT { $$ = nn(ZN,TIMEOUT, ZN, ZN);
+ modify_ln_fn($$, $1); /* A.Tanaka, 2014.2.18 */
+ }
| NONPROGRESS { $$ = nn(ZN,NONPROGRESS, ZN, ZN);
has_np++;
+ modify_ln_fn($$, $1); /* A.Tanaka, 2014.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, 2014.2.18 */
}
| '-' CONST %prec UMIN { $$ = nn(ZN,CONST,ZN,ZN);
$$->val = - ($2->val);
+ modify_ln_fn($$, $2); /* A.Tanaka, 2014.2.18 */
}
;
@@ -997,11 +1026,28 @@
m->sym = lookup(ltl_formula);
+ modify_ln_fn(m, n); /* A.Tanaka, 2014.2.18 */
+
return m;
}
+
+/* A.Tanaka, 2014.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);
}
+
+Patch 2:
--- spinlex.c 2014-03-09 23:53:58.400411848 +0900
+++ spinlex_mod.c 2014-03-09 23:59:22.774061879 +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,24 @@
break;
case '#':
if (cnr == 0)
- { p--;
+ {
+ /* A.Tanaka 2014.3.9 */
+ int before_lineno = lineno;
+ p--;
do_directive(c); /* reads to newline */
+ if(before_lineno < lineno){
+ int n;
+ int ln = lineno;
+ /* get ceiling(log10(lineno)) */
+ for(n = 0; ln > 0; n++) ln /= 10;
+ /* check Buf1's buffer overflow */
+ n += 3; /* 3(SCACE '\n' '\0') */
+ if ((p+n) - Buf1 >= SOMETHINGBIG)
+ fatal("inline text too long", 0);
+ sprintf(p, "# %d\n", lineno);
+ p += n;
+ }
+
} else
{ firstchar = 0;
cnr++;Offline
Pages: 1