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

Also available in: Atom PDF