diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 00315ab1904b8f67d1cc066f48233f9f5bc195d6..cccda3a9169be72d7c7d2202aec9827b2b477ada 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -3297,12 +3297,17 @@ let rec collectInitializer (if len_used then newtype else thistype), reads - | TComp (comp, _, _), CompoundPre (pMaxIdx, pArray) when comp.cstruct -> + | TComp (comp, _, _) as t, + CompoundPre (pMaxIdx, pArray) when comp.cstruct -> Kernel.debug ~dkey "Initialization of an object of type %a with at least %d components" Cil_printer.pp_typ thistype !pMaxIdx; let rec collect (idx: int) reads = function [] -> [], reads + | [ _ ] when Cil.has_flexible_array_member t && idx > !pMaxIdx -> + (* Do not add an empty initializer to the FAM, making an ill-formed + AST. An explicit initialization is allowed in gcc-mode. *) + [], reads | f :: restf -> if f.fname = missingFieldName then collect (idx + 1) reads restf diff --git a/tests/misc/fam_with_init.i b/tests/misc/fam_with_init.i new file mode 100644 index 0000000000000000000000000000000000000000..d7e8c5463b4468718e08c0388284d369ee08f7d5 --- /dev/null +++ b/tests/misc/fam_with_init.i @@ -0,0 +1,13 @@ +/* run.config +STDOPT: +"-print" +*/ + +struct s { + int a; + char data[]; // FAM +}; + +int main() { + struct s s1 = {0}; + return s1.a; +} diff --git a/tests/misc/oracle/fam_with_init.res.oracle b/tests/misc/oracle/fam_with_init.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..6672d06da2e8d37ac925ffaac63821a5d1b1af3e --- /dev/null +++ b/tests/misc/oracle/fam_with_init.res.oracle @@ -0,0 +1,37 @@ +[kernel] Parsing tests/misc/fam_with_init.i (no preprocessing) +[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] Recording results for main +[eva] done for function main +[eva] ====== VALUES COMPUTED ====== +[eva:final-states] Values at end of function main: + s1 ∈ {0} + __retres ∈ {0} +[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 main: + \result FROM \nothing +[from] ====== END OF DEPENDENCIES ====== +[inout] Out (internal) for function main: + s1; __retres +[inout] Inputs for function main: + \nothing +/* Generated by Frama-C */ +struct s { + int a ; + char data[] ; +}; +int main(void) +{ + int __retres; + struct s s1 = {.a = 0}; + __retres = s1.a; + return __retres; +} + +