Project

General

Profile

Actions
Copy link

Bug #507

open

SMT sovler could not parse the request (Error: Undefined name)

Added by Vadim Mutilin about 14 years ago. Updated over 13 years ago.

Status:
New
Priority:
Low
Assignee:
-
Category:
-
Target version:
-
Start date:
10/27/2010
Due date:
% Done:

0%

Estimated time:
Detected in build:
ebfe9ed48e0684365a6f8aacb0b8c22e82157b8a
Platform:
Linux x86
Published in build:

Description

Blast fails with exception
ZZZ: Exception: Failure("SMT sovler answer is strange: Error: Undefined name \"-1073741824\".")
on the attached driver.

Command line:
LDV_DEBUG=100 BLAST_EXP_NOALIAS=1 RCV_TIMELIMIT=900 RCV_MEMLIMIT=1800000 BLAST_SOLVER=yices BLAST_OPTIONS="-devdebug" ldv-manager tag=current envs=linux-2.6.31.6.tar.bz2 drivers=wl12xx.ko.tar.bz2 "rule_models=32_7"

If comment the following line in spi.c then the result will be unsafe.

void wl12xx_spi_read(struct wl12xx *wl, int addr, void *buf,
            size_t len)
...
   //cmd |= WSPI_CMD_READ;

Files

wl12xx.ko.tar.bz2 (50.2 KB) wl12xx.ko.tar.bz2 extracted driver with bug Vadim Mutilin, 10/27/2010 04:23 PM
Actions
Copy link
 #1

Updated by Pavel Shved about 14 years ago

I ran this, but I nothing actually happened...

Actions
Copy link
 #2

Updated by Alexey Khoroshilov almost 14 years ago

Can it be reproduced now?

Actions
Copy link
 #3

Updated by Vadim Mutilin almost 14 years ago

  • Priority changed from Normal to Low

It appeared only on my old 32 bit OS.

Actions
Copy link
 #4

Updated by Pavel Shved almost 14 years ago

  • Category set to BLAST
  • Platform set to Linux x86

Heh, we even have a special "Platform" field to demonstrate this. :)

Actions
Copy link
 #5

Updated by Pavel Shved over 13 years ago

  • Project changed from Linux Driver Verification to BLAST
  • Category deleted (BLAST)
Actions
Copy link

Also available in: Atom PDF