Skip to content
Snippets Groups Projects
Commit 8269bc74 authored by David Bühler's avatar David Bühler
Browse files

[Wp] Fixes a crash in the GUI.

parent 5e6d288d
No related branches found
No related tags found
No related merge requests found
...@@ -407,19 +407,23 @@ let model_varinfo : ...@@ -407,19 +407,23 @@ let model_varinfo :
| PLval(Some kf, _ , (Var x,NoOffset)) | PLval(Some kf, _ , (Var x,NoOffset))
| PTermLval(Some kf, _, _, (TVar {lv_origin=Some x},TNoOffset)) | PTermLval(Some kf, _, _, (TVar {lv_origin=Some x},TNoOffset))
when button=1 -> when button=1 ->
let init = WpStrategy.is_main_init kf in begin
let acc = RefUsage.get ~kf ~init x in try
let model = match acc with let init = WpStrategy.is_main_init kf in
| RefUsage.NoAccess -> "any" let acc = RefUsage.get ~kf ~init x in
| RefUsage.ByValue -> "'var'" let model = match acc with
| RefUsage.ByRef -> "'ref'" | RefUsage.NoAccess -> "any"
| RefUsage.ByArray when x.vformal && Cil.isPointerType x.vtype | RefUsage.ByValue -> "'var'"
-> "'caveat'" | RefUsage.ByRef -> "'ref'"
| _ -> "'typed'" | RefUsage.ByArray when x.vformal && Cil.isPointerType x.vtype
in -> "'caveat'"
main#pretty_information | _ -> "'typed'"
"Is is accessed as %t and fits in %s wp-model@." in
(RefUsage.print x acc) model ; main#pretty_information
"Is is accessed as %t and fits in %s wp-model@."
(RefUsage.print x acc) model ;
with _ -> ()
end
| _ -> () | _ -> ()
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
......
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