Project

General

Profile

Actions
Copy link

Bug #5469

open

Removing header "slab.h" from rule models leads to BLAST exception

Added by Vitaly Mordan almost 10 years ago. Updated almost 10 years ago.

Status:
New
Priority:
Normal
Assignee:
Vadim Mutilin
Category:
BLAST
Start date:
12/04/2014
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

BLAST fails with exception at module drivers/block/aoe/aoe.ko, main4, rule 77_1a after removing unused header linux/slab.h:

Next iteration of model-check's big while-loop
3031
Now processing tree node:
No error found at this node
Exception raised :(Failure("Attempt to take the union of a structure value and a non-structure value")

Command to reproduce:

res-manager -d ldv -m 15Gb -t 15min /home/ldvuser/ldv/inst/dscv/rcv/backends/blast/bin/ocamltune /home/ldvuser/ldv/inst/dscv/rcv/backends/blast/bin/pblast.opt blast_fail/* -predH 7 -craig 2 -ignoredupfn -nosserr -enable-recursion -nolabelmeanssafe -main ldv_main3_sequence_infinite_withcheck_stateful -L LDV_ERROR -cldepth 0 -alias "" -lattice -include-lattice symb -stop-sep -merge bdd

Processing common model files with CIF doesn't solve this problem.

Files

blast_fail.tar (280 KB) blast_fail.tar Vitaly Mordan, 12/04/2014 07:16 PM

Related issues 1 (1 open — 0 closed)

Related to Linux Driver Verification - Bug #5452: Removing header "module.h" from rule models leads to BLAST exceptionNewVadim Mutilin11/27/2014

Actions
Actions
Copy link

Also available in: Atom PDF