Skip to content

Commit f3a075d

Browse files
Merge pull request #56 from goblint/coreutils-no-error
Change some errors to warnings for coreutils
2 parents 64f3010 + 22a7d21 commit f3a075d

File tree

2 files changed

+6
-3
lines changed

2 files changed

+6
-3
lines changed

src/frontc/cabs2cil.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2870,10 +2870,10 @@ and doType (nameortype: attributeClass) (* This is AttrName if we are doing
28702870
(cabsTypeAddAttributes a1f tf), ap)
28712871
| _ ->
28722872
if a1f <> [] && not a1fadded then
2873-
E.s (error "Invalid position for (prefix) function type attributes:%a"
2873+
ignore (warn "Invalid position for (prefix) function type attributes:%a"
28742874
d_attrlist a1f);
28752875
if a2f <> [] then
2876-
E.s (error "Invalid position for (post) function type attributes:%a"
2876+
ignore (warn "Invalid position for (post) function type attributes:%a"
28772877
d_attrlist a2f);
28782878
restyp
28792879
in

src/frontc/cabshelper.ml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,10 @@ let joinLoc l1 l2 = match l1, l2 with
3131
{l1 with endLineno = l2.lineno; endByteno = l2.byteno; endColumnno = l2.columnno}
3232
| l1, l2 when l1.filename = l2.filename && l1.endByteno = l2.endByteno && l1.byteno = l2.byteno ->
3333
l1 (* alias fundefs *)
34-
| _, _ -> Errormsg.s (Errormsg.unimp "joinLoc %s %s" (string_of_loc l1) (string_of_loc l2))
34+
| _, _ ->
35+
(* some code generators leave start and end into different files: https://github.com/goblint/cil/issues/54 *)
36+
Errormsg.warn "joinLoc %s %s" (string_of_loc l1) (string_of_loc l2);
37+
l1 (* no way to give an actual range *)
3538

3639
(* clexer puts comments here *)
3740
let commentsGA = GrowArray.make 100 (GrowArray.Elem(cabslu,"",false))

0 commit comments

Comments
 (0)