Bug #5469: Removing header "slab.h" from rule models leads to BLAST exception - Linux Driver Verification - Open-Source Projects

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:

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)