Actions
Feature #3204
closedDo not use BLAST specific in models and special LDV subroutines
Start date:
07/13/2012
Due date:
% Done:
0%
Estimated time:
Published in build:
1f558ed
Description
When there was just BLAST static verifier, we created models for this engine. We use 'blast' in model names, in models itself, in general subroutines (primarily via "engine-blast.h" and "engine-blast-assert.h" headers).
But some time ago we began to use CPAchecker static verifier. And we have heard questions like: "Why is CPAchecker fails when blast_assert() function is called?" and so on.
I have developed a special general header defining special LDV subroutines ("ldv.h"). And I'm going to remove any BLAST specific from models while fixing issue #453 that touches all models anyway.
Actions