search

Practical-Formal-Methods / adiff

Tool for differentially testing soundness and precision of program analyzers
MIT License
11 stars 6 forks source link

Bug: exp06 got stuck #101

Closed chkl closed 6 years ago

chkl commented 6 years ago

output (might be related)

/tmp/kleedir5281/program.c:2228:67: warning: '&&' within '||' [-Wlogical-op-parentheses]
    else if (a2 == 4 && (input == 6 && (a29 <= -144 || -144 < a29 && -16 >= a29)) && (-86 < a4 && -42 >= a4) && (-147 < a0 && -98 >= a0))
                                                    ~~ ~~~~~~~~~~~^~~~~~~~~~~~~
/tmp/kleedir5281/program.c:2228:67: note: place parentheses around the '&&' expression to silence this warning
    else if (a2 == 4 && (input == 6 && (a29 <= -144 || -144 < a29 && -16 >= a29)) && (-86 < a4 && -42 >= a4) && (-147 < a0 && -98 >= a0))
                                                                  ^
                                                       (                       )
/tmp/kleedir5281/program.c:2236:79: warning: '&&' within '||' [-Wlogical-op-parentheses]
    else if (a2 == 5 && (-86 < a4 && -42 >= a4 && ((a29 <= -144 || -144 < a29 && -16 >= a29 || -16 < a29 && 43 >= a29) && input == 5)) && a0 <= -147)
                                                                ~~ ~~~~~~~~~~~^~~~~~~~~~~~~
/tmp/kleedir5281/program.c:2236:79: note: place parentheses around the '&&' expression to silence this warning
    else if (a2 == 5 && (-86 < a4 && -42 >= a4 && ((a29 <= -144 || -144 < a29 && -16 >= a29 || -16 < a29 && 43 >= a29) && input == 5)) && a0 <= -147)
                                                                              ^
                                                                   (                       )
/tmp/kleedir5281/program.c:2236:106: warning: '&&' within '||' [-Wlogical-op-parentheses]
    else if (a2 == 5 && (-86 < a4 && -42 >= a4 && ((a29 <= -144 || -144 < a29 && -16 >= a29 || -16 < a29 && 43 >= a29) && input == 5)) && a0 <= -147)
                                                                                            ~~ ~~~~~~~~~~^~~~~~~~~~~~
/tmp/kleedir5281/program.c:2236:106: note: place parentheses around the '&&' expression to silence this warning
    else if (a2 == 5 && (-86 < a4 && -42 >= a4 && ((a29 <= -144 || -144 < a29 && -16 >= a29 || -16 < a29 && 43 >= a29) && input == 5)) && a0 <= -147)
                                                                                                         ^
                                                                                               (                     )
/tmp/kleedir5281/program.c:2244:78: warning: '&&' within '||' [-Wlogical-op-parentheses]
    else if (a2 == 4 && (a0 <= -147 && (-86 < a4 && -42 >= a4 && ((-16 < a29 && 43 >= a29 || 43 < a29) && input == 3))))
                                                                   ~~~~~~~~~~^~~~~~~~~~~~ ~~
/tmp/kleedir5281/program.c:2244:78: note: place parentheses around the '&&' expression to silence this warning
    else if (a2 == 4 && (a0 <= -147 && (-86 < a4 && -42 >= a4 && ((-16 < a29 && 43 >= a29 || 43 < a29) && input == 3))))
                                                                             ^
                                                                   (                     )
301 warnings generated.

It's probably not related. The problem is that it vdiff is taking up 17.8G of memory.

chkl commented 6 years ago

Program c/termination-crafted-lit-todo/ChenFlurMukhopadhyay-SAS2012-Ex2.01_true-termination.c seems to cause excessive memory usage.

chkl commented 6 years ago

Somehow language-c creates some recursive value (probably because of the typdef in the file). So this will be a won't fix, probably.