proctype test(int a) {
int ilocal;
progress:
i = 0;
do
:: i < a ->
i++;
printf("i = %d\n", i);
c_code {
now.i++;
Ptest->ilocal = 1478;
now.j = 8741;
};
assert(ilocal == 1478 && j == 8741);
printf("after c_code i = %d\n", i);
:: else -> break;
od
}
init {
run test(15);
}
When i simulate the code by iSpin, it reports an access violation as bellow:
7: proc 1 (test) a.pml:15 (state 5) [{c_code1}]
spin: a.pml:16, Error: assertion violated
spin: text of failed assertion: assert(((ilocal==1478)&&(j==8741)))
It seems that the embedded C code not run at all, please help me.
Thanks.
Regards,
Madhukar
[url]http://spinroot.com/spin/Doc/spin4_ch17.pdf[/url]
]]>However, I have some doubts about the variables that I need to "track".
In the sample code that I had put above, I had just tried to replicate the behavior of my code. The actual code is a bit more involved and the value of x in modified depending on a lot of other factors (an integer array, amongst other things). When I "track" x alone, the verification does not work fine. Although when I "track" the array as well, I do get the counterexample as expected.
How would I figure out, in general, the set of variables that I need to "track"?
Regards,
Madhukar
c_track "&x" "sizeof(int)"
then, also add a semicolon after the } following the call to increment(); to avoid a syntax error there.
next, add the following ltl formula:
ltl { !<> badstate }
and you'll get the counter-example as expected:
$ spin -a example.pml
ltl ltl_0: ! (<> (badstate))
$ cc -o pan pan.c
$ ./pan
warning: never claim + accept labels requires -a flag to fully verify
hint: this search is more efficient if pan.c is compiled -DSAFETY
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan:1: end state in claim reached (at depth 43)
pan: wrote foobar.pml.trail
(Spin Version 6.1.0 -- 3 March 2011)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (ltl_0)
assertion violations + (if within scope of claim)
acceptance cycles - (not selected)
invalid end states - (disabled by never claim)
State-vector 24 byte, depth reached 43, errors: 1
22 states, stored
0 states, matched
22 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.001 equivalent memory usage for states (stored*(State-vector + overhead))
0.291 actual memory usage for states (unsuccessful compression: 34665.00%)
state-vector as stored = 13850 byte + 16 byte overhead
2.000 memory used for hash table (-w19)
0.343 memory used for DFS stack (-m10000)
2.539 total actual memory usage
pan: elapsed time 0.034 seconds
pan: rate 647.05882 states/second
I have a very simple piece of c code which looks like this :
int x = 0;
void increment()
{
x++;
return;
}
I have embedded this in a promela code. Essentially, I call this 'increment' function from my promela code. And at the same time, I want an assertion violation (or a never claim violation) when x reached a particular value, 5 let's say. The promela code I have written looks something like this :
c_code{
#include "ccode.c" /* the c code written above */
}
bool badstate = false;
active proctype driver()
{
do
:: (1) ->
c_code{
increment();
}
if
:: c_expr{ x == 5 } ->
badstate = true;
:: else ->
skip;
fi;
od;
}
I have added the never claim for the LTL formula "<>badstate", but it does not seem to work.
I think my code has a problem in accessing the variables defined in the code from my promela code. I can't seem to find a way to figure this out. Please help.
Thanks and Regards.
Madhukar