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 about 10 years ago. Updated about 10 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 about 10 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 about 10 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 about 10 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