Open-Source Projects

08/03/2013

10:58 PM Linux Driver Verification Bug #1312: Timeout script sometimes fails with "No child processes" message

If wait is interrupted by a signal, it will return EINTR rather than ECHILD. In any case, the SIGALRM can arrive bet... Pavel Shved

12:29 PM Linux Driver Verification Bug #1312: Timeout script sometimes fails with "No child processes" message

FYI, it was a race condition between waitpid and alarm. If wait4 syscall reaps the child process, but alarm is deliv... Pavel Shved

01/02/2013

09:22 AM Linux Driver Verification Bug #3834: SMT sovler answer is strange: Error: Invalid top level command.

Did you follow this piece of instructions from the README file?... Pavel Shved

11/07/2012

11:38 AM BLAST Support #3662: Blast documentation?

Vadim Mutilin wrote:
> For *Linux drivers* we use options
> -predH 7 -lattice -include-lattice symb -include-latti... Pavel Shved

04/04/2012

11:51 PM BLAST Bug #2705 (Open): BLAST knows something about huge integer numbers?

OCaml doesn't support unsigned 64-bit integers. The maximum value of an integer constant is 2⁶³. See "the documenta... Pavel Shved

07:52 PM BLAST Bug #2705: BLAST knows something about huge integer numbers?

Did you try using -sv-comp flag? Pavel Shved

11:06 PM BLAST Bug #2699: BLAST doesn't find an error in a rather simple example with division

CSIsat interpolating prover doesn't seem to support division. BLAST replaces the division by an uninterpreted funct... Pavel Shved

03/25/2012

07:42 PM BLAST Bug #2264 (Closed): Improve descriptions of legitimate exceptions

Yes, that's pretty much everything I planned for this feature. Pavel Shved

02/19/2012

10:40 PM BLAST blast-2.7.1-bin-i686.tgz

Binary distribution of BLAST 2.7.1 for i686 Pavel Shved

10:37 PM BLAST blast-2.7.1-bin-x86_64.tgz

Binary distribution of BLAST 2.7.1 for x86_64 Pavel Shved