diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml index e0e40434a36cdf33479f24bebc5c0b75d4f2f0c5..52c110ee0e55659eee21fb931dcca15defccbd22 100644 --- a/src/kernel_services/ast_queries/ast_info.ml +++ b/src/kernel_services/ast_queries/ast_info.ml @@ -39,7 +39,7 @@ let rec possible_value_of_integral_const = function | _ -> None and possible_value_of_integral_expr e = - match e.enode with + match (Cil.constFold true e).enode with | Const c -> possible_value_of_integral_const c | _ -> None diff --git a/tests/misc/local_array_non_literal_size.i b/tests/misc/local_array_non_literal_size.i new file mode 100644 index 0000000000000000000000000000000000000000..cc8c1cf75ba71b423dc3d295f3e938e9c2f3c58d --- /dev/null +++ b/tests/misc/local_array_non_literal_size.i @@ -0,0 +1,25 @@ +/* run.config + PLUGIN: eva,inout + OPT: -eva -machdep gcc_x86_64 +*/ + +void one_dim() { + int empty_array[3%1] = { }; + int normal_array[3+1] = { 0, 1, 2, 3 }; +} + +void two_dim_literal() { + int empty_array[1][0] = { }; + int normal_array[1][4] = { 0, 1, 2, 3 }; +} + +void two_dim_non_literal () { + int empty_array[1][3%1] = { }; + int normal_array[1][3+1] = { 0, 1, 2, 3 }; +} + +int main() { + one_dim(); + two_dim_literal(); + two_dim_non_literal(); +} diff --git a/tests/misc/oracle/local_array_non_literal_size.err.oracle b/tests/misc/oracle/local_array_non_literal_size.err.oracle new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/tests/misc/oracle/local_array_non_literal_size.res.oracle b/tests/misc/oracle/local_array_non_literal_size.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391