Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CompareCIL.comparCilFiles: Handle multiple declarations of globals #941

Closed
wants to merge 1 commit into from
+12 −3
Closed

CompareCIL.comparCilFiles: Handle multiple declarations of globals #941

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 12 additions & 3 deletions src/incremental/compareCIL.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,14 +137,23 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
| GFun (f,_) -> f.svar.vname, {decls = None; def = Some (Fun f)}
| GVarDecl (v,_) -> v.vname, {decls = Some v; def = None}
| _ -> raise Not_found in
let merge_d def1 def2 = match def1, def2 with
let merge_decl decl1 decl2 = match decl1, decl2 with
| Some d, None -> Some d
| None, Some d -> Some d
| None, None -> None
| _ -> failwith "there can only be one definition and one declaration per global" in
| Some d, Some d' ->
if d != d' then
failwith "Multiple declaration of global where varinfos are not the same object.";
Some d' in
let merge_def def1 def2 = match def1, def2 with
| Some d, None -> Some d
| None, Some d -> Some d
| None, None -> None
| _ ->
failwith @@ "Only one definition per global expected, but there were multiple." in
let merge_global_col entry = match entry with
| None -> Some col
| Some col' -> Some {decls = merge_d col.decls col'.decls; def = merge_d col.def col'.def} in
| Some col' -> Some {decls = merge_decl col.decls col'.decls; def = merge_def col.def col'.def} in
GlobalMap.update name merge_global_col map;
with
Not_found -> map
Expand Down