Spinroot

Hi,

I'am using spin version 6.1.0 on Windows and tried to verify a simple safety property. Therefore I run spin with the -a flag and compile the generated pan.c file with the switches -DBITSTATE -DSAFETY. When I run the verification of the example below, the result (if an counter example was found or not) depends on several settings.

- If the compile switch SAFETY is used or not
- if the variable 'r1' is at the global scope or in the scope of process 'all'
- the data type of the variable 'NR1' (bool or int)

I'am a bit confused about this. It seems to me that in some settings a full verifaction is not done although I run the verifier in this mode (I do not use any options when running the generated verifier).

Could you please have a look at my small piece of promela code and give me some hints what I'am doing wrong here?

Here is the promela code:

int REG_2;
hidden int TMP_VALUE;
byte MEMORY[2];
int NR1 = 0;
byte r1;

init
{
  atomic {
    run all();
  }
}

inline write() {
  select(r1: 0..255);
  MEMORY[0] = r1;

  select(r1: 0..255);
  MEMORY[1] = r1;
}

proctype all()
{
  write();
  d_step {
    TMP_VALUE = (MEMORY[0] << 8);
    TMP_VALUE = (TMP_VALUE | MEMORY[1]);
    REG_2 = TMP_VALUE;
  }
  write();
  if
    ::(REG_2 != 42) ->   goto BB0_2;
    ::else -> skip
  fi;

  NR1 = 1;

BB0_2:
    skip;
}

never {
    do
       ::skip
       ::NR1 == 1 -> break;
    od;
}

The promela parser seems not to read the smallest integer value (32 bit) correctly. In the following example spin will print out
-2147483647.

int v;

proctype all() {
  v = -2147483648;
  printf("%d\n", v);
}
init
{
run all();
}