diff --git a/tests/constant_propagation/array_pointers.i b/tests/constant_propagation/array_pointers.i index 5f2d17c28f129708156e261807464f616cacdecc..41762ffb56af1f94772c5ff55c58392c451537bb 100644 --- a/tests/constant_propagation/array_pointers.i +++ b/tests/constant_propagation/array_pointers.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-eva" + STDOPT: #"-eva" */ void *p; diff --git a/tests/constant_propagation/const_field_return_struct.i b/tests/constant_propagation/const_field_return_struct.i index 6b4473198a227ba1a1c6ca5835d2706c1441d847..6fdf85d653e586a12ac070adfefd583a2136d7d0 100644 --- a/tests/constant_propagation/const_field_return_struct.i +++ b/tests/constant_propagation/const_field_return_struct.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-eva" + STDOPT: #"-eva" */ struct S { diff --git a/tests/constant_propagation/const_globals.c b/tests/constant_propagation/const_globals.c index c0661d55d4f2a4006517e7881ef04f181f7ea550..ccbe6326b6dbacd1967309c2c236e8791f7d54b9 100644 --- a/tests/constant_propagation/const_globals.c +++ b/tests/constant_propagation/const_globals.c @@ -1,7 +1,7 @@ /* run.config + PLUGIN: OPT: -constfold -print -machdep x86_32 */ - #include <stddef.h> typedef const size_t const_size_t; diff --git a/tests/constant_propagation/const_propagate.c b/tests/constant_propagation/const_propagate.c index c9a65bcc33bc3291cde3802cb13e8a9dd5d0022b..509ebe2185954346cf60c974496704d1df99b51f 100644 --- a/tests/constant_propagation/const_propagate.c +++ b/tests/constant_propagation/const_propagate.c @@ -1,8 +1,8 @@ /* run.config -PLUGIN: @CONSTANT_PROPAGATION_PLUGINS@ from inout - OPT: -eva @EVA_OPTIONS@ -deps -out -input -scf + OPT: -eva @EVA_OPTIONS@ -deps -out -input -then -scf OPT: -scf @EVA_OPTIONS@ -main init -cast-from-constant -semantic-const-fold add3 */ + int x,y,z, TAB[10]; struct st { int a, b ; } s1, s2; typedef struct st ST ; diff --git a/tests/constant_propagation/declaration2.c b/tests/constant_propagation/declaration2.c index cfde5c962b55e8486361ddbb4d15852764d0f956..aa830c74e4e7671c6ddeca0c028a0040d66426c6 100644 --- a/tests/constant_propagation/declaration2.c +++ b/tests/constant_propagation/declaration2.c @@ -1,5 +1,5 @@ /* run.config - OPT: -eva @EVA_OPTIONS@ -scf + OPT: -eva @EVA_OPTIONS@ -then -scf */ void f(int *x) { (*x)++; } diff --git a/tests/constant_propagation/introduction_of_non_explicit_cast.c b/tests/constant_propagation/introduction_of_non_explicit_cast.c index bd95af567f0900dc0a96bf490449d0af886ffd6a..8db347548927dc2510a5e2eb8df566d51fa89d1a 100644 --- a/tests/constant_propagation/introduction_of_non_explicit_cast.c +++ b/tests/constant_propagation/introduction_of_non_explicit_cast.c @@ -1,8 +1,9 @@ /* run.config - MODULE: @PTEST_NAME@ + MODULE: @PTEST_NAME@ OPT: -eva @EVA_OPTIONS@ -deps */ + int x,y,z; int TAB[10]; struct st { int a, b ; } s1, s2; diff --git a/tests/constant_propagation/oracle/const_propagate.0.res.oracle b/tests/constant_propagation/oracle/const_propagate.0.res.oracle index db357d9854128a8478c40bb11cd1c3c131b85360..72a698cc3999064713e38b479d33ae68636600ae 100644 --- a/tests/constant_propagation/oracle/const_propagate.0.res.oracle +++ b/tests/constant_propagation/oracle/const_propagate.0.res.oracle @@ -128,6 +128,107 @@ p ∈ {{ &x }} q ∈ {{ &x ; &y }} yy ∈ {7} +[from] Computing for function add3 +[from] Done for function add3 +[from] Computing for function init +[from] Done for function init +[from] Computing for function test_float_double +[from] Done for function test_float_double +[from] Computing for function test_ptr +[from] Done for function test_ptr +[from] Computing for function test_struct +[from] Done for function test_struct +[from] Computing for function test_struct_ptr +[from] Done for function test_struct_ptr +[from] Computing for function test_tab +[from] Done for function test_tab +[from] Computing for function test_ull +[from] Done for function test_ull +[from] Computing for function main +[from] Done for function main +[from] ====== DEPENDENCIES COMPUTED ====== + These dependencies hold at termination for the executions that terminate: +[from] Function add3: + \result FROM v1; v2; v3 +[from] Function init: + x FROM v + y FROM \nothing + z FROM v + \result FROM \nothing +[from] Function test_float_double: + f1 FROM f0 + f2 FROM f0 + f3 FROM f0 + d1 FROM d0 + d2 FROM d0 + d3 FROM d0 +[from] Function test_ptr: + x FROM v + \result FROM \nothing +[from] Function test_struct: + s1 FROM \nothing + s2 FROM \nothing +[from] Function test_struct_ptr: + \result FROM \nothing +[from] Function test_tab: + TAB[1] FROM TAB[2]; s1.b; s2.b + [4..5] FROM v + s2.b FROM s2.b +[from] Function test_ull: + ull FROM ull +[from] Function main: + x FROM \nothing + y FROM \nothing + z FROM a + TAB[1] FROM TAB[2] + [4..5] FROM \nothing + s1 FROM \nothing + s2 FROM \nothing + ull FROM ull + f1 FROM f0 + f2 FROM f0 + f3 FROM f0 + d1 FROM d0 + d2 FROM d0 + d3 FROM d0 +[from] ====== END OF DEPENDENCIES ====== +[inout] Out (internal) for function add3: + __retres +[inout] Inputs for function add3: + \nothing +[inout] Out (internal) for function init: + x; y; z; zero; sept; z1 +[inout] Inputs for function init: + x; y; z +[inout] Out (internal) for function test_float_double: + f1; f2; f3; d1; d2; d3 +[inout] Inputs for function test_float_double: + f0; f1; f2; d0; d1; d2 +[inout] Out (internal) for function test_ptr: + x; p; s; decal; __retres +[inout] Inputs for function test_ptr: + \nothing +[inout] Out (internal) for function test_struct: + s1; s2; s +[inout] Inputs for function test_struct: + s1.a +[inout] Out (internal) for function test_struct_ptr: + q; __retres +[inout] Inputs for function test_struct_ptr: + \nothing +[inout] Out (internal) for function test_tab: + TAB{[1]; [4..5]}; s2.b; r; q; decal +[inout] Inputs for function test_tab: + TAB[2]; s1.b; s2.b +[inout] Out (internal) for function test_ull: + ull +[inout] Inputs for function test_ull: + ull +[inout] Out (internal) for function main: + x; y; z; TAB{[1]; [4..5]}; s1; s2; ull; f1; f2; f3; d1; d2; d3; b; + p; q; tmp_1; yy +[inout] Inputs for function main: + x; y; z; TAB[2]; s1; s2.b; ull; f0; f1; f2; d0; d1; d2 [scf] beginning constant propagation /* Generated by Frama-C */ struct st { @@ -257,104 +358,3 @@ void main(int a) [scf] constant propagation done -[from] Computing for function add3 -[from] Done for function add3 -[from] Computing for function init -[from] Done for function init -[from] Computing for function test_float_double -[from] Done for function test_float_double -[from] Computing for function test_ptr -[from] Done for function test_ptr -[from] Computing for function test_struct -[from] Done for function test_struct -[from] Computing for function test_struct_ptr -[from] Done for function test_struct_ptr -[from] Computing for function test_tab -[from] Done for function test_tab -[from] Computing for function test_ull -[from] Done for function test_ull -[from] Computing for function main -[from] Done for function main -[from] ====== DEPENDENCIES COMPUTED ====== - These dependencies hold at termination for the executions that terminate: -[from] Function add3: - \result FROM v1; v2; v3 -[from] Function init: - x FROM v - y FROM \nothing - z FROM v - \result FROM \nothing -[from] Function test_float_double: - f1 FROM f0 - f2 FROM f0 - f3 FROM f0 - d1 FROM d0 - d2 FROM d0 - d3 FROM d0 -[from] Function test_ptr: - x FROM v - \result FROM \nothing -[from] Function test_struct: - s1 FROM \nothing - s2 FROM \nothing -[from] Function test_struct_ptr: - \result FROM \nothing -[from] Function test_tab: - TAB[1] FROM TAB[2]; s1.b; s2.b - [4..5] FROM v - s2.b FROM s2.b -[from] Function test_ull: - ull FROM ull -[from] Function main: - x FROM \nothing - y FROM \nothing - z FROM a - TAB[1] FROM TAB[2] - [4..5] FROM \nothing - s1 FROM \nothing - s2 FROM \nothing - ull FROM ull - f1 FROM f0 - f2 FROM f0 - f3 FROM f0 - d1 FROM d0 - d2 FROM d0 - d3 FROM d0 -[from] ====== END OF DEPENDENCIES ====== -[inout] Out (internal) for function add3: - __retres -[inout] Inputs for function add3: - \nothing -[inout] Out (internal) for function init: - x; y; z; zero; sept; z1 -[inout] Inputs for function init: - x; y; z -[inout] Out (internal) for function test_float_double: - f1; f2; f3; d1; d2; d3 -[inout] Inputs for function test_float_double: - f0; f1; f2; d0; d1; d2 -[inout] Out (internal) for function test_ptr: - x; p; s; decal; __retres -[inout] Inputs for function test_ptr: - \nothing -[inout] Out (internal) for function test_struct: - s1; s2; s -[inout] Inputs for function test_struct: - s1.a -[inout] Out (internal) for function test_struct_ptr: - q; __retres -[inout] Inputs for function test_struct_ptr: - \nothing -[inout] Out (internal) for function test_tab: - TAB{[1]; [4..5]}; s2.b; r; q; decal -[inout] Inputs for function test_tab: - TAB[2]; s1.b; s2.b -[inout] Out (internal) for function test_ull: - ull -[inout] Inputs for function test_ull: - ull -[inout] Out (internal) for function main: - x; y; z; TAB{[1]; [4..5]}; s1; s2; ull; f1; f2; f3; d1; d2; d3; b; - p; q; tmp_1; yy -[inout] Inputs for function main: - x; y; z; TAB[2]; s1; s2.b; ull; f0; f1; f2; d0; d1; d2 diff --git a/tests/constant_propagation/oracle/introduction_of_non_explicit_cast.res.oracle b/tests/constant_propagation/oracle/introduction_of_non_explicit_cast.res.oracle index 6473a33045386585cd8c1f35f8466b23286323e4..6d5bb7f553d0a1fb538be91ad3bf27f160c15220 100644 --- a/tests/constant_propagation/oracle/introduction_of_non_explicit_cast.res.oracle +++ b/tests/constant_propagation/oracle/introduction_of_non_explicit_cast.res.oracle @@ -11,41 +11,41 @@ s2 ∈ {0} ull ∈ {0} [eva] computing for function test_ull <- main. - Called from introduction_of_non_explicit_cast.c:68. + Called from introduction_of_non_explicit_cast.c:69. [eva] Recording results for test_ull [eva] Done for function test_ull [eva] computing for function test_struct <- main. - Called from introduction_of_non_explicit_cast.c:69. + Called from introduction_of_non_explicit_cast.c:70. [eva] Recording results for test_struct [eva] Done for function test_struct [eva] computing for function test_struct_ptr <- main. - Called from introduction_of_non_explicit_cast.c:70. + Called from introduction_of_non_explicit_cast.c:71. [eva] Recording results for test_struct_ptr [eva] Done for function test_struct_ptr [eva] computing for function test_tab <- main. - Called from introduction_of_non_explicit_cast.c:71. + Called from introduction_of_non_explicit_cast.c:72. [eva] Recording results for test_tab [eva] Done for function test_tab [eva] computing for function init <- main. - Called from introduction_of_non_explicit_cast.c:73. + Called from introduction_of_non_explicit_cast.c:74. [eva] computing for function add3 <- init <- main. - Called from introduction_of_non_explicit_cast.c:57. + Called from introduction_of_non_explicit_cast.c:58. [eva] Recording results for add3 [eva] Done for function add3 [eva] Recording results for init [eva] Done for function init [eva] computing for function add3 <- main. - Called from introduction_of_non_explicit_cast.c:74. + Called from introduction_of_non_explicit_cast.c:75. [eva] Recording results for add3 [eva] Done for function add3 [eva] computing for function test_ptr <- main. - Called from introduction_of_non_explicit_cast.c:76. + Called from introduction_of_non_explicit_cast.c:77. [eva] Recording results for test_ptr [eva] Done for function test_ptr -[eva] introduction_of_non_explicit_cast.c:77: assertion got status valid. -[eva:alarm] introduction_of_non_explicit_cast.c:80: Warning: +[eva] introduction_of_non_explicit_cast.c:78: assertion got status valid. +[eva:alarm] introduction_of_non_explicit_cast.c:81: Warning: assertion got status unknown. -[eva] introduction_of_non_explicit_cast.c:81: assertion got status valid. +[eva] introduction_of_non_explicit_cast.c:82: assertion got status valid. [eva] Recording results for main [eva] done for function main [eva] ====== VALUES COMPUTED ====== diff --git a/tests/constant_propagation/struct_field.i b/tests/constant_propagation/struct_field.i index 97e18ced9849b044b3f42186a7082b89a9d1aacd..6f67d14b78e0493b5ae3e93f6a272df2d485785d 100644 --- a/tests/constant_propagation/struct_field.i +++ b/tests/constant_propagation/struct_field.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-eva" + STDOPT: #"-eva" */ struct st { diff --git a/tests/constant_propagation/test_config b/tests/constant_propagation/test_config index b3a8965ab1afefa926424d9f4730c5832a90b05a..a0809882b6a8268c6431a2d0f1c71fb4d00042c3 100644 --- a/tests/constant_propagation/test_config +++ b/tests/constant_propagation/test_config @@ -1,3 +1,3 @@ -MACRO: CONSTANT_PROPAGATION_PLUGINS constant_propagation eva,scope +MACRO: CONSTANT_PROPAGATION_PLUGINS constant_propagation @EVA_MAIN_PLUGINS@ from,inout PLUGIN: @CONSTANT_PROPAGATION_PLUGINS@ -OPT: -journal-disable -scf @EVA_OPTIONS@ -machdep x86_32 +OPT: @EVA_OPTIONS@ -machdep x86_32 -then -scf