Commit 4d7915e8 authored by Michele Alberti's avatar Michele Alberti
Browse files

Merge branch 'e-acsl-import/julien/archi/no_visitor' into 'master'

[e-acsl:archi] restore correct behavior of ghost parameters

See merge request frama-c/frama-c!2486
parents 24e83690 404c8c60
...@@ -568,6 +568,11 @@ let inject_in_fundec main fundec = ...@@ -568,6 +568,11 @@ let inject_in_fundec main fundec =
(* convert ghost variables *) (* convert ghost variables *)
vi.vghost <- false; vi.vghost <- false;
List.iter (fun vi -> vi.vghost <- false) fundec.slocals; List.iter (fun vi -> vi.vghost <- false) fundec.slocals;
let unghost_formal vi =
vi.vghost <- false ;
vi.vattr <- Cil.dropAttribute Cil.frama_c_ghost_formal vi.vattr
in
List.iter unghost_formal fundec.sformals;
(* update environments *) (* update environments *)
Builtins.update vi.vname vi; Builtins.update vi.vname vi;
(* track function addresses but the main function that is tracked internally (* track function addresses but the main function that is tracked internally
...@@ -575,9 +580,9 @@ let inject_in_fundec main fundec = ...@@ -575,9 +580,9 @@ let inject_in_fundec main fundec =
if not (Kernel_function.is_main kf) then Global_observer.add vi; if not (Kernel_function.is_main kf) then Global_observer.add vi;
(* exit point computations *) (* exit point computations *)
if Functions.instrument kf then Exit_points.generate fundec; if Functions.instrument kf then Exit_points.generate fundec;
(* recursive visit *)
Options.feedback ~dkey ~level:2 "entering in function %a." Options.feedback ~dkey ~level:2 "entering in function %a."
Kernel_function.pretty kf; Kernel_function.pretty kf;
(* recursive visit *)
let env = inject_in_block Env.empty kf fundec.sbody in let env = inject_in_block Env.empty kf fundec.sbody in
Exit_points.clear (); Exit_points.clear ();
add_generated_variables_in_function env fundec; add_generated_variables_in_function env fundec;
...@@ -592,6 +597,18 @@ let inject_in_fundec main fundec = ...@@ -592,6 +597,18 @@ let inject_in_fundec main fundec =
(* The whole AST *) (* The whole AST *)
(* ************************************************************************** *) (* ************************************************************************** *)
let unghost_vi vi =
(* do not convert extern ghost variables, because they can't be linked,
see bts #1392 *)
if vi.vstorage <> Extern then vi.vghost <- false;
match Cil.unrollType vi.vtype with
| TFun(res, Some l, va, attr) ->
(* unghostify function's parameters *)
let retype (n, t, a) = n, t, Cil.dropAttribute Cil.frama_c_ghost_formal a in
vi.vtype <- TFun(res, Some (List.map retype l), va, attr)
| _ ->
()
let inject_in_global (env, main) = function let inject_in_global (env, main) = function
(* library functions and built-ins *) (* library functions and built-ins *)
| GVarDecl(vi, _) | GVar(vi, _, _) | GVarDecl(vi, _) | GVar(vi, _, _)
...@@ -610,21 +627,19 @@ let inject_in_global (env, main) = function ...@@ -610,21 +627,19 @@ let inject_in_global (env, main) = function
(* variable declarations *) (* variable declarations *)
| GVarDecl(vi, _) | GFunDecl(_, vi, _) -> | GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
(* do not convert extern ghost variables, because they can't be linked, unghost_vi vi;
see bts #1392 *)
if vi.vstorage <> Extern then vi.vghost <- false;
Global_observer.add vi; Global_observer.add vi;
env, main env, main
(* variable definition *) (* variable definition *)
| GVar(vi, { init = None }, _) -> | GVar(vi, { init = None }, _) ->
Global_observer.add vi; Global_observer.add vi;
vi.vghost <- false; unghost_vi vi;
env, main env, main
| GVar(vi, { init = Some init }, _) -> | GVar(vi, { init = Some init }, _) ->
Global_observer.add vi; Global_observer.add vi;
vi.vghost <- false; unghost_vi vi;
let _init, env = inject_in_init env None vi NoOffset init in let _init, env = inject_in_init env None vi NoOffset init in
(* ignore the new initializer that handles literal strings since they are (* ignore the new initializer that handles literal strings since they are
not substituted in global initializers (see not substituted in global initializers (see
...@@ -632,7 +647,8 @@ let inject_in_global (env, main) = function ...@@ -632,7 +647,8 @@ let inject_in_global (env, main) = function
env, main env, main
(* function definition *) (* function definition *)
| GFun(fundec, _) -> | GFun({ svar = vi } as fundec, _) ->
unghost_vi vi;
inject_in_fundec main fundec inject_in_fundec main fundec
(* other globals: nothing to do *) (* other globals: nothing to do *)
......
/* Generated by Frama-C */ /* Generated by Frama-C */
#include "stdio.h" #include "stdio.h"
#include "stdlib.h" #include "stdlib.h"
void function(int a, int b) /*@ ghost (int c, int d) */ void function(int a, int b, int c, int d)
{ {
return; return;
} }
...@@ -14,7 +14,7 @@ int main(void) ...@@ -14,7 +14,7 @@ int main(void)
int x = 1; int x = 1;
int y = 2; int y = 2;
int z = 3; int z = 3;
function(w,x) /*@ ghost (y,z) */; function(w,x,y,z);
__retres = 0; __retres = 0;
return __retres; return __retres;
} }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment