Project

General

Profile

Actions

Bug #3514

open

LRALogic.C:614: void LRALogic::splitTermToVarAndConst(const PTRef&, PTRef&, PTRef&): Assertion `isRealTimes(term) || isRealDiv(term) || isRealVar(term) || isConstant(term)' failed.

Added by Karine Even Mendoza about 8 years ago. Updated over 7 years ago.

Status:
Resolved
Priority:
Normal
Start date:
30/09/2016
Due date:
% Done:

0%

Estimated time:

Description

Code example: hi-bench/main-bench/funfrog_regression/03_simple/main7.c --show-error-trace --unwind 10

Error:
Checking claims in program...
; Warning: disabling SATElite preprocessing to track proof
; Warning: disabling SATElite preprocessing to track proof
Checking Claim #1 (100%) ...
Last assertion location: 30 / 36 ( 3)
  • INLINING function: c::__CPROVER_initialize
  • INLINING function: c::main
    Processing a deferred function: c::__CPROVER_initialize
    Processing a deferred function: c::main
  • INLINING function: c::strncpy
    Processing a deferred function: c::strncpy
    Unwinding loop c::strncpy.0 iteration 1 file main7.c line 7 function strncpy thread 0
    Unwinding loop c::strncpy.0 iteration 2 file main7.c line 7 function strncpy thread 0
    Unwinding loop c::strncpy.0 iteration 3 file main7.c line 7 function strncpy thread 0
    Unwinding loop c::strncpy.0 iteration 4 file main7.c line 7 function strncpy thread 0
    Unwinding loop c::strncpy.0 iteration 5 file main7.c line 7 function strncpy thread 0
    Unwinding loop c::strncpy.0 iteration 6 file main7.c line 7 function strncpy thread 0
    Unwinding loop c::strncpy.0 iteration 7 file main7.c line 7 function strncpy thread 0
    Unwinding loop c::strncpy.0 iteration 8 file main7.c line 7 function strncpy thread 0
    Unwinding loop c::strncpy.0 iteration 9 file main7.c line 7 function strncpy thread 0
    Unwinding loop c::strncpy.0 iteration 10 file main7.c line 7 function strncpy thread 0
    SYMEX TIME: 0.028
    All SSA steps: 245
    Ignored SSA steps after slice: 164
    SLICER TIME: 0.001
    evolcheck: LRALogic.C:614: void LRALogic::splitTermToVarAndConst(const PTRef&, PTRef&, PTRef&): Assertion `isRealTimes(term) || isRealDiv(term) || isRealVar(term) || isConstant(term)' failed.
    Aborted (core dumped)
This is the code:
  • strncpy example */
    //#include <stdio.h>
    //#include <string.h>
    #define LEN 2

char *strncpy (char *dest, const char *src, int n) {
for (int i = 0; i < n; ++i) {
*dest = *src;
if (!*src)
return dest;
++dest;
++src;
}
return dest;
}

int main () {
char str1[]= "To be ";
char str2[LEN];
strncpy (str2,str1,LEN-1);

assert('T' == str1[0]);
//puts (str2);
return 0;
}

I don't think hifrog-lra can cop with it now, and so I expected to have an error from hifrog (or warning) not from opensmt2. Any idea what could be the reason?

Thanks,
Karine

Actions

Also available in: Atom PDF