Skip to content
Snippets Groups Projects
Commit da9f64cd authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[kernel] fix frama-c visitor

parent bf61a240
No related branches found
No related tags found
No related merge requests found
...@@ -631,8 +631,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c ...@@ -631,8 +631,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
method! vglob g = method! vglob g =
let fundec, has_kf = match g with let fundec, has_kf = match g with
| GFunDecl(_,v,_) -> | GFunDecl(_,v,_) ->
let ov = Visitor_behavior.Get_orig.varinfo self#behavior v in let kf = try Globals.Functions.get v with Not_found ->
let kf = try Globals.Functions.get ov with Not_found ->
Kernel.fatal "No kernel function for %s(%d)" v.vname v.vid Kernel.fatal "No kernel function for %s(%d)" v.vname v.vid
in in
(* Just make a copy of current kernel function in case it is needed *) (* Just make a copy of current kernel function in case it is needed *)
...@@ -642,7 +641,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c ...@@ -642,7 +641,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
self#set_current_kf kf; self#set_current_kf kf;
None, true None, true
| GFun(f,_) -> | GFun(f,_) ->
let v = Visitor_behavior.Get_orig.varinfo self#behavior f.svar in let v = f.svar in
let kf = let kf =
try Globals.Functions.get v try Globals.Functions.get v
with Not_found -> with Not_found ->
......
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