diff --git a/src/plugins/value_types/widen_type.ml b/src/plugins/value_types/widen_type.ml index d49b1a0fc6dc433bcc1b2dc1ee3f2144379ff755..92f57f012f4572c7efb29e6096013f40b7afcfe5 100644 --- a/src/plugins/value_types/widen_type.ml +++ b/src/plugins/value_types/widen_type.ml @@ -227,7 +227,8 @@ let hints_from_keys stmt h = float_hints_for_base b) let var_hints stmt prio_bases = - { empty with priority_bases = Stmt.Map.singleton stmt prio_bases } + let bases = Base.Set.filter (fun b -> not (Base.is_function b)) prio_bases in + { empty with priority_bases = Stmt.Map.singleton stmt bases } let num_hints stmto baseo hints = match stmto, baseo with diff --git a/tests/value/oracle/widen_non_constant.res.oracle b/tests/value/oracle/widen_non_constant.res.oracle index 6d5b5622a50133d23f68a4dd49a64e297d862e3c..2e157ad4b543e584a8fa0896bcc5f163df6296bb 100644 --- a/tests/value/oracle/widen_non_constant.res.oracle +++ b/tests/value/oracle/widen_non_constant.res.oracle @@ -10,7 +10,7 @@ t[0..19] ∈ {0} u[0..39] ∈ {0} [eva] computing for function main1 <- main. - Called from tests/value/widen_non_constant.i:84. + Called from tests/value/widen_non_constant.i:97. [eva] tests/value/widen_non_constant.i:11: Frama_C_show_each_out: {0} [eva] tests/value/widen_non_constant.i:13: Frama_C_show_each_in: {0}, {1} [eva] tests/value/widen_non_constant.i:12: starting to merge loop iterations @@ -29,7 +29,7 @@ [eva] Recording results for main1 [eva] Done for function main1 [eva] computing for function main2 <- main. - Called from tests/value/widen_non_constant.i:85. + Called from tests/value/widen_non_constant.i:98. [eva] tests/value/widen_non_constant.i:27: Frama_C_show_each_out: {0} [eva] tests/value/widen_non_constant.i:29: Frama_C_show_each_in: {0}, {1} [eva] tests/value/widen_non_constant.i:28: starting to merge loop iterations @@ -48,7 +48,7 @@ [eva] Recording results for main2 [eva] Done for function main2 [eva] computing for function main3 <- main. - Called from tests/value/widen_non_constant.i:86. + Called from tests/value/widen_non_constant.i:99. [eva] tests/value/widen_non_constant.i:46: Frama_C_show_each_out: {0} [eva] tests/value/widen_non_constant.i:48: Frama_C_show_each_in: {0}, {1} [eva] tests/value/widen_non_constant.i:47: starting to merge loop iterations @@ -67,7 +67,7 @@ [eva] Recording results for main3 [eva] Done for function main3 [eva] computing for function main4 <- main. - Called from tests/value/widen_non_constant.i:87. + Called from tests/value/widen_non_constant.i:100. [eva] tests/value/widen_non_constant.i:63: starting to merge loop iterations [eva] tests/value/widen_non_constant.i:69: starting to merge loop iterations [eva] tests/value/widen_non_constant.i:72: Frama_C_show_each: {43} @@ -76,6 +76,11 @@ Frama_C_show_each: {35; 36; 37; 38; 39; 40; 41; 42} [eva] Recording results for main4 [eva] Done for function main4 +[eva] computing for function main5 <- main. + Called from tests/value/widen_non_constant.i:101. +[eva] tests/value/widen_non_constant.i:90: starting to merge loop iterations +[eva] Recording results for main5 +[eva] Done for function main5 [eva] Recording results for main [eva] done for function main [eva] ====== VALUES COMPUTED ====== @@ -97,6 +102,9 @@ j ∈ {35; 36; 37; 38; 39; 40; 41; 42} maxi ∈ {19} maxj ∈ {35} +[eva:final-states] Values at end of function main5: + i ∈ {32} + ptr ∈ {{ (void *)&sub }} [eva:final-states] Values at end of function main: t[0] ∈ {-1} [1..19] ∈ [0..18] @@ -109,6 +117,8 @@ [from] Done for function main3 [from] Computing for function main4 [from] Done for function main4 +[from] Computing for function main5 +[from] Done for function main5 [from] Computing for function main [from] Done for function main [from] ====== DEPENDENCIES COMPUTED ====== @@ -123,6 +133,8 @@ t[0] FROM \nothing [1..19] FROM \nothing (and SELF) u[0..39] FROM \nothing (and SELF) +[from] Function main5: + NO EFFECTS [from] Function main: t[0] FROM \nothing [1..19] FROM \nothing (and SELF) @@ -144,6 +156,10 @@ t[0..19]; u[0..39]; i; j; maxi; maxj [inout] Inputs for function main4: \nothing +[inout] Out (internal) for function main5: + i; ptr +[inout] Inputs for function main5: + \nothing [inout] Out (internal) for function main: t[0..19]; u[0..39] [inout] Inputs for function main: diff --git a/tests/value/widen_non_constant.i b/tests/value/widen_non_constant.i index 4a297fc1a4fd930d8334c66bc53bfee250ecb027..00ec24ccbe489909ef00e449b579634065427d4a 100644 --- a/tests/value/widen_non_constant.i +++ b/tests/value/widen_non_constant.i @@ -80,9 +80,23 @@ void main4() { } +static double sub(double a, double b) {return a - b;} + +/* Test for a possible crash on function pointers. */ +void main5 (void) { + int i = 0; + void *ptr = sub; + /* Do not add [sub] to the bases to be widened. */ + while(i < 32 && ptr == sub) { + i++; + } +} + + void main() { main1(); main2(); main3(); main4(); + main5(); }