航空资料41(95)

曝光台 注意防骗 网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者

x in [0.18999993, 0.41680009]
fltloop.c:3.2-9.3:up iteration #3
x in [0.18999993, 1.0000002]
...
Antoine Min´e Building a specialized static analyzer p. 40 / 112
Design of Astr´ee Iterator
Loop analysis example
fltloop.c
1 void main() {
2 float x = 0.1;
3 while (1) {
4 int r;
5 if (r) x = 0.2; else x = 0.9*x + 0.1;
6 __ASTREE_log_vars((x;interv));
7 }
8 }
Analysis result
fltloop.c:3.2-9.3:up iteration #4
x in [0.18999993, 1.0000002]
fltloop.c:3.2-9.3:up iteration #5
x in [0.18999993, 1.0000002]
%
Antoine Min´e Building a specialized static analyzer p. 40 / 112
Design of Astr´ee Iterator
Improved loop analysis
Actually, Astr´ee performs more complex iterations:
unrolls the first iterations
(separate analysis of initialization)
performs increasing iterations with widening
performs decreasing iterations after stabilisation
(improves the fixpoint)
alarms are printed in a final checking iteration
Loop analysis can be configured by command-line options
Antoine Min´e Building a specialized static analyzer p. 41 / 112
Design of Astr´ee Iterator
Loop unrolling example
initloop.c
1 void main() {
2 int I = 1, x;
3 while (1) {
4 __ASTREE_log_vars((I, x; interv));
5 if (I) { x = 0; I = 0; }
6 else { x++; if (x > 100) x = 0; }
7 }
8 }
Antoine Min´e Building a specialized static analyzer p. 43 / 112
Design of Astr´ee Iterator
Loop unrolling example
initloop.c
1 void main() {
2 int I = 1, x;
3 while (1) {
4 __ASTREE_log_vars((I, x; interv));
5 if (I) { x = 0; I = 0; }
6 else { x++; if (x > 100) x = 0; }
7 }
8 }
Analysis result without unrolling
% astree initloop.c --exec-fn main --unroll 0
| egrep "iteration| in|WARN"
I in {1}, x in [-2147483648, 2147483647]
...
Antoine Min´e Building a specialized static analyzer p. 43 / 112
Design of Astr´ee Iterator
Loop unrolling example
initloop.c
1 void main() {
2 int I = 1, x;
3 while (1) {
4 __ASTREE_log_vars((I, x; interv));
5 if (I) { x = 0; I = 0; }
6 else { x++; if (x > 100) x = 0; }
7 }
8 }
Analysis result without unrolling
initloop.c:3.2-7.3:up iteration #0
I in [0, 1], x in [-2147483648, 2147483647]
initloop.c:3.2-7.3:up iteration #1
I in [0, 1], x in [-2147483648, 2147483647]
...
Antoine Min´e Building a specialized static analyzer p. 43 / 112
Design of Astr´ee Iterator
Loop unrolling example
initloop.c
1 void main() {
2 int I = 1, x;
3 while (1) {
4 __ASTREE_log_vars((I, x; interv));
5 if (I) { x = 0; I = 0; }
6 else { x++; if (x > 100) x = 0; }
7 }
8 }
Analysis result without unrolling
initloop.c:3.2-7.3:down iteration #0
I in [0, 1], x in [-2147483648, 2147483647]
initloop.c:6.11-14::[call#main@1:]: WARN: signed int
arithmetic range [-2147483647, 2147483648]
not included in [-2147483648, 2147483647]
%
Antoine Min´e Building a specialized static analyzer p. 43 / 112
Design of Astr´ee Iterator
Loop unrolling example
initloop.c
1 void main() {
2 int I = 1, x;
3 while (1) {
4 __ASTREE_log_vars((I, x; interv));
5 if (I) { x = 0; I = 0; }
6 else { x++; if (x > 100) x = 0; }
7 }
8 }
Antoine Min´e Building a specialized static analyzer p. 43 / 112
Design of Astr´ee Iterator
Loop unrolling example
initloop.c
1 void main() {
2 int I = 1, x;
3 while (1) {
4 __ASTREE_log_vars((I, x; interv));
5 if (I) { x = 0; I = 0; }
6 else { x++; if (x > 100) x = 0; }
7 }
8 }
Analysis result with unrolling
% astree initloop.c --exec-fn main --unroll 1
| egrep "iteration| in|WARN" -B 1
loop@3=1: I in {1}, x in [-2147483648, 2147483647]
...
Antoine Min´e Building a specialized static analyzer p. 43 / 112
Design of Astr´ee Iterator
Loop unrolling example
initloop.c
1 void main() {
2 int I = 1, x;
3 while (1) {
4 __ASTREE_log_vars((I, x; interv));
5 if (I) { x = 0; I = 0; }
6 else { x++; if (x > 100) x = 0; }
7 }
8 }
Analysis result with unrolling
loop@3>=2: I in {0}, x in {0}
initloop.c:3.2-7.3:up iteration #0
loop@3>=2: I in {0}, x in [0, 1]
initloop.c:3.2-7.3:up iteration #1
...
Antoine Min´e Building a specialized static analyzer p. 43 / 112
　
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：航空资料41(95)