[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Problems

Dear Galina Teneva,

PVS integers are the mathematical integers, and hence unbounded.

If you want a bounded fragment, use a subrange such as
 machine_int: TYPE = subrange(-32768,32767)
(If I remember correctly, that's the 16 bits 2s complement range).
If you want an actual bit representation, use the bitvectors library.

We can't check the parser error without more of the files: use
M-x smail-pvs-files.

John Rushby