MOPSA missing a warning
Dear all,
please consider the program below:
extern int __VERIFIER_nondet_int(void);
int main() {
int a = __VERIFIER_nondet_int();
_mopsa_assume(a <= 1);
double x = a / 2.0;
int cond = 2 * x >= 0.0;
_mopsa_assert(x <= 0.0);
return 0;
}
When calling ~/mopsa-analyzer/bin/mopsa -config ~/mopsa-analyzer/share/mopsa/configs/c/default.json test.c, there's no warning about the assertion printed even tough it is unsafe (for e.g. a=1).
I'm working with version 1.0~pre2 .