Frama-C crashed with an unexpected error Abstract_interp.Error_Bottom
Steps to reproduce the issue
I ran frama-c with these parameters:
frama-c -eva -slevel 100 -plevel 255 -eva-precision 5 -val-warn-undefined-pointer-comparison pointer -no-val-alloc-returns-null -warn-signed-overflow -val -no-val-show-progress -machdep x86_64 4ee67af5850fa1e85ef52301e74c7093eba28573.cand 4ee67af5850fa1e85ef52301e74c7093eba28573.c is the following program:
__attribute__((noinline)) int
f (int a, int b, int d)
{
int r = 8;
b += d + 42 -((short)((((int)(b)) %((int)(d)))))-((short)((((int)(b)) >>((int)(b))))) + 42 -((short)((((int)(b)) %((int)(d + 42 -((short)((((int)(b)) %((int)(d)))))-((short)((((int)(b)) >>((int)(b))))))))))-((short)((((int)(b)) >>((int)(b)))));
r = b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))) + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) %((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))-((long)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) ^((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))+((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) &((int)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) >>((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))-((short)((((int)(r)) >>((int)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) >>((int)(r)))))+((long)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) &((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))));
return r;
}
int
main (void)
{
int l = 8;
asm ("" : "=r" (l) : "0" ((-(-2))));
if (((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))) != -(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))) + 42 -((short)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) %((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))+((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))) &((int)(((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))-((short)((((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) &((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))-((short)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3))))))))) |((int)(((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))+((short)((((int)(((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))) &((int)(((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))))))*((int)((((int)(((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) <<((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))))))-((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3))))))))) %((int)(((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3))))))))))))+((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) |((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))))
return 0;
}Expected behaviour
Not to crash.
Actual behaviour
The program crashed with this trace:
[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
Please use -eva-slevel instead.
[kernel] Warning: -plevel is a deprecated alias for option -eva-plevel.
Please use -eva-plevel instead.
[kernel] Warning: -val-warn-undefined-pointer-comparison is a deprecated alias
for option -eva-warn-undefined-pointer-comparison.
Please use -eva-warn-undefined-pointer-comparison instead.
[kernel] Warning: -no-val-alloc-returns-null is a deprecated alias
for option -eva-no-alloc-returns-null.
Please use -eva-no-alloc-returns-null instead.
[kernel] Warning: -val is a deprecated alias for option -eva. Please use -eva instead.
[kernel] Warning: -no-val-show-progress is a deprecated alias for option -eva-no-show-progress.
Please use -eva-no-show-progress instead.
[kernel] Parsing 4ee67af5850fa1e85ef52301e74c7093eba28573.c (with preprocessing)
[eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
option -eva-min-loop-unroll set to 0 (default value).
option -eva-auto-loop-unroll set to 128.
option -eva-widening-delay set to 3 (default value).
option -eva-partition-history set to 0 (default value).
option -eva-slevel already set to 100.
option -eva-ilevel set to 48.
option -eva-plevel already set to 255 (not modified).
option -eva-subdivide-non-linear set to 100.
option -eva-remove-redundant-alarms set to true (default value).
option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
option -eva-split-return set to 'auto'.
option -eva-equality-through-calls set to 'formals' (default value).
option -eva-octagon-through-calls set to false (default value).
[eva] Splitting return states on:
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:17: Warning:
signed overflow. assert l + (int)(-((int)(-6))) ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
division by zero. assert d ≢ 0;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
invalid RHS operand for shift. assert 0 ≤ b < 32;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow. assert d + 42 ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert -2147483648 ≤ (int)(d + 42) - (int)((short)((int)(b % d)));
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert (int)(d + 42) - (int)((short)((int)(b % d))) ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
division by zero.
assert
(int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
(int)((short)((int)(b >> b))))
≢ 0;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert
(int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
(int)((short)((int)(b >> b))))
+ 42 ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert
b +
(int)((int)((int)((int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
(int)((short)((int)(b >> b))))
+ 42)
-
(int)((short)((int)(b %
(int)((int)((int)(d + 42) -
(int)((short)((int)(b % d))))
- (int)((short)((int)(b >> b))))))))
- (int)((short)((int)(b >> b))))
≤ 2147483647;
[kernel] Current source was: 4ee67af5850fa1e85ef52301e74c7093eba28573.c:8
The full backtrace is:
Raised at file "src/kernel_services/abstract_interp/ival.ml", line 267, characters 14-32
Called from file "src/kernel_services/abstract_interp/ival.ml", line 281, characters 16-30
Called from file "src/plugins/value/domains/octagons.ml", line 352, characters 11-43
Called from file "src/plugins/value/domains/octagons.ml", line 360, characters 8-74
Called from file "src/plugins/value/domains/octagons.ml", line 395, characters 19-48
Called from file "src/plugins/value/domains/octagons.ml", line 1054, characters 6-77
Called from file "src/plugins/value/domains/domain_product.ml", line 94, characters 6-42
Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
Called from file "src/plugins/value/engine/evaluation.ml", line 837, characters 36-73
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 907, characters 6-33
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 907, characters 6-33
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 1103, characters 6-36
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 664, characters 25-60
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 602, characters 21-38
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 618, characters 23-76
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 685, characters 17-73
Called from file "src/plugins/value/engine/evaluation.ml" (inlined), line 1148, characters 4-67
Called from file "src/plugins/value/engine/evaluation.ml", line 1509, characters 23-77
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 157, characters 14-59
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 177, characters 4-54
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 251, characters 10-55
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 233, characters 28-33
Called from file "src/plugins/value/engine/iterator.ml", line 261, characters 4-60
Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 221, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 318, characters 10-43
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 456, characters 22-60
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 758, characters 26-75
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 754, characters 10-447
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 769, characters 24-59
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 742, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 274, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 333, characters 25-75
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Abstract_interp.Error_Bottom).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugsContextual information
- Frama-C installation mode: Opam
- Frama-C version: Frama-C version (as reported by
frama-c -version) 22.0 (Titanium) - Plug-in used: eva
- OS name: Ubuntu
- OS version: 18
Additional information (optional)
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information