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

Actions

Copy link

Bug #5452

open

Removing header "module.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:

11/27/2014

Due date:

% Done:

Estimated time:

Detected in build:

svn

Platform:

Published in build:

Description

After removing header <linux/module.h> from rule models section "before: file ("$this")" leads to BLAST exception:

Exception raised :(Not_found
Ack! The gremlins again!: Not_found
Ack! The gremlins again!: Not_found
Fatal error: exception Not_found
Exit code: 2.

Possible command for BLAST execution:
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

This issue was revealed at fixed rule models 10_1a, 43_1a, 77_1a, 134_1a.
Also this issue is presented in current rule models 129_1a, 146_1a, 147_1a.

Files

blast_fail.tar (206 KB) blast_fail.tar

Vitaly Mordan, 11/27/2014 04:58 PM

Related issues 1 (1 open — 0 closed)