2021-01-24 22:47 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002384Frama-CKernelpublic2018-11-30 10:07
Reporterevdenis 
Assigned Tovalentin.perrelle 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C 17-Chlorine 
Target VersionFixed in VersionFrama-C 18-Argon 
Summary0002384: user error: scalar value (of type int) initialized by compound initializer
DescriptionExample:
struct test {
   union {
      int a;
      long b;
   };
};

static struct test t = { { .a = 0 } };


Run:
$ gcc -c test.c
$ echo $?
0
$ frama-c test.c


Error Log:
[kernel] Parsing test.c (with preprocessing)
[kernel] test.c:1: Warning:
  unnamed fields are a C11 extension (use -c11 to avoid this warning)
[kernel] test.c:8: User Error:
  scalar value (of type int) initialized by compound initializer
  6     };
  7
  8     static struct test t = { { .a = 0 } };
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[kernel] User Error: stopping on file "test.c" that has errors. Add '-kernel-msg-key pp'
  for preprocessing command.
[kernel] Frama-C aborted: invalid user input.


Frama-C Version:
$ frama-c -version
Chlorine-20180501
TagsNo tags attached.
Attached Files
  • c file icon test.c (101 bytes) 2018-07-04 09:30 -
    struct test {
       union {
          int a;
          long b;
       };
    };
    
    static struct test t = { { .a = 0 } };
    
    c file icon test.c (101 bytes) 2018-07-04 09:30 +
  • patch file icon restore-initializers.patch (5,453 bytes) 2018-07-06 19:18 -
    ---
     src/kernel_internals/typing/cabs2cil.ml | 89 +++++++++++++--------------------
     1 file changed, 35 insertions(+), 54 deletions(-)
    
    diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
    index 29131725..b98eca07 100644
    --- a/src/kernel_internals/typing/cabs2cil.ml
    +++ b/src/kernel_internals/typing/cabs2cil.ml
    @@ -3335,7 +3335,7 @@ type stackElem =
                                                  * length, current index. If the
                                                  * array length is unspecified we
                                                  * use Int.max_int  *)
    -  | InComp  of offset * compinfo * offset list (* offset of parent,
    +  | InComp  of offset * compinfo * fieldinfo list (* offset of parent,
                                                          base comp, current fields *)
     
     
    @@ -3405,16 +3405,15 @@ and normalSubobj (so: subobj) : unit =
         end
     
       (* The fields are over *)
    -  | InComp (parOff, compinfo, nextflds) :: rest ->
    +  | InComp (parOff, _, nextflds) :: rest ->
         if nextflds == [] then begin (* No more fields here *)
           Kernel.debug ~dkey:Kernel.dkey_typing_init "Past the end of structure";
           so.stack <- rest;
           advanceSubobj so
         end else begin
    -      let fst = List.hd nextflds
    -      and baseTyp = TComp (compinfo,empty_size_cache (), []) in
    -      so.soTyp <- Cil.typeOffset baseTyp fst;
    -      so.soOff <- addOffset fst parOff
    +      let fst = List.hd nextflds in
    +      so.soTyp <- fst.ftype;
    +      so.soOff <- addOffset (Field(fst, NoOffset)) parOff
         end
     
     (* Advance to the next subobject. Always apply to a normalized object *)
    @@ -3433,64 +3432,43 @@ and advanceSubobj (so: subobj) : unit =
     
       (* The fields are over *)
       | InComp (parOff, comp, nextflds) :: rest ->
    -    let fi, flds' =
    -      match nextflds with
    -      | Field (fi,_) :: flds' -> fi, flds'
    -      | _ -> abort_context "advanceSubobj"
    -    in
         Kernel.debug ~dkey:Kernel.dkey_typing_init
    -      "Advancing past .%s" fi.fname;
    +      "Advancing past .%s" (List.hd nextflds).fname;
    +    let flds' =
    +      try List.tl nextflds
    +      with Failure _ -> abort_context "advanceSubobj"
    +    in
         so.stack <- InComp(parOff, comp, flds') :: rest;
         normalSubobj so
     
    -let anonCompFieldNameId = ref 0
    -let anonCompFieldName = "__anonCompField"
    +
     
     (* Find the fields to initialize in a composite. *)
     let fieldsToInit
         (comp: compinfo)
         (designator: string option)
    -  : offset list =
    -  (* Traversal of the comp fields (also goes through anonymous comp)
    -     the resulting fields are in reverse order *)
    -  let rec add_comp (offset : offset) (comp : compinfo) acc =
    -    let in_union = not comp.cstruct in
    -    add_fields offset in_union comp.cfields acc
    -  and add_fields (offset : offset) (in_union : bool) (l : fieldinfo list) acc =
    -    match l with
    -    | [] -> acc
    -    | f :: l ->
    -      let (found, _ as acc) = add_field offset f acc in
    -      if found && in_union
    -      then acc (* only consider one field in an union - stop if we found it *)
    -      else add_fields offset in_union l acc
    -  and add_field (offset : offset) (f : fieldinfo) (found, loff as acc) =
    -    (* update current offset *)
    -    let offset = Cil.addOffset (Field (f, NoOffset)) offset in
    -    (* if this field is an anonymous comp *)
    -    if prefix anonCompFieldName f.fname then
    -      match unrollType f.ftype with
    -      | TComp (comp, _, _) ->
    -        add_comp offset comp acc (* go deeper inside *)
    -      | _ ->
    -        abort_context "unnamed field type is not a struct/union"
    -    (* if this field is an anonymous field but not a comp *)
    -    else if f.fname = missingFieldName then
    -      acc (* Ignore anonymous non-comp fields *)
    -    (* if we have already found the designator, just append the current field *)
    -    else if found then
    -      found, offset :: loff
    -   (* we didn't find the designator yet, does this field match ? *)
    -    else match designator with
    -      | Some fn when f.fname = fn -> (true, [offset])
    -      | _ -> acc
    +  : fieldinfo list =
    +  (* Never look at anonymous fields *)
    +  let flds1 =
    +    List.filter (fun f -> f.fname <> missingFieldName) comp.cfields in
    +  let flds2 =
    +    match designator with
    +    | None -> flds1
    +    | Some fn ->
    +      let rec loop = function
    +        | [] ->
    +          Kernel.fatal ~current:true "Cannot find designated field %s" fn
    +        | (f :: _) as nextflds when f.fname = fn -> nextflds
    +        | _ :: rest -> loop rest
    +      in
    +      loop flds1
       in
    -  let found, r = add_comp NoOffset comp (designator = None, []) in
    -  begin if not found then
    -    let fn = Extlib.the designator in
    -    Kernel.fatal ~current:true "Cannot find designated field %s" fn;
    -  end;
    -  List.rev r
    +  (* If it is a union we only initialize one field *)
    +  match flds2 with
    +  | [] -> []
    +  | (f :: _) as toinit ->
    +    if comp.cstruct then toinit else [f]
    +
     
     let integerArrayLength (leno: exp option) : int =
       match leno with
    @@ -3502,6 +3480,9 @@ let integerArrayLength (leno: exp option) : int =
             "Initializing non-constant-length array with length=%a"
             Cil_printer.pp_exp len
     
    +let anonCompFieldNameId = ref 0
    +let anonCompFieldName = "__anonCompField"
    +
     let find_field_offset cond (fidlist: fieldinfo list) : offset =
       (* Depth first search for the field. This appears to be what GCC does.
        * MSVC checks that there are no ambiguous field names, so it does not
    -- 
    2.13.6
    
    
    patch file icon restore-initializers.patch (5,453 bytes) 2018-07-06 19:18 +

-Relationships
+Relationships

-Notes

~0006572

maroneze (administrator)

Thank you for the report. Indeed this is a regression w.r.t. Frama-C 16 and it must be fixed.

In the meanwhile, reverting to the previous Frama-C version might help. I'll upload a patch that should be applicable to Frama-C 17, in case it might be useful.

~0006573

maroneze (administrator)

The attached 'restore-initializers.patch' should hopefully allow parsing to behave as before, at least for this example. I didn't test it extensively though, so it's possible that it will not restore it in all cases.

~0006665

virgile (developer)

Fix will be available in the next release
+Notes

-Issue History
Date Modified Username Field Change
2018-07-04 09:30 evdenis New Issue
2018-07-04 09:30 evdenis File Added: test.c
2018-07-04 16:53 yakobowski Assigned To => maroneze
2018-07-04 16:53 yakobowski Status new => assigned
2018-07-06 19:17 maroneze Note Added: 0006572
2018-07-06 19:17 maroneze Status assigned => confirmed
2018-07-06 19:18 maroneze File Added: restore-initializers.patch
2018-07-06 19:21 maroneze Note Added: 0006573
2018-07-06 19:22 maroneze Product Version Frama-C GIT, precise the release id => Frama-C 17-Chlorine
2018-07-12 14:13 signoles Assigned To maroneze => virgile
2018-07-12 14:13 signoles Assigned To virgile => valentin.perrelle
2018-07-12 14:13 signoles Status confirmed => assigned
2018-10-18 10:33 virgile Note Added: 0006665
2018-10-18 10:33 virgile Status assigned => resolved
2018-10-18 10:33 virgile Fixed in Version => Frama-C 18-Argon
2018-10-18 10:33 virgile Resolution open => fixed
2018-11-30 10:07 signoles Status resolved => closed
+Issue History