Skip to content
Snippets Groups Projects
Commit f1a60164 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Hypotheses: fixes assigned via pointer

parent 656e89b2
No related branches found
No related tags found
No related merge requests found
...@@ -89,12 +89,17 @@ let set x p w = ...@@ -89,12 +89,17 @@ let set x p w =
let assigned t w = let assigned t w =
let rec assigned_via_pointer t = let rec assigned_via_pointer t =
match t.term_node with match t.term_node with
| TLval (TMem _, _) -> true | TLval (TMem _, _) ->
| Tif (_, t, _) | Tat (t, _) true
| TCastE (_, t) | TLogic_coerce (_, t) | TCastE (_, t) | TLogic_coerce (_, t)
| Tunion (t :: _) | Tinter (t :: _) | Tcomprehension(t, _, _) | Tat (t, _) ->
| Tcomprehension(t, _, _) -> assigned_via_pointer t assigned_via_pointer t
| _ -> false | Tunion l | Tinter l ->
List.exists assigned_via_pointer l
| Tif (_, t1, t2) ->
assigned_via_pointer t1 || assigned_via_pointer t2
| _ ->
false
in in
let assigned = let assigned =
if assigned_via_pointer t.it_content then t :: w.assigned if assigned_via_pointer t.it_content then t :: w.assigned
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment