Skip to content

cdizy might not terminate #2

Open
@ClearlyClaire

Description

@ClearlyClaire
Contributor

Good evening,
I stumbled over a case where cdizy seems to enter an infinite loop.
It is most probably due to widening being incorrectly applied (or fixed-point incorrectly detected), but I haven't been able to track it down yet.

In any case, here is an example exhibiting such behavior:

typedef short Guard;

int res;
int T_res;

void test(int a, int b)
{
    Guard Ret = 0;
    Guard T_Ret = 0;

    int T_a = a;
    int T_b = b;

    int x;
    int T_x;

    if (!Ret) x = a + 2 * b;
    if (!T_Ret) T_x = T_a + 2 * T_b;

L1:;
    Guard G0 = 1;
    Guard T_G0 = 1;
    if (!T_Ret) T_G0 = (1 <= T_b);
    if (!Ret) G0 = (1 <= a);

    if (!T_Ret) if (T_G0) T_x = T_x + 1;
    if (!T_Ret) if (T_G0) T_b = T_b - 1;
    if (!Ret) if (G0) x = x + 1;
    if (!Ret) if (G0) a = a - 1;

    if (!Ret) if (G0) goto L1;
    if (!T_Ret) if (T_G0) goto L1;

    res = x;
    T_res = T_x;

    {char *CP7;}
}

Activity

nimrodpar

nimrodpar commented on Apr 7, 2015

@nimrodpar
Contributor

This is a widening issue. I will further investigate but for now: dizy does finish with -w_s=all (precision is poor of course...)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

      Development

      No branches or pull requests

        Participants

        @ClearlyClaire@nimrodpar

        Issue actions

          cdizy might not terminate · Issue #2 · tech-srl/differential