Assertion failure in llreve-dynamic

[mattulbrich]

Hej,

I tried to use the llreve-dyamic tool on the following example:

extern int __mark(int);

void send(int *to, int *from, int count)
{
    do {                          /* count > 0 assumed */
        *to = *from++;
    } while(__mark(1) & (--count > 0));
}
extern int __mark(int);

and

void send(int *to, int *from, int count)
{
    int n = (count + 7) / 8;
    switch (count % 8) {
    case 0: do { *to = *from++;
    case 7:      *to = *from++;
    case 6:      *to = *from++;
    case 5:      *to = *from++;
    case 4:      *to = *from++;
    case 3:      *to = *from++;
    case 2:      *to = *from++;
    case 1:      *to = *from++;
            } while (__mark(1) & (--n > 0));
    }
}

which are duff1.c and duff2.c. Invoking llreve-dynamic gives a seg fault.

$ ./llreve-dynamic -patterns ../../patterns/looppatterns ~/duff1.c ~/duff2.c 
Found 4 patterns
(_ ≥ _)
(_ > _)
(_ < 0)
(_ ≥ 0)
MAIN: 1
startMark: -1
endMark: 0
function 1: send
function 2: send
---
Found counterexample:
starting at mark -1
ending at mark 0
 5
 5
HEAP$1_old
background: 0
HEAP$2_old
background: 0
llreve-dynamic: /home/ubuntu/src/llreve/reve/dynamic/llreve-dynamic/include/llreve/dynamic/Integer.h:69: Integer &Integer::operator+=(const Integer &): Assertion `type == other.type' failed.
Aborted (core dumped)

[cocreature]

I am unable to reproduce this. At which commit did you build llreve-dynamic?

[cocreature]

Not useful now, since you have already built your executable but for future bugreports you can now just run llreve-dynamic --version to see the git revision used to build it. llreve itself supported this for some time but I forgot to add it to llreve-dynamic as well.