Project

General

Profile

Actions
Copy link

Bug #5397

open

BLAST error trace converter misses the last line of the error trace

Added by Vadim Mutilin over 9 years ago. Updated over 9 years ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
-
Start date:
10/28/2014
Due date:
% Done:

0%

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

Description

For example example0.tokens.c
It misses point of __VERIFIER_error() call (Location: id=0#5 src="example0.c"; line=7). 

                                                Location: id=0#1 src="example0.c"; line=0
                                                Location: id=0#1 src="example0.c"; line=0
FunctionCall(__BLAST_initialize_example0.c())
Locals:
                                                Location: id=1#1 src="example0.c"; line=0
   Block(Return(0);)
Skip
                                                Location: id=0#3 src="example0.c"; line=4
Block(a@main = 1;c@main = 1;)
                                                Location: id=0#4 src="example0.c"; line=6
Pred(a@main  !=  0)
                                                Location: id=0#5 src="example0.c"; line=7

After blast converter

Error trace common format v0.1

"example0.c" CALL INIT : __BLAST_initialize_example0.c()
RETURN
CALL ENTRY
4 BLOCK : a = 1;c = 1;
6 ASSUME : a != 0

Original program

extern void __VERIFIER_error(void);

int main() {
    int a = 1;
    int c = 1 || (a = 0);
    if (a) {
      __VERIFIER_error();
      return 1;
    }
    return 0;
}

Actions
Copy link
 #1

Updated by Evgeny Novikov over 9 years ago

I don't see the __VERIFIER_error() call in the original BLAST error trace. The convertor isn't a God to create it.

Actions
Copy link
 #2

Updated by Vadim Mutilin over 9 years ago

The final ERROR location is before the call, and not the call itself.
It is competition settings where ERROR location is defined by __VERIFIER_error() function call.

Actions
Copy link
 #3

Updated by Vadim Mutilin over 9 years ago

BLAST error trace is always ends by location,
the same as in competition error trace format http://www.sosy-lab.org/~dbeyer/cpa-witnesses/

Actions
Copy link

Also available in: Atom PDF