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

[Eva] In Ivette, fixes the value of function parameters in the Inspector panel.

Function parameters were wrongly evaluated in the initial state of the
analysis instead of the initial state of the given function.
parent 760f907c
No related branches found
No related tags found
No related merge requests found
...@@ -189,22 +189,30 @@ let term_lval_to_lval tlval = ...@@ -189,22 +189,30 @@ let term_lval_to_lval tlval =
let print_value fmt loc = let print_value fmt loc =
let is_scalar = Cil.isScalarType in let is_scalar = Cil.isScalarType in
let kinstr, eval = let kf, kinstr, eval =
match loc with match loc with
| Printer_tag.PLval (_kf, ki, lval) when is_scalar (Cil.typeOfLval lval) -> | Printer_tag.PLval (kf, ki, lval) when is_scalar (Cil.typeOfLval lval) ->
ki, Results.eval_lval lval kf, ki, Results.eval_lval lval
| Printer_tag.PExp (_kf, ki, expr) when is_scalar (Cil.typeOf expr) -> | Printer_tag.PExp (kf, ki, expr) when is_scalar (Cil.typeOf expr) ->
ki, Results.eval_exp expr kf, ki, Results.eval_exp expr
| PVDecl (_kf, ki, vi) when is_scalar vi.vtype -> | PVDecl (kf, ki, vi) when is_scalar vi.vtype ->
ki, Results.eval_var vi kf, ki, Results.eval_var vi
| PTermLval (_kf, ki, _ip, tlval) -> | PTermLval (kf, ki, _ip, tlval) ->
let lval = term_lval_to_lval tlval in let lval = term_lval_to_lval tlval in
ki, Results.eval_lval lval if is_scalar (Cil.typeOfLval lval)
then kf, ki, Results.eval_lval lval
else raise Not_found
| _ -> raise Not_found | _ -> raise Not_found
in in
let pretty = Cvalue.V_Or_Uninitialized.pretty in let pretty = Cvalue.V_Or_Uninitialized.pretty in
let eval_cvalue at = Results.(eval at |> as_cvalue_or_uninitialized) in let eval_cvalue at = Results.(eval at |> as_cvalue_or_uninitialized) in
let before = eval_cvalue (Results.before_kinstr kinstr) in let request =
match kf, kinstr with
| _, Kstmt stmt -> Results.before stmt
| Some kf, Kglobal -> Results.at_start_of kf
| None, Kglobal -> Results.at_start
in
let before = eval_cvalue request in
match kinstr with match kinstr with
| Kglobal -> pretty fmt before | Kglobal -> pretty fmt before
| Kstmt stmt -> | Kstmt stmt ->
......
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