From 5032018f9dcd941724c0325cecd2a7a764a67b2f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 31 May 2024 11:53:03 +0200
Subject: [PATCH] [Eva] Renames Evast into Eva_ast in all modules related to
the new Eva AST.
---
.../aorai/aorai_eva_analysis.enabled.ml | 2 +-
src/plugins/eva/Eva.mli | 6 +-
src/plugins/eva/api/values_request.ml | 10 +--
src/plugins/eva/ast/{evast.ml => eva_ast.ml} | 14 ++--
.../eva/ast/{evast.mli => eva_ast.mli} | 0
.../{evast_builder.ml => eva_ast_builder.ml} | 6 +-
...{evast_datatype.ml => eva_ast_datatype.ml} | 26 ++++----
.../{evast_printer.ml => eva_ast_printer.ml} | 2 +-
.../ast/{evast_types.ml => eva_ast_types.ml} | 0
.../{evast_typing.ml => eva_ast_typing.ml} | 2 +-
.../ast/{evast_utils.ml => eva_ast_utils.ml} | 16 ++---
.../{evast_visitor.ml => eva_ast_visitor.ml} | 6 +-
src/plugins/eva/ast/eva_automata.ml | 8 +--
src/plugins/eva/ast/eva_automata.mli | 2 +-
src/plugins/eva/domains/abstract_domain.ml | 4 +-
src/plugins/eva/domains/apron/apron_domain.ml | 6 +-
src/plugins/eva/domains/cvalue/builtins.ml | 4 +-
src/plugins/eva/domains/cvalue/builtins.mli | 2 +-
.../eva/domains/cvalue/builtins_memory.ml | 4 +-
.../eva/domains/cvalue/builtins_split.ml | 10 +--
.../eva/domains/cvalue/builtins_watchpoint.ml | 4 +-
.../eva/domains/cvalue/cvalue_offsetmap.ml | 2 +-
.../eva/domains/cvalue/cvalue_offsetmap.mli | 2 +-
.../eva/domains/cvalue/cvalue_queries.ml | 6 +-
.../eva/domains/cvalue/cvalue_queries.mli | 2 +-
.../eva/domains/cvalue/cvalue_transfer.ml | 2 +-
.../eva/domains/cvalue/cvalue_transfer.mli | 4 +-
src/plugins/eva/domains/domain_builder.ml | 4 +-
src/plugins/eva/domains/equality/equality.ml | 4 +-
src/plugins/eva/domains/equality/equality.mli | 2 +-
.../eva/domains/equality/equality_domain.ml | 32 ++++-----
.../eva/domains/gauges/gauges_domain.ml | 2 +-
src/plugins/eva/domains/hcexprs.ml | 18 ++---
src/plugins/eva/domains/hcexprs.mli | 14 ++--
src/plugins/eva/domains/inout_domain.ml | 6 +-
.../eva/domains/multidim/abstract_memory.ml | 4 +-
.../eva/domains/multidim/abstract_memory.mli | 4 +-
.../eva/domains/multidim/abstract_offset.ml | 16 ++---
.../eva/domains/multidim/abstract_offset.mli | 8 +--
.../eva/domains/multidim/multidim_domain.ml | 46 ++++++-------
.../eva/domains/multidim/segmentation.ml | 16 ++---
.../eva/domains/multidim/segmentation.mli | 2 +-
.../eva/domains/multidim/typed_memory.mli | 2 +-
.../eva/domains/numerors/numerors_value.ml | 2 +-
src/plugins/eva/domains/octagons.ml | 28 ++++----
src/plugins/eva/domains/offsm_domain.ml | 4 +-
src/plugins/eva/domains/printer_domain.ml | 10 +--
src/plugins/eva/domains/simple_memory.ml | 8 +--
src/plugins/eva/domains/symbolic_locs.ml | 16 ++---
src/plugins/eva/domains/taint_domain.ml | 12 ++--
src/plugins/eva/domains/traces_domain.ml | 12 ++--
src/plugins/eva/dune | 2 +-
src/plugins/eva/engine/evaluation.ml | 66 +++++++++----------
src/plugins/eva/engine/initialization.ml | 24 +++----
src/plugins/eva/engine/initialization.mli | 2 +-
src/plugins/eva/engine/iterator.ml | 10 +--
.../eva/engine/subdivided_evaluation.ml | 34 +++++-----
src/plugins/eva/engine/transfer_stmt.ml | 38 +++++------
src/plugins/eva/eval.ml | 10 +--
src/plugins/eva/eval.mli | 4 +-
src/plugins/eva/gui/gui_eval.ml | 8 +--
src/plugins/eva/gui/register_gui.ml | 2 +-
src/plugins/eva/legacy/eval_terms.ml | 8 +--
.../eva/partitioning/auto_loop_unroll.ml | 38 +++++------
src/plugins/eva/partitioning/partition.ml | 18 ++---
src/plugins/eva/partitioning/partition.mli | 2 +-
.../eva/partitioning/trace_partitioning.ml | 2 +-
.../eva/partitioning/trace_partitioning.mli | 2 +-
src/plugins/eva/utils/backward_formals.ml | 4 +-
src/plugins/eva/utils/backward_formals.mli | 2 +-
src/plugins/eva/utils/eva_utils.ml | 2 +-
src/plugins/eva/utils/eva_utils.mli | 2 +-
src/plugins/eva/utils/private.ml | 2 +-
src/plugins/eva/utils/private.mli | 2 +-
src/plugins/eva/utils/results.ml | 16 ++---
src/plugins/eva/utils/results.mli | 2 +-
src/plugins/eva/utils/unit_tests.ml | 8 +--
src/plugins/eva/utils/widen.ml | 6 +-
src/plugins/eva/values/abstract_value.ml | 10 +--
src/plugins/eva/values/cvalue_backward.ml | 6 +-
src/plugins/eva/values/cvalue_backward.mli | 4 +-
src/plugins/eva/values/cvalue_forward.ml | 10 +--
src/plugins/eva/values/cvalue_forward.mli | 6 +-
src/plugins/eva/values/main_values.ml | 2 +-
src/plugins/eva/values/offsm_value.ml | 10 +--
src/plugins/eva/values/sign_value.ml | 10 +--
86 files changed, 399 insertions(+), 399 deletions(-)
rename src/plugins/eva/ast/{evast.ml => eva_ast.ml} (90%)
rename src/plugins/eva/ast/{evast.mli => eva_ast.mli} (100%)
rename src/plugins/eva/ast/{evast_builder.ml => eva_ast_builder.ml} (98%)
rename src/plugins/eva/ast/{evast_datatype.ml => eva_ast_datatype.ml} (88%)
rename src/plugins/eva/ast/{evast_printer.ml => eva_ast_printer.ml} (99%)
rename src/plugins/eva/ast/{evast_types.ml => eva_ast_types.ml} (100%)
rename src/plugins/eva/ast/{evast_typing.ml => eva_ast_typing.ml} (99%)
rename src/plugins/eva/ast/{evast_utils.ml => eva_ast_utils.ml} (98%)
rename src/plugins/eva/ast/{evast_visitor.ml => eva_ast_visitor.ml} (97%)
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index 7cfcc78b6f7..9a9df3c2ca5 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -36,7 +36,7 @@ let show_aorai_variable state fmt var_name =
let show_val fmt (expr, v) =
Format.fprintf fmt "%a in %a"
- Eva.Evast.pp_exp expr
+ Eva.Eva_ast.pp_exp expr
(Cvalue.V.pretty_typ (Some expr.typ)) v
let show_non_det_state fmt state =
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index c2da63fdb26..36074201304 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -217,7 +217,7 @@ module Deps: sig
val narrow : t -> t -> t
end
-module Evast: sig
+module Eva_ast: sig
(** Eva Syntax Tree. *)
type origin =
@@ -658,7 +658,7 @@ module Results: sig
(** Returns the list of expressions which have been inferred to be equal to
the given expression by the Equality domain. *)
- val equality_class : Evast.exp -> request -> Evast.exp list result
+ val equality_class : Eva_ast.exp -> request -> Eva_ast.exp list result
(** Returns the Cvalue state. Error cases are converted into the bottom or top
cvalue state accordingly. *)
@@ -1000,7 +1000,7 @@ module Builtins: sig
(** Eva analysis builtins for the cvalue domain, more efficient than their
equivalent in C. *)
- open Evast
+ open Eva_ast
exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index ac42855caf9..eca8979c168 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -450,7 +450,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
(* --- Evaluates an expression or lvalue into an evaluation [result]. ----- *)
- let lval_to_offsetmap (lval : Evast.lval) state =
+ let lval_to_offsetmap (lval : Eva_ast.lval) state =
let cvalue_state = get_cvalue_or_top state in
match lval.node with
| Var vi, NoOffset ->
@@ -461,7 +461,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let precise_loc = get_precise_loc loc in
find_offsetmap cvalue_state precise_loc
- let eval_lval (lval : Evast.lval) state =
+ let eval_lval (lval : Eva_ast.lval) state =
match Cil.(unrollType lval.typ) with
| TInt _ | TEnum _ | TPtr _ | TFloat _ ->
A.copy_lvalue state lval >>=: fun value -> Value value
@@ -489,7 +489,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let do_next eval state eval_point callstack =
match next_steps eval_point with
| `Condition (stmt, cond) ->
- let cond' = Evast.translate_exp cond in
+ let cond' = Eva_ast.translate_exp cond in
let then_state = (A.assume_cond stmt state cond' true :> dstate) in
let else_state = (A.assume_cond stmt state cond' false :> dstate) in
Cond (eval then_state, eval else_state)
@@ -517,10 +517,10 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let evaluate (term, eval_point) callstack =
match term with
| Plval lval ->
- let lval' = Evast.translate_lval lval in
+ let lval' = Eva_ast.translate_lval lval in
eval_steps lval'.typ (eval_lval lval') eval_point callstack
| Pexpr expr ->
- let expr' = Evast.translate_exp expr in
+ let expr' = Eva_ast.translate_exp expr in
eval_steps expr'.typ (eval_expr expr') eval_point callstack
| Ppred pred ->
eval_steps Cil.intType (eval_pred eval_point pred) eval_point callstack
diff --git a/src/plugins/eva/ast/evast.ml b/src/plugins/eva/ast/eva_ast.ml
similarity index 90%
rename from src/plugins/eva/ast/evast.ml
rename to src/plugins/eva/ast/eva_ast.ml
index 57c57be3481..a925e447f26 100644
--- a/src/plugins/eva/ast/evast.ml
+++ b/src/plugins/eva/ast/eva_ast.ml
@@ -20,10 +20,10 @@
(* *)
(**************************************************************************)
-include Evast_types
-include Evast_typing
-include Evast_printer
-include Evast_datatype
-include Evast_builder
-include Evast_utils
-include Evast_visitor
+include Eva_ast_types
+include Eva_ast_typing
+include Eva_ast_printer
+include Eva_ast_datatype
+include Eva_ast_builder
+include Eva_ast_utils
+include Eva_ast_visitor
diff --git a/src/plugins/eva/ast/evast.mli b/src/plugins/eva/ast/eva_ast.mli
similarity index 100%
rename from src/plugins/eva/ast/evast.mli
rename to src/plugins/eva/ast/eva_ast.mli
diff --git a/src/plugins/eva/ast/evast_builder.ml b/src/plugins/eva/ast/eva_ast_builder.ml
similarity index 98%
rename from src/plugins/eva/ast/evast_builder.ml
rename to src/plugins/eva/ast/eva_ast_builder.ml
index f10e076101c..b6dbd7f16d6 100644
--- a/src/plugins/eva/ast/evast_builder.ml
+++ b/src/plugins/eva/ast/eva_ast_builder.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast_types
+open Eva_ast_types
(* --- Constructors --- *)
@@ -29,11 +29,11 @@ let value_or f x = function
| None -> f x
let mk_exp ?(origin=Built) ?typ node =
- let typ = typ |> value_or Evast_typing.type_of_exp_node node in
+ let typ = typ |> value_or Eva_ast_typing.type_of_exp_node node in
{ node ; origin ; typ }
let mk_lval ?(origin=Built) ?typ node =
- let typ = typ |> value_or Evast_typing.type_of_lval_node node in
+ let typ = typ |> value_or Eva_ast_typing.type_of_lval_node node in
{ node ; origin ; typ }
diff --git a/src/plugins/eva/ast/evast_datatype.ml b/src/plugins/eva/ast/eva_ast_datatype.ml
similarity index 88%
rename from src/plugins/eva/ast/evast_datatype.ml
rename to src/plugins/eva/ast/eva_ast_datatype.ml
index d81b52dbb13..d6c7c4b1925 100644
--- a/src/plugins/eva/ast/evast_datatype.ml
+++ b/src/plugins/eva/ast/eva_ast_datatype.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast_types
+open Eva_ast_types
module Typ = Cil_datatype.Typ
module Varinfo = Cil_datatype.Varinfo
@@ -69,59 +69,59 @@ module Lval =
Datatype.Make_with_collections (struct
include Datatype.Serializable_undefined
type t = lval
- let name = "Evast_datatype.Lval"
+ let name = "Eva_ast_datatype.Lval"
let compare = compare_lval
let equal = equal_lval
let hash = hash_lval
let reprs =
reprs_tag (List.map (fun v -> Var v, NoOffset) Cil_datatype.Varinfo.reprs)
- let pretty = Evast_printer.pp_lval
+ let pretty = Eva_ast_printer.pp_lval
end)
module Lhost =
Datatype.Make_with_collections (struct
include Datatype.Serializable_undefined
type t = lhost
- let name = "Evast_datatype.Lhost"
+ let name = "Eva_ast_datatype.Lhost"
let compare = compare_lhost
let equal = equal_lhost
let hash = hash_lhost
let reprs = List.map (fun v -> Var v) Cil_datatype.Varinfo.reprs
let pretty fmt h =
- let lv = Evast_builder.mk_lval (h, NoOffset) in
- Evast_printer.pp_lval fmt lv
+ let lv = Eva_ast_builder.mk_lval (h, NoOffset) in
+ Eva_ast_printer.pp_lval fmt lv
end)
module Offset = Datatype.Make_with_collections (struct
include Datatype.Serializable_undefined
type t = offset
- let name = "Evast_datatype.Offset"
+ let name = "Eva_ast_datatype.Offset"
let compare = compare_offset
let equal = equal_offset
let hash = hash_offset
let reprs = [NoOffset]
- let pretty = Evast_printer.pp_offset
+ let pretty = Eva_ast_printer.pp_offset
end)
module Exp = Datatype.Make_with_collections (struct
include Datatype.Serializable_undefined
type t = exp
- let name = "Evast_datatype.Exp"
+ let name = "Eva_ast_datatype.Exp"
let compare = compare_exp
let equal = equal_exp
let hash = hash_exp
let reprs =
- List.map (fun e -> Evast_builder.translate_exp e) Cil_datatype.Exp.reprs
- let pretty = Evast_printer.pp_exp
+ List.map (fun e -> Eva_ast_builder.translate_exp e) Cil_datatype.Exp.reprs
+ let pretty = Eva_ast_printer.pp_exp
end)
module Constant = Datatype.Make_with_collections (struct
include Datatype.Serializable_undefined
type t = constant
- let name = "Evast_datatype.Constant"
+ let name = "Eva_ast_datatype.Constant"
let compare = compare_constant
let equal = equal_constant
let hash = hash_constant
let reprs = [ CInt64(Integer.zero, IInt, Some "0") ]
- let pretty = Evast_printer.pp_constant
+ let pretty = Eva_ast_printer.pp_constant
end)
diff --git a/src/plugins/eva/ast/evast_printer.ml b/src/plugins/eva/ast/eva_ast_printer.ml
similarity index 99%
rename from src/plugins/eva/ast/evast_printer.ml
rename to src/plugins/eva/ast/eva_ast_printer.ml
index 9da4343e166..a55a64d07fb 100644
--- a/src/plugins/eva/ast/evast_printer.ml
+++ b/src/plugins/eva/ast/eva_ast_printer.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast_types
+open Eva_ast_types
module Precedence =
struct
diff --git a/src/plugins/eva/ast/evast_types.ml b/src/plugins/eva/ast/eva_ast_types.ml
similarity index 100%
rename from src/plugins/eva/ast/evast_types.ml
rename to src/plugins/eva/ast/eva_ast_types.ml
diff --git a/src/plugins/eva/ast/evast_typing.ml b/src/plugins/eva/ast/eva_ast_typing.ml
similarity index 99%
rename from src/plugins/eva/ast/evast_typing.ml
rename to src/plugins/eva/ast/eva_ast_typing.ml
index e61bea32766..7791d14a4e1 100644
--- a/src/plugins/eva/ast/evast_typing.ml
+++ b/src/plugins/eva/ast/eva_ast_typing.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast_types
+open Eva_ast_types
let type_of node =
node.typ
diff --git a/src/plugins/eva/ast/evast_utils.ml b/src/plugins/eva/ast/eva_ast_utils.ml
similarity index 98%
rename from src/plugins/eva/ast/evast_utils.ml
rename to src/plugins/eva/ast/eva_ast_utils.ml
index a99df83a756..a6f978cb7dc 100644
--- a/src/plugins/eva/ast/evast_utils.ml
+++ b/src/plugins/eva/ast/eva_ast_utils.ml
@@ -20,18 +20,18 @@
(* *)
(**************************************************************************)
-open Evast_types
-open Evast_builder
+open Eva_ast_types
+open Eva_ast_builder
(* --- Conversion to Cil --- *)
module ConversionToCil =
State_builder.Hashtbl
- (Evast_datatype.Exp.Hashtbl)
+ (Eva_ast_datatype.Exp.Hashtbl)
(Cil_datatype.Exp)
(struct
- let name = "Value.Evast_utils.ConversionToCil"
+ let name = "Value.Eva_ast_utils.ConversionToCil"
let size = 16
let dependencies = [ Ast.self ]
end)
@@ -130,7 +130,7 @@ let is_mutable (lval : lval) : bool =
| _typ, Index _ ->
invalid_arg "Index on a non-array type"
in
- aux false (Evast_typing.type_of_lhost lhost) offset
+ aux false (Eva_ast_typing.type_of_lhost lhost) offset
let rec is_initialized_exp (on_same_obj : bool) (exp : exp) =
match exp.node with
@@ -177,7 +177,7 @@ and height_offset = function
(* --- Specialized visitors --- *)
let iter_lvals f =
- let open Evast_visitor.Fold in
+ let open Eva_ast_visitor.Fold in
let neutral = () and combine () () = () in
visit_exp ~neutral ~combine {
default with
@@ -185,7 +185,7 @@ let iter_lvals f =
}
let exp_contains_volatile, lval_contains_volatile =
- let open Evast_visitor.Fold in
+ let open Eva_ast_visitor.Fold in
let neutral = false and combine b1 b2 = b1 || b2 in
let fold_lval ~visitor lval =
Cil.isVolatileType (lval.typ) || default.fold_lval ~visitor lval
@@ -195,7 +195,7 @@ let exp_contains_volatile, lval_contains_volatile =
let vars_in_exp, vars_in_lval =
let module VarSet = Cil_datatype.Varinfo.Set in
- let open Evast_visitor.Fold in
+ let open Eva_ast_visitor.Fold in
let neutral = VarSet.empty and combine = VarSet.union in
let fold_lval ~visitor lval =
let set =
diff --git a/src/plugins/eva/ast/evast_visitor.ml b/src/plugins/eva/ast/eva_ast_visitor.ml
similarity index 97%
rename from src/plugins/eva/ast/evast_visitor.ml
rename to src/plugins/eva/ast/eva_ast_visitor.ml
index 74d08cb3b8b..b73b3eafedd 100644
--- a/src/plugins/eva/ast/evast_visitor.ml
+++ b/src/plugins/eva/ast/eva_ast_visitor.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast_types
+open Eva_ast_types
module Rewrite =
struct
@@ -50,7 +50,7 @@ struct
let rewrite_exp ~visitor exp =
let replace_if condition node =
- if condition then Evast_builder.mk_exp node else exp
+ if condition then Eva_ast_builder.mk_exp node else exp
in
match exp.node with
| Lval lv ->
@@ -87,7 +87,7 @@ struct
if e' != e then Mem e' else lhost
and offset' = visitor.offset offset in
if lhost' != lhost || offset' != offset
- then Evast_builder.mk_lval (lhost', offset')
+ then Eva_ast_builder.mk_lval (lhost', offset')
else lval
let rewrite_offset ~visitor offset =
diff --git a/src/plugins/eva/ast/eva_automata.ml b/src/plugins/eva/ast/eva_automata.ml
index b065380cf31..d19266c4706 100644
--- a/src/plugins/eva/ast/eva_automata.ml
+++ b/src/plugins/eva/ast/eva_automata.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
open Cil_types
-open Evast
+open Eva_ast
(* --- Vertices and Edges types --- *)
@@ -88,9 +88,9 @@ module Transition = Datatype.Make (struct
function
| Skip -> ()
| Return (None,_) -> fprintf fmt "return"
- | Return (Some exp,_) -> fprintf fmt "return %a" Evast.pp_exp exp
- | Guard (exp,Then,_) -> Evast.pp_exp fmt exp
- | Guard (exp,Else,_) -> fprintf fmt "!(%a)" Evast.pp_exp exp
+ | Return (Some exp,_) -> fprintf fmt "return %a" Eva_ast.pp_exp exp
+ | Guard (exp,Then,_) -> Eva_ast.pp_exp fmt exp
+ | Guard (exp,Else,_) -> fprintf fmt "!(%a)" Eva_ast.pp_exp exp
| Assign (_,_,stmt)
| Call (_,_,_,stmt)
| Init (_,_,stmt)
diff --git a/src/plugins/eva/ast/eva_automata.mli b/src/plugins/eva/ast/eva_automata.mli
index e4bde64e510..3a575edd130 100644
--- a/src/plugins/eva/ast/eva_automata.mli
+++ b/src/plugins/eva/ast/eva_automata.mli
@@ -26,7 +26,7 @@
vertex, edge and transitions types. *)
open Cil_types
-open Evast
+open Eva_ast
type vertex = private {
vertex_key : int;
diff --git a/src/plugins/eva/domains/abstract_domain.ml b/src/plugins/eva/domains/abstract_domain.ml
index 99782c18153..79e3f38dfd2 100644
--- a/src/plugins/eva/domains/abstract_domain.ml
+++ b/src/plugins/eva/domains/abstract_domain.ml
@@ -79,8 +79,8 @@
(* The types of the Cil AST. *)
open Cil_types
-type exp = Evast.exp
-type lval = Evast.lval
+type exp = Eva_ast.exp
+type lval = Eva_ast.lval
(* Definition of the types frequently used in Eva. *)
open Eval
diff --git a/src/plugins/eva/domains/apron/apron_domain.ml b/src/plugins/eva/domains/apron/apron_domain.ml
index eeed011cf15..a8628869f24 100644
--- a/src/plugins/eva/domains/apron/apron_domain.ml
+++ b/src/plugins/eva/domains/apron/apron_domain.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
open Eval
-open Evast
+open Eva_ast
open Apron
let dkey = Self.register_category "d-apron"
@@ -287,7 +287,7 @@ let rec constraint_expr eval oracle env expr positive =
let typ = translate_typ (Cil.unrollType typ) in
let e = Texpr1.Binop (Texpr1.Sub, e1'', e2'', typ, round) in
let expr = Texpr1.of_expr env e in
- let binop = Evast.conv_relation binop in
+ let binop = Eva_ast.conv_relation binop in
let binop = if positive then binop else Abstract_interp.Comp.inv binop in
translate_relation expr typ binop
| _ -> raise (Out_of_Scope "constraint_expr not handled")
@@ -495,7 +495,7 @@ module Make (Man : Input) = struct
compute state expr
let extract_lval ~oracle:_ _context state lval _loc =
- let expr = Evast.Build.lval lval in
+ let expr = Eva_ast.Build.lval lval in
compute state expr
let maybe_bottom state =
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index c74f0d491f4..088f1e19618 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast
+open Eva_ast
exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
@@ -254,7 +254,7 @@ let process_result call state call_result =
let b_ret = Base.of_varinfo vi_ret in
let offsm = Eval_op.offsetmap_of_v ~typ:vi_ret.vtype value in
let prefix = "Builtin " ^ Kernel_function.get_name call.kf in
- let lval_ret = Evast.Build.var vi_ret in
+ let lval_ret = Eva_ast.Build.var vi_ret in
Cvalue_transfer.warn_imprecise_offsm_write ~prefix lval_ret offsm;
Cvalue.Model.add_base b_ret offsm state, clob
| _, _ -> state, clob (* TODO: error? *)
diff --git a/src/plugins/eva/domains/cvalue/builtins.mli b/src/plugins/eva/domains/cvalue/builtins.mli
index 82813cdbe2a..830131d4b0e 100644
--- a/src/plugins/eva/domains/cvalue/builtins.mli
+++ b/src/plugins/eva/domains/cvalue/builtins.mli
@@ -25,7 +25,7 @@
(** Eva analysis builtins for the cvalue domain, more efficient than their
equivalent in C. *)
-open Evast
+open Eva_ast
exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index c0d912865c0..f49e1812f4d 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
open Cil_types
-open Evast
+open Eva_ast
open Cvalue
open Abstract_interp
open Locations
@@ -35,7 +35,7 @@ let rec lval_of_address exp =
match exp.node with
| AddrOf lval -> lval
| CastE (_typ, exp) -> lval_of_address exp
- | _ -> Evast.Build.mem exp
+ | _ -> Eva_ast.Build.mem exp
let plevel = Parameters.ArrayPrecisionLevel.get
diff --git a/src/plugins/eva/domains/cvalue/builtins_split.ml b/src/plugins/eva/domains/cvalue/builtins_split.ml
index f428b5d4bae..e688ca723c4 100644
--- a/src/plugins/eva/domains/cvalue/builtins_split.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_split.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast
+open Eva_ast
open Abstract_interp
open Cvalue
@@ -95,16 +95,16 @@ let split_v ~warn lv state max_card =
V.fold_enum aux_v v []
with Not_less_than ->
warning warn "Location %a points to too many values (%a). \
- Cannot split." Evast.pp_lval lv V.pretty v;
+ Cannot split." Eva_ast.pp_lval lv V.pretty v;
[state]
else begin
warning warn "Location %a is not a singleton (%a). Cannot split."
- Evast.pp_lval lv Locations.pretty loc;
+ Eva_ast.pp_lval lv Locations.pretty loc;
[state]
end
else begin
warning warn "Cannot split on lvalue %a of non-arithmetic type"
- Evast.pp_lval lv;
+ Eva_ast.pp_lval lv;
[state]
end
@@ -114,7 +114,7 @@ let split_pointer ~warn lv state max_card =
match lv.node with
| (Mem {node = Lval lv}, _) -> split_v ~warn lv state max_card
| _ ->
- warning warn "cannot split on non-pointer %a" Evast.pp_lval lv;
+ warning warn "cannot split on non-pointer %a" Eva_ast.pp_lval lv;
[state]
(** The three functions below gather all lvalues with integral type that appear
diff --git a/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml b/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml
index 0c0100ec719..681a6d020c1 100644
--- a/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_watchpoint.ml
@@ -32,7 +32,7 @@ let equal_watch w1 w2 =
| _ -> false
type watchpoint =
- { name_lv : Evast.exp;
+ { name_lv : Eva_ast.exp;
loc: Locations.location;
v: watch;
mutable remaining_count: Integer.t;
@@ -115,7 +115,7 @@ let watch_hook _callstack stmt states =
then begin
Self.warning ~wkey:Self.wkey_watchpoint ~once:true ~current:true
"%a %a%t"
- Evast.pp_exp name
+ Eva_ast.pp_exp name
V.pretty vs
Eva_utils.pp_callstack;
if Integer.is_zero current ||
diff --git a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml
index d24bfc1feef..3bb203a658e 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml
@@ -32,4 +32,4 @@ let offsetmap_of_assignment state expr = function
| Copy (lv, _value) ->
Bottom.non_bottom (Eval_op.offsetmap_of_loc lv.lloc state)
| Assign value ->
- offsetmap_of_v ~typ:expr.Evast.typ value
+ offsetmap_of_v ~typ:expr.Eva_ast.typ value
diff --git a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli
index 185292cb1fe..eb0d07611b1 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli
@@ -28,5 +28,5 @@ open Cvalue
- in case of a copy, extracts the offsetmap from the state;
- otherwise, translates the value assigned into an offsetmap. *)
val offsetmap_of_assignment:
- Model.t -> Evast.exp -> (Precise_locs.precise_location, V.t) Eval.assigned ->
+ Model.t -> Eva_ast.exp -> (Precise_locs.precise_location, V.t) Eval.assigned ->
V_Offsetmap.t
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
index 4d0c162429a..2ee6847b25d 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -45,7 +45,7 @@ module Queries = struct
let status =
if Cvalue.V.is_bottom (get_v v) then Alarmset.False else Alarmset.Unknown
in
- let lval = Evast.to_cil_lval lval in
+ let lval = Eva_ast.to_cil_lval lval in
match v with
| C_uninit_noesc _ -> Alarmset.singleton ~status (Alarms.Uninitialized lval)
| C_init_esc _ -> Alarmset.singleton ~status (Alarms.Dangling lval)
@@ -118,7 +118,7 @@ module Queries = struct
v, alarms
let extract_lval ~oracle:_ _context state lval loc =
- if Cil.isArithmeticOrPointerType lval.Evast.typ
+ if Cil.isArithmeticOrPointerType lval.Eva_ast.typ
then extract_scalar_lval state lval loc
else extract_aggregate_lval state lval loc
@@ -128,7 +128,7 @@ module Queries = struct
let loc = Precise_locs.imprecise_location precise_loc in
let eval_one_loc single_loc =
let v = Cvalue.Model.find state single_loc in
- let v = Cvalue_forward.make_volatile ~typ:lval.Evast.typ v in
+ let v = Cvalue_forward.make_volatile ~typ:lval.Eva_ast.typ v in
Cvalue_forward.reinterpret lval.typ v
in
let process_ival base ival (acc_loc, acc_val as acc) =
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.mli b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
index bb32e78e1c3..888d0325b39 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.mli
@@ -36,4 +36,4 @@ include Evaluation_sig.S with type state := state
and type origin := origin
(** Evaluates the location of a lvalue in a given cvalue state. *)
-val lval_to_loc: state -> Evast.lval -> Locations.location
+val lval_to_loc: state -> Eva_ast.lval -> Locations.location
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index 76d912877af..40e175ad0c6 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
open Eval
-open Evast
+open Eva_ast
type value = Main_values.CVal.t
type origin = value
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.mli b/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
index a04d9a98287..a4947d3c828 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
@@ -36,13 +36,13 @@ include Abstract_domain.Transfer
value [v] into location [loc] if one of them is overly imprecise. [lval] is
the assigned lvalue, and [prefix] is an optional prefix to the warning. *)
val warn_imprecise_write:
- ?prefix:string -> Evast.lval -> Locations.location -> Cvalue.V.t -> unit
+ ?prefix:string -> Eva_ast.lval -> Locations.location -> Cvalue.V.t -> unit
(** [warn_imprecise_offsm_write lval offsm] emits a warning about the assignment
of offsetmap [offsm] if it contains an overly imprecise value. [lval] is the
assigned lvalue, and [prefix] is an optional prefix to the warning. *)
val warn_imprecise_offsm_write:
- ?prefix:string -> Evast.lval -> Cvalue.V_Offsetmap.t -> unit
+ ?prefix:string -> Eva_ast.lval -> Cvalue.V_Offsetmap.t -> unit
(*
Local Variables:
diff --git a/src/plugins/eva/domains/domain_builder.ml b/src/plugins/eva/domains/domain_builder.ml
index 57ac9c2a525..eff6e6bf4f0 100644
--- a/src/plugins/eva/domains/domain_builder.ml
+++ b/src/plugins/eva/domains/domain_builder.ml
@@ -165,7 +165,7 @@ module Make_Minimal
Domain.initialize_variable lval ~initialized value state
let initialize_variable_using_type _kind varinfo state =
- let lval = Evast.Build.var varinfo in
+ let lval = Eva_ast.Build.var varinfo in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
let logic_assign _assigns _location _state = top
@@ -295,7 +295,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
Domain.initialize_variable lval ~initialized value state
let initialize_variable_using_type _kind varinfo state =
- let lval = Evast.Build.var varinfo in
+ let lval = Eva_ast.Build.var varinfo in
Domain.initialize_variable lval ~initialized:true Abstract_domain.Top state
let logic_assign _assigns _location _state = top
diff --git a/src/plugins/eva/domains/equality/equality.ml b/src/plugins/eva/domains/equality/equality.ml
index f84f9b54164..0683f1f9a5d 100644
--- a/src/plugins/eva/domains/equality/equality.ml
+++ b/src/plugins/eva/domains/equality/equality.ml
@@ -184,12 +184,12 @@ module Set = struct
let pick_representative set =
let choose elt (current, height) =
let elt = HCE.to_exp elt in
- let h = Evast.height_exp elt in
+ let h = Eva_ast.height_exp elt in
if h < height then (elt, h) else (current, height)
in
let head = HCESet.choose set in
let current = HCE.to_exp head in
- let height = Evast.height_exp current in
+ let height = Eva_ast.height_exp current in
fst (HCESet.fold choose (HCESet.remove head set) (current, height))
(* Binds the terms of the [equality] to [equality] in the [map].
diff --git a/src/plugins/eva/domains/equality/equality.mli b/src/plugins/eva/domains/equality/equality.mli
index c88dbbb1ff1..bff3cdb7e61 100644
--- a/src/plugins/eva/domains/equality/equality.mli
+++ b/src/plugins/eva/domains/equality/equality.mli
@@ -118,7 +118,7 @@ module Set : sig
(** [remove lval set] remove any expression [e] such that [lval] belongs to
[syntactic_lval e] from the set of equalities [set]. *)
- val remove : Hcexprs.kill_type -> Evast.lval -> t -> t
+ val remove : Hcexprs.kill_type -> Eva_ast.lval -> t -> t
(** [unite (a, a_set) (b, b_set) map] unites [a] and [b] in [map].
[a_set] must be equal to [syntactic_lval a],
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index 3030dff7750..adf3a682216 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -200,7 +200,7 @@ struct
Equality.Equality.fold
(fun atom acc ->
let e = HCE.to_exp atom in
- if Evast.Exp.equal e expr
+ if Eva_ast.Exp.equal e expr
then acc else (e, value) :: acc)
equality []
| None -> []
@@ -240,7 +240,7 @@ struct
| None -> `Value (Value.top, None), Alarmset.all
let extract_expr ~oracle _context (equalities, _, _) expr =
- let expr = Evast.const_fold expr in
+ let expr = Eva_ast.const_fold expr in
let atom_e = HCE.of_exp expr in
coop_eval oracle equalities atom_e
@@ -322,8 +322,8 @@ struct
match lv.node with
| Var vi, NoOffset -> Locations.zone_of_varinfo vi
| _ ->
- let expr = Evast.Build.lval lv in
- Evast.zone_of_exp (find_loc valuation) expr
+ let expr = Eva_ast.Build.lval lv in
+ Eva_ast.zone_of_exp (find_loc valuation) expr
in
Deps.add lval zone deps
@@ -345,7 +345,7 @@ struct
| `Top -> false (* should not happen *)
| `Value { value = { v } } -> is_singleton v
- let expr_is_cardinal_zero_or_one_loc valuation (e : Evast.exp) =
+ let expr_is_cardinal_zero_or_one_loc valuation (e : Eva_ast.exp) =
match e.node with
| Lval lv -> begin
let loc = valuation.Abstract_domain.find_loc lv in
@@ -379,8 +379,8 @@ struct
the reevaluation of [right_expr] would reduce it incorrectly, by
removing indeterminate flags without emitting alarms. *)
let assign_eq left_lval right_expr value valuation state =
- if Evast.lval_contains_volatile left_lval ||
- Evast.exp_contains_volatile right_expr ||
+ if Eva_ast.lval_contains_volatile left_lval ||
+ Eva_ast.exp_contains_volatile right_expr ||
not (Cil.isArithmeticOrPointerType left_lval.typ) ||
indeterminate_copy value
then state
@@ -401,12 +401,12 @@ struct
let left_loc = Precise_locs.imprecise_location left_value.lloc in
let direct_left_zone = Locations.(enumerate_valid_bits Write left_loc) in
let state = kill Hcexprs.Modified direct_left_zone state in
- let right_expr = Evast.const_fold right_expr in
+ let right_expr = Eva_ast.const_fold right_expr in
try
let indirect_left_zone =
- Evast.indirect_zone_of_lval (find_loc valuation) left_value.lval
+ Eva_ast.indirect_zone_of_lval (find_loc valuation) left_value.lval
and right_zone =
- Evast.zone_of_exp (find_loc valuation) right_expr
+ Eva_ast.zone_of_exp (find_loc valuation) right_expr
in
(* After an assignment lv = e, the equality [lv == eq] holds iff the value
of [e] and the location of [lv] are not modified by the assignment,
@@ -431,7 +431,7 @@ struct
state
else
try
- let left_value = Evast.Build.var arg.formal in
+ let left_value = Eva_ast.Build.var arg.formal in
assign_eq left_value arg.concrete arg.avalue valuation state
with Top_location -> state
in
@@ -446,17 +446,17 @@ struct
reasoning. This is the case for equalities between 0. and -0., and
between non-comparable pointers, so we need to skip such equalities. *)
let assume _stmt expr positive valuation (eqs, deps, modified_zone as state) =
- match positive, (expr : Evast.exp).node with
+ match positive, (expr : Eva_ast.exp).node with
| true, BinOp (Eq, e1, e2, _)
| false, BinOp (Ne, e1, e2, _) ->
begin
if not (is_safe_equality valuation e1 e2)
then `Value state
else
- let e1 = Evast.const_fold e1
- and e2 = Evast.const_fold e2 in
- if Evast.exp_contains_volatile e1
- || Evast.exp_contains_volatile e2
+ let e1 = Eva_ast.const_fold e1
+ and e2 = Eva_ast.const_fold e2 in
+ if Eva_ast.exp_contains_volatile e1
+ || Eva_ast.exp_contains_volatile e2
|| not (Cil.isArithmeticOrPointerType e1.typ)
|| (expr_is_cardinal_zero_or_one_loc valuation e1 &&
expr_cardinal_zero_or_one valuation e2)
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index 1c618b9551f..ea16b89bfc9 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Evast
+open Eva_ast
open Eval
type function_calls =
diff --git a/src/plugins/eva/domains/hcexprs.ml b/src/plugins/eva/domains/hcexprs.ml
index b7de1ba5084..b67b7b20813 100644
--- a/src/plugins/eva/domains/hcexprs.ml
+++ b/src/plugins/eva/domains/hcexprs.ml
@@ -20,8 +20,8 @@
(* *)
(**************************************************************************)
-module Exp = Evast.Exp
-module Lval = Evast.Lval
+module Exp = Eva_ast.Exp
+module Lval = Eva_ast.Lval
(* lvalues are never stored under a constructor [E]. *)
type unhashconsed_exprs = E of Exp.t | LV of Lval.t
@@ -70,8 +70,8 @@ module E = struct
end)
let replace kind ~late ~heir =
- let open Evast.Rewrite in
- let rewrite_exp ~visitor (exp : Evast.exp) =
+ let open Eva_ast.Rewrite in
+ let rewrite_exp ~visitor (exp : Eva_ast.exp) =
match exp.node with
| Lval lval ->
if Lval.equal lval late then heir else exp
@@ -82,7 +82,7 @@ module E = struct
| _ -> default.rewrite_exp ~visitor exp
in
let rewriter = { default with rewrite_exp } in
- Evast.Rewrite.visit_exp rewriter
+ Eva_ast.Rewrite.visit_exp rewriter
end
module HCE = struct
@@ -100,14 +100,14 @@ module HCE = struct
let of_lval lv = hashcons (LV lv)
- let of_exp (exp : Evast.exp) =
+ let of_exp (exp : Eva_ast.exp) =
match exp.node with
| Lval lv -> of_lval lv
| _ -> hashcons (E exp)
let to_exp h = match get h with
| E e -> e
- | LV lv -> Evast.Build.lval lv
+ | LV lv -> Eva_ast.Build.lval lv
let to_lval h = match get h with
| E _ -> None
@@ -124,7 +124,7 @@ module HCE = struct
let replace kind ~late ~heir h = match get h with
| E e ->
let e = E.replace kind ~late ~heir e in
- if Evast.height_exp e > height_limit
+ if Eva_ast.height_exp e > height_limit
then raise NonExchangeable
else of_exp e
| LV lval -> if Lval.equal lval late then of_exp heir else h
@@ -141,7 +141,7 @@ type lvalues = {
let empty_lvalues = { read = HCESet.empty; addr = HCESet.empty; }
let syntactic_lvalues expr =
- let rec gather (expr : Evast.exp) lvalues =
+ let rec gather (expr : Eva_ast.exp) lvalues =
match expr.node with
| Lval lv ->
{ lvalues with read = HCESet.add (HCE.of_lval lv) lvalues.read }
diff --git a/src/plugins/eva/domains/hcexprs.mli b/src/plugins/eva/domains/hcexprs.mli
index b22664907a4..0b65e6e224e 100644
--- a/src/plugins/eva/domains/hcexprs.mli
+++ b/src/plugins/eva/domains/hcexprs.mli
@@ -22,7 +22,7 @@
(** Hash-consed expressions and lvalues. *)
-type unhashconsed_exprs = private E of Evast.exp | LV of Evast.lval
+type unhashconsed_exprs = private E of Eva_ast.exp | LV of Eva_ast.lval
(** lvalues are never stored under a constructor [E], only [LV] *)
(** Raised when the replacement of an lvalue in an expression is impossible. *)
@@ -46,18 +46,18 @@ module HCE: sig
(** Conversions between type [t] and Cil lvalues and expressions. *)
- val of_lval: Evast.lval -> t
- val of_exp: Evast.exp -> t
+ val of_lval: Eva_ast.lval -> t
+ val of_exp: Eva_ast.exp -> t
val get: t -> unhashconsed_exprs
- val to_exp: t -> Evast.exp
- val to_lval: t -> Evast.lval option
+ val to_exp: t -> Eva_ast.exp
+ val to_lval: t -> Eva_ast.lval option
val is_lval: t -> bool
val type_of: t -> Cil_types.typ
(** Replaces all occurrences of the lvalue [late] by the expression [heir].
@raise NonExchangeable if the replacement is not feasible. *)
- val replace: kill_type -> late:Evast.lval -> heir:Evast.exp -> t -> t
+ val replace: kill_type -> late:Eva_ast.lval -> heir:Eva_ast.exp -> t -> t
end
@@ -82,7 +82,7 @@ val empty_lvalues: lvalues
removed. This function only computes the first lvalues of the expression,
and does not go through the lvalues (for the expression t[i]+1, only the
lvalue t[i] is returned). *)
-val syntactic_lvalues: Evast.exp -> lvalues
+val syntactic_lvalues: Eva_ast.exp -> lvalues
(** Maps from symbolic expressions to their memory dependencies, expressed as a
diff --git a/src/plugins/eva/domains/inout_domain.ml b/src/plugins/eva/domains/inout_domain.ml
index 342a7be295a..0b2f3dd185b 100644
--- a/src/plugins/eva/domains/inout_domain.ml
+++ b/src/plugins/eva/domains/inout_domain.ml
@@ -162,7 +162,7 @@ module Transfer = struct
in [e] into locations. Nothing is written, the memory locations
present in [e] are read. *)
let effects_assume to_z e =
- let inputs = Evast.zone_of_exp to_z e in
+ let inputs = Eva_ast.zone_of_exp to_z e in
{
over_outputs = Zone.bottom;
over_inputs = inputs;
@@ -173,8 +173,8 @@ module Transfer = struct
(* Effects of an assigment [lv = e]. [to_z] converts the lvalues present
in [lv] and [e] into locations. *)
let effects_assign to_z lv e =
- let inputs_e = Evast.zone_of_exp to_z e in
- let inputs_lv = Evast.indirect_zone_of_lval to_z lv.Eval.lval in
+ let inputs_e = Eva_ast.zone_of_exp to_z e in
+ let inputs_lv = Eva_ast.indirect_zone_of_lval to_z lv.Eval.lval in
let inputs = Zone.join inputs_e inputs_lv in
let outputs =
Precise_locs.enumerate_valid_bits Locations.Write lv.Eval.lloc
diff --git a/src/plugins/eva/domains/multidim/abstract_memory.ml b/src/plugins/eva/domains/multidim/abstract_memory.ml
index ff77bb78a8f..a21015dba02 100644
--- a/src/plugins/eva/domains/multidim/abstract_memory.ml
+++ b/src/plugins/eva/domains/multidim/abstract_memory.ml
@@ -157,7 +157,7 @@ end
type size = Integer.t
type side = Left | Right
-type oracle = Evast.exp -> Int_val.t
+type oracle = Eva_ast.exp -> Int_val.t
type bioracle = side -> oracle
module type ProtoMemory =
@@ -190,5 +190,5 @@ sig
val incr_bound : oracle:oracle -> Cil_types.varinfo -> Integer.t option ->
t -> t
val add_segmentation_bounds : oracle:oracle -> typ:Cil_types.typ ->
- Evast.exp list -> t -> t
+ Eva_ast.exp list -> t -> t
end
diff --git a/src/plugins/eva/domains/multidim/abstract_memory.mli b/src/plugins/eva/domains/multidim/abstract_memory.mli
index 7b32e7e9636..620d0e4a621 100644
--- a/src/plugins/eva/domains/multidim/abstract_memory.mli
+++ b/src/plugins/eva/domains/multidim/abstract_memory.mli
@@ -62,7 +62,7 @@ type size = Integer.t
(* Oracles for memory abstraction *)
type side = Left | Right
-type oracle = Evast.exp -> Int_val.t
+type oracle = Eva_ast.exp -> Int_val.t
type bioracle = side -> oracle
(* Early stage of memory abstraction building *)
@@ -96,5 +96,5 @@ sig
val incr_bound : oracle:oracle -> Cil_types.varinfo -> Integer.t option ->
t -> t
val add_segmentation_bounds : oracle:oracle -> typ:Cil_types.typ ->
- Evast.exp list -> t -> t
+ Eva_ast.exp list -> t -> t
end
diff --git a/src/plugins/eva/domains/multidim/abstract_offset.ml b/src/plugins/eva/domains/multidim/abstract_offset.ml
index 35a34392969..b2d889194a2 100644
--- a/src/plugins/eva/domains/multidim/abstract_offset.ml
+++ b/src/plugins/eva/domains/multidim/abstract_offset.ml
@@ -25,7 +25,7 @@ open Top.Operators
type t =
| NoOffset of Cil_types.typ
- | Index of Evast.exp option * Int_val.t * Cil_types.typ * t
+ | Index of Eva_ast.exp option * Int_val.t * Cil_types.typ * t
| Field of Cil_types.fieldinfo * t
let rec pretty fmt = function
@@ -37,7 +37,7 @@ let rec pretty fmt = function
pretty s
| Index (Some e, i, _t, s) ->
Format.fprintf fmt "[%a∈%a]%a"
- Evast.pp_exp e
+ Eva_ast.pp_exp e
Int_val.pretty i
pretty s
@@ -61,10 +61,10 @@ let add_index oracle base exp =
let idx' = Int_val.add i (oracle exp) in
let e = match e with (* If i is singleton, we can use this as the index expression *)
| None when Int_val.is_singleton i ->
- Some (Evast.Build.integer (Int_val.project_int i))
+ Some (Eva_ast.Build.integer (Int_val.project_int i))
| e -> e
in
- let e' = Option.map (fun e -> Evast.Build.(add e exp)) e in
+ let e' = Option.map (fun e -> Eva_ast.Build.(add e exp)) e in
(* TODO: is idx inside bounds ? *)
`Value (Index (e', idx', t, sub))
| Index (e, i, t, sub) ->
@@ -85,7 +85,7 @@ let rec join o1 o2 =
| Index (e1, i1, t, sub1), Index (e2, i2, t', sub2)
when Bit_utils.type_compatible t t' ->
let e = match e1, e2 with
- | Some e1, Some e2 when Evast.Exp.equal e1 e2 ->
+ | Some e1, Some e2 when Eva_ast.Exp.equal e1 e2 ->
Some e1 (* keep expression only when equivalent from both offsets *)
| _ -> None
in
@@ -116,8 +116,8 @@ let assert_valid_index idx size =
let of_var_address vi =
NoOffset vi.Cil_types.vtype
-let rec of_evast_offset (oracle : Evast.exp -> Int_val.t) base_typ = function
- | Evast.NoOffset -> `Value (NoOffset base_typ)
+let rec of_evast_offset (oracle : Eva_ast.exp -> Int_val.t) base_typ = function
+ | Eva_ast.NoOffset -> `Value (NoOffset base_typ)
| Field (fi, sub) ->
if Cil.typeHasQualifier "volatile" fi.ftype then
`Top
@@ -246,7 +246,7 @@ let references =
| NoOffset _ -> acc
| Field (_, sub) | Index (None, _, _, sub) -> aux acc sub
| Index (Some e, _, _, sub) ->
- let r = Evast.vars_in_exp e in
+ let r = Eva_ast.vars_in_exp e in
let acc = Cil_datatype.Varinfo.Set.union r acc in
aux acc sub
in
diff --git a/src/plugins/eva/domains/multidim/abstract_offset.mli b/src/plugins/eva/domains/multidim/abstract_offset.mli
index 6608c1c1726..d5f4644d6a9 100644
--- a/src/plugins/eva/domains/multidim/abstract_offset.mli
+++ b/src/plugins/eva/domains/multidim/abstract_offset.mli
@@ -24,14 +24,14 @@ open Lattice_bounds
type t =
| NoOffset of Cil_types.typ
- | Index of Evast.exp option * Int_val.t * Cil_types.typ * t
+ | Index of Eva_ast.exp option * Int_val.t * Cil_types.typ * t
| Field of Cil_types.fieldinfo * t
val pretty : Format.formatter -> t -> unit
val of_var_address : Cil_types.varinfo -> t
-val of_evast_offset : (Evast.exp -> Int_val.t) ->
- Cil_types.typ -> Evast.offset -> t or_top
+val of_evast_offset : (Eva_ast.exp -> Int_val.t) ->
+ Cil_types.typ -> Eva_ast.offset -> t or_top
val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t or_top
val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t or_top
@@ -40,4 +40,4 @@ val references : t -> Cil_datatype.Varinfo.Set.t (* variables referenced in the
val append : t -> t -> t (* Does not check that the appened offset fits *)
val join : t -> t -> t or_top
-val add_index : (Evast.exp -> Int_val.t) -> t -> Evast.exp -> t or_top
+val add_index : (Eva_ast.exp -> Int_val.t) -> t -> Eva_ast.exp -> t or_top
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 814f90a2f6e..26cf2a953cf 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -177,9 +177,9 @@ struct
let of_lval oracle (lval : lval) : t or_top =
let (host,offset) = lval.node in
let oracle' = convert_oracle oracle in
- let base_typ = Evast.type_of_lhost host in
+ let base_typ = Eva_ast.type_of_lhost host in
let offset =
- if Evast.lval_contains_volatile lval then
+ if Eva_ast.lval_contains_volatile lval then
`Top
else
Offset.of_evast_offset oracle' base_typ offset in
@@ -413,19 +413,19 @@ struct
state referees
let update_var_references ~oracle (dst : Cil_types.varinfo)
- (src : Evast.exp option) (base_map,tracked : t) =
+ (src : Eva_ast.exp option) (base_map,tracked : t) =
let incr = Option.bind src (fun expr ->
- let is_dst (exp : Evast.exp) = match exp.node with
+ let is_dst (exp : Eva_ast.exp) = match exp.node with
| Lval { node = Var v, NoOffset } -> Cil_datatype.Varinfo.equal dst v
| _ -> false
in
match expr.node with
| BinOp ((PlusA|PlusPI), e1, e2, _typ) when is_dst e1 ->
- Evast.fold_to_integer e2
+ Eva_ast.fold_to_integer e2
| BinOp ((PlusA|PlusPI), e1, e2, _typ) when is_dst e2 ->
- Evast.fold_to_integer e1
+ Eva_ast.fold_to_integer e1
| BinOp ((MinusA|MinusPI), e1, e2, _typ) when is_dst e1 ->
- Option.map Integer.neg (Evast.fold_to_integer e2)
+ Option.map Integer.neg (Eva_ast.fold_to_integer e2)
| _ -> None)
in
(* [oracle] must be the oracle before the (non-invertible)
@@ -454,7 +454,7 @@ struct
base_map, tracked
let update_references ~oracle (dst : mdlocation)
- (src : Evast.exp option) (state : t) =
+ (src : Eva_ast.exp option) (state : t) =
let remove_references b state =
match Base.to_varinfo b with
| exception Base.Not_a_C_variable -> state (* only references to variables are kept *)
@@ -485,10 +485,10 @@ struct
let oracle = convert_oracle oracle in
read (Memory.get ~oracle) Value_or_Uninitialized.join state src
- let mk_oracle (state : state) : Evast.exp -> value =
+ let mk_oracle (state : state) : Eva_ast.exp -> value =
(* Until Eva gives access to good oracles, we use this poor stupid oracle
instead *)
- let rec oracle (exp : Evast.exp) =
+ let rec oracle (exp : Eva_ast.exp) =
match exp.node with
| Lval lval ->
begin match Location.of_lval oracle lval with
@@ -516,9 +516,9 @@ struct
| _ ->
Self.fatal
"This type of array index expression is not supported: %a"
- Evast.pp_exp exp
+ Eva_ast.pp_exp exp
in
- fun exp -> oracle (Evast.const_fold exp)
+ fun exp -> oracle (Eva_ast.const_fold exp)
let mk_bioracle s1 s2 =
let oracle_left = mk_oracle s1
@@ -673,7 +673,7 @@ struct
`Value (Value.top, None), Alarmset.all
let extract_lval ~oracle _context state lv _loc =
- if Cil.isScalarType lv.Evast.typ then
+ if Cil.isScalarType lv.Eva_ast.typ then
let oracle = fun exp ->
match oracle exp with
| `Value v, alarms when Alarmset.is_empty alarms -> v (* only use values safely evaluated *)
@@ -689,7 +689,7 @@ struct
Value_or_Uninitialized.get_v_normalized v >>-: (fun v -> v, None),
if Value_or_Uninitialized.is_initialized v
then
- let origin = Evast.to_cil_lval lv in
+ let origin = Eva_ast.to_cil_lval lv in
Alarmset.(set (Alarms.Uninitialized origin) True all)
else Alarmset.all
else
@@ -698,7 +698,7 @@ struct
(* Eva Transfer *)
- let valuation_to_oracle state valuation : Evast.exp -> value = fun exp ->
+ let valuation_to_oracle state valuation : Eva_ast.exp -> value = fun exp ->
let multidim_oracle = mk_oracle state in
match valuation.Abstract_domain.find exp with
| `Top -> multidim_oracle exp
@@ -708,7 +708,7 @@ struct
let assume_exp valuation expr record state' =
let* state = state' in
let oracle = valuation_to_oracle state valuation in
- match (expr : Evast.exp).node with
+ match (expr : Eva_ast.exp).node with
| Lval lv when Cil.isScalarType lv.typ ->
let value = Value_or_Uninitialized.from_flagged record.value in
if not (Value.is_topint (Value_or_Uninitialized.get_v value)) then
@@ -771,7 +771,7 @@ struct
let oracle = valuation_to_oracle state valuation in
let bind state arg =
state >>-:
- assign' ~oracle ~value:arg.avalue (Evast.Build.var arg.formal) (Some arg.concrete)
+ assign' ~oracle ~value:arg.avalue (Eva_ast.Build.var arg.formal) (Some arg.concrete)
in
List.fold_left bind (`Value state) call.arguments
@@ -782,11 +782,11 @@ struct
let args = List.map (fun arg -> arg.avalue) call.arguments in
let+ assigned_result = f args in
let oracle = mk_oracle post in
- let dst = Evast.Build.var return in
+ let dst = Eva_ast.Build.var return in
assign' ~oracle ~value:assigned_result dst None post
let show_expr valuation state fmt expr =
- match (expr : Evast.exp).node with
+ match (expr : Eva_ast.exp).node with
| Lval lval | StartOf lval ->
let oracle = valuation_to_oracle state valuation in
begin match Location.of_lval oracle lval with
@@ -856,8 +856,8 @@ struct
let annotation = Eva_annotations.read_array_segmentation extension in
let vi,offset,bounds = annotation in
(* Update the segmentation *)
- let bounds = List.map Evast.translate_exp bounds in
- let lval = Evast.translate_lval (Var vi, offset) in
+ let bounds = List.map Eva_ast.translate_exp bounds in
+ let lval = Eva_ast.translate_lval (Var vi, offset) in
let oracle = mk_oracle state in
begin match Location.of_lval oracle lval with
| `Top -> state
@@ -869,7 +869,7 @@ struct
let state = write update state loc in
(* Update the references *)
let add acc e =
- let r = Evast.vars_in_exp e in
+ let r = Eva_ast.vars_in_exp e in
(Cil_datatype.Varinfo.Set.to_seq r |> List.of_seq) @ acc
in
let references = List.fold_left add [] bounds in
@@ -905,7 +905,7 @@ struct
erase ~oracle state dst d
let initialize_variable_using_type _kind vi state =
- let lval = Evast.Build.var vi in
+ let lval = Eva_ast.Build.var vi in
let oracle = mk_oracle state in
match Location.of_lval oracle lval with
| `Top -> top
diff --git a/src/plugins/eva/domains/multidim/segmentation.ml b/src/plugins/eva/domains/multidim/segmentation.ml
index 764d781cff6..0dc39ef6a66 100644
--- a/src/plugins/eva/domains/multidim/segmentation.ml
+++ b/src/plugins/eva/domains/multidim/segmentation.ml
@@ -103,15 +103,15 @@ struct
module Var = Cil_datatype.Varinfo
module Exp =
struct
- include Evast.Exp
+ include Eva_ast.Exp
let equal e1 e2 =
if e1 == e2 then true else equal e1 e2
end
type t =
| Const of Integer.t
- | Exp of Evast.exp * Integer.t (* x + c *)
- | Ptroffset of Evast.exp * Cil_types.offset * Integer.t (* (x - &b.offset) + c *)
+ | Exp of Eva_ast.exp * Integer.t (* x + c *)
+ | Ptroffset of Eva_ast.exp * Cil_types.offset * Integer.t (* (x - &b.offset) + c *)
let pretty fmt : t -> unit = function
| Const i -> Integer.pretty fmt i
@@ -153,7 +153,7 @@ struct
exception NonLinear
(* Find a coefficient before vi in exp *)
- let rec linearity vi (exp : Evast.exp) =
+ let rec linearity vi (exp : Eva_ast.exp) =
match exp.node with
| Const _
| AddrOf _ | StartOf _ -> Integer.zero
@@ -182,21 +182,21 @@ struct
(* Check that the linearity of any variable is not hidden into a mem access *)
ignore (linearity Var.dummy exp)
- let of_exp (exp : Evast.exp) =
+ let of_exp (exp : Eva_ast.exp) =
check_support exp;
(* Normalizes x + c, c + x and x - c *)
- match Evast.fold_to_integer exp with
+ match Eva_ast.fold_to_integer exp with
| Some i -> Const i
| None ->
match exp.node with
| BinOp ((PlusA|PlusPI), e1, e2, _typ) ->
- begin match Evast.(fold_to_integer e1, fold_to_integer e2) with
+ begin match Eva_ast.(fold_to_integer e1, fold_to_integer e2) with
| None, Some i -> Exp (e1, i)
| Some i, None -> Exp (e2, i)
| _ -> Exp (exp, Integer.zero)
end
| BinOp ((MinusA|MinusPI), e1, e2, _typ) ->
- begin match Evast.fold_to_integer e2 with
+ begin match Eva_ast.fold_to_integer e2 with
| Some i -> Exp (e1, Integer.neg i)
| None -> Exp (exp, Integer.zero)
end
diff --git a/src/plugins/eva/domains/multidim/segmentation.mli b/src/plugins/eva/domains/multidim/segmentation.mli
index 6caad373072..4b5d523e385 100644
--- a/src/plugins/eva/domains/multidim/segmentation.mli
+++ b/src/plugins/eva/domains/multidim/segmentation.mli
@@ -34,7 +34,7 @@ module Bound :
sig
type t
exception UnsupportedBoundExpression
- val of_exp : Evast.exp -> t
+ val of_exp : Eva_ast.exp -> t
val of_integer : Integer.t -> t
val succ : t -> t
end
diff --git a/src/plugins/eva/domains/multidim/typed_memory.mli b/src/plugins/eva/domains/multidim/typed_memory.mli
index 4c6f64331a9..7d4baefd196 100644
--- a/src/plugins/eva/domains/multidim/typed_memory.mli
+++ b/src/plugins/eva/domains/multidim/typed_memory.mli
@@ -121,5 +121,5 @@ sig
(* Update the array segmentation at the given offset so the given bound
expressions appear in the segmentation *)
val segmentation_hint : oracle:oracle ->
- t -> location -> Evast.exp list -> t
+ t -> location -> Eva_ast.exp list -> t
end
diff --git a/src/plugins/eva/domains/numerors/numerors_value.ml b/src/plugins/eva/domains/numerors/numerors_value.ml
index 37551cf346b..85485626c68 100644
--- a/src/plugins/eva/domains/numerors/numerors_value.ml
+++ b/src/plugins/eva/domains/numerors/numerors_value.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
open Eval
-open Evast
+open Eva_ast
open Numerors_utils
module I = Numerors_interval
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index e4c8e57a46a..90a0f6e707a 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
open Eval
-open Evast
+open Eva_ast
(* If [true], checks invariants of the states created by most functions. *)
let debug = false
@@ -141,7 +141,7 @@ module Variable : Variable = struct
let lval (var, _) =
match var with
- | Var vi -> Some (Evast.Build.var vi)
+ | Var vi -> Some (Eva_ast.Build.var vi)
| Lval lval -> HCE.to_lval lval
| Int _ | StartOf _ -> None
@@ -155,7 +155,7 @@ module Variable : Variable = struct
| StartOf _ ->
{ data = Locations.Zone.bottom ; indirect = Locations.Zone.bottom }
| Lval lval ->
- Evast.deps_of_lval eval_loc (Option.get (HCE.to_lval lval))
+ Eva_ast.deps_of_lval eval_loc (Option.get (HCE.to_lval lval))
end
module VarSet =
@@ -432,7 +432,7 @@ module Rewriting = struct
(* Returns the range of the expression X-Y when the comparison X#Y holds. *)
let comparison_range =
function
- | Evast.Lt -> Ival.inject_range None (Some Integer.minus_one)
+ | Eva_ast.Lt -> Ival.inject_range None (Some Integer.minus_one)
| Gt -> Ival.inject_range (Some Integer.one) None
| Le -> Ival.inject_range None (Some Integer.zero)
| Ge -> Ival.inject_range (Some Integer.zero) None
@@ -442,7 +442,7 @@ module Rewriting = struct
(* Transforms the constraint [expr] ∈ [ival] into a list of octagonal
constraints. *)
- let make_octagons evaluate env (expr : Evast.exp) ival =
+ let make_octagons evaluate env (expr : Eva_ast.exp) ival =
let make_octagons_from_binop kind e1 op e2 ival =
(* equivalent octagonal forms ±(X±Y-v) for [e1 op e2]. *)
let rewritings = rewrite_binop evaluate env e1 op e2 in
@@ -466,7 +466,7 @@ module Rewriting = struct
else
let comp =
if Ival.is_zero ival
- then Evast.invert_relation binop
+ then Eva_ast.invert_relation binop
else binop
in
let range = comparison_range comp in
@@ -484,7 +484,7 @@ module Rewriting = struct
let aux has_better_bound bound bound_kind alarms =
if Ival.is_bottom ival || has_better_bound ival ival_range >= 0
then
- let cil_expr = Evast.to_cil_exp expr in
+ let cil_expr = Eva_ast.to_cil_exp expr in
let alarm = Alarms.Overflow (overflow, cil_expr, bound, bound_kind) in
Alarmset.set alarm Alarmset.True alarms
else alarms
@@ -500,7 +500,7 @@ module Rewriting = struct
constraints using [evaluate_expr] to evaluate sub-expressions, and
then using [evaluate_octagon] to evaluate the octagons. *)
let evaluate_through_octagons (eval : evaluator) evaluate_octagon env
- (expr : Evast.exp) =
+ (expr : Eva_ast.exp) =
let evaluate_octagon acc (sign, octagon) =
match evaluate_octagon octagon with
| None -> acc
@@ -1300,7 +1300,7 @@ module State = struct
match exp.node with
| Lval lval
when Cil.isIntegralOrPointerType lval.typ
- && not (Evast.lval_contains_volatile lval)
+ && not (Eva_ast.lval_contains_volatile lval)
&& not (is_singleton (eval exp)) ->
Some (Variable.make_lval lval, Ival.zero)
@@ -1682,7 +1682,7 @@ module Domain = struct
in
let y_ival = Ival.narrow y_ival1 y_ival2 in
if Ival.(equal top y_ival) then acc else
- let y_expr = Evast.Build.lval lval in
+ let y_expr = Eva_ast.Build.lval lval in
let y_cvalue = Cvalue.V.inject_ival y_ival in
(y_expr, y_cvalue) :: acc
in
@@ -1720,7 +1720,7 @@ module Domain = struct
else
match expr.node with
| Lval lval when Cil.(isIntegralType lval.typ)
- && not (Evast.lval_contains_volatile lval) ->
+ && not (Eva_ast.lval_contains_volatile lval) ->
let var = Variable.make_lval lval in
let deps = Deps.add var (eval_deps var) state.deps in
let intervals = Intervals.add var ival state.intervals in
@@ -1786,7 +1786,7 @@ module Domain = struct
with Not_found -> State.remove state variable
in
let state = assign_interval eval_deps variable assigned state in
- let left_expr = Evast.Build.lval lvalue in
+ let left_expr = Eva_ast.Build.lval lvalue in
(* On the assignment X = E; if X-E can be rewritten as ±(X±Y-v),
then the octagonal constraint [X±Y ∈ v] holds. *)
let octagons = Rewriting.rewrite_binop eval_exp env left_expr Sub expr in
@@ -1802,7 +1802,7 @@ module Domain = struct
let assign kinstr left_value expr assigned valuation state =
if kinstr <> Cil_types.Kglobal
&& Cil.isIntegralOrPointerType left_value.lval.typ
- && not (Evast.lval_contains_volatile left_value.lval)
+ && not (Eva_ast.lval_contains_volatile left_value.lval)
then assign_variable left_value.lval expr assigned valuation state
else
let written_loc = Precise_locs.imprecise_location left_value.lloc in
@@ -1834,7 +1834,7 @@ module Domain = struct
`Value (start_recursive_call recursion state)
| None ->
let assign_formal state { formal; concrete; avalue } =
- let lval = Evast.Build.var formal in
+ let lval = Eva_ast.Build.var formal in
if Cil.isIntegralOrPointerType formal.vtype
then state >>- assign_variable lval concrete avalue valuation
else state
diff --git a/src/plugins/eva/domains/offsm_domain.ml b/src/plugins/eva/domains/offsm_domain.ml
index 3c845092e20..190deb18e57 100644
--- a/src/plugins/eva/domains/offsm_domain.ml
+++ b/src/plugins/eva/domains/offsm_domain.ml
@@ -185,8 +185,8 @@ module D : Abstract_domain.Leaf
let extract_lval ~oracle:_ _context state lv locs =
let o =
- if Cil.typeHasQualifier "volatile" lv.Evast.typ ||
- not (Cil.isArithmeticOrPointerType lv.Evast.typ)
+ if Cil.typeHasQualifier "volatile" lv.Eva_ast.typ ||
+ not (Cil.isArithmeticOrPointerType lv.Eva_ast.typ)
then
`Value (Top, None)
else
diff --git a/src/plugins/eva/domains/printer_domain.ml b/src/plugins/eva/domains/printer_domain.ml
index 86cd9a4b2ac..3b8150832a9 100644
--- a/src/plugins/eva/domains/printer_domain.ml
+++ b/src/plugins/eva/domains/printer_domain.ml
@@ -71,19 +71,19 @@ module Simple : Simpler_domains.Simple_Cvalue = struct
let pp_arg fmt arg =
Format.fprintf fmt "%a = %a"
- Evast.pp_exp arg.concrete
+ Eva_ast.pp_exp arg.concrete
pp_cvalue_assigned arg.avalue
let assign _kinstr loc exp cvalue_assigned _valuation state =
feedback "assign %a with %a = %a"
- Evast.pp_lval loc.lval
- Evast.pp_exp exp
+ Eva_ast.pp_lval loc.lval
+ Eva_ast.pp_exp exp
pp_cvalue_assigned cvalue_assigned;
`Value state
let assume _stmt exp truth _valuation state =
feedback "assume %a is %b"
- Evast.pp_exp exp
+ Eva_ast.pp_exp exp
truth;
`Value state
@@ -112,7 +112,7 @@ module Simple : Simpler_domains.Simple_Cvalue = struct
let initialize_variable lval ~initialized:_ init state =
feedback "initialize_variable %a with %a"
- Evast.pp_lval lval
+ Eva_ast.pp_lval lval
pp_init_val init;
state
diff --git a/src/plugins/eva/domains/simple_memory.ml b/src/plugins/eva/domains/simple_memory.ml
index 3c3719544c8..39aef1ca1f1 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -204,14 +204,14 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
corresponding to [_lv], so that it may be used by the engine during
evaluation. *)
let extract_lval ~oracle:_ _context state lv loc =
- let v = find loc lv.Evast.typ state in
+ let v = find loc lv.Eva_ast.typ state in
`Value (v, None), Alarmset.all
let extract_expr ~oracle:_ _context _state _expr =
`Value (Value.top, None), Alarmset.all
let backward_location state lval loc _value =
- let new_value = find loc lval.Evast.typ state in
+ let new_value = find loc lval.Eva_ast.typ state in
`Value (loc, new_value)
(* This function binds [loc] to [v], of type [typ], in [state].
@@ -229,7 +229,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
location with the result of the evaluation of [exp]. Both the value and
the location are found in the [valuation]. *)
let assume_exp valuation expr record state =
- match (expr : Evast.exp).node with
+ match (expr : Eva_ast.exp).node with
| Lval lv -> begin
match valuation.Abstract_domain.find_loc lv with
| `Top -> state
@@ -308,7 +308,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
bind_loc return_loc return.vtype (`Value result) post
let show_expr valuation state fmt expr =
- match (expr : Evast.exp).node with
+ match (expr : Eva_ast.exp).node with
| Lval lval ->
begin
match valuation.Abstract_domain.find_loc lval with
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index 8d72449d972..276e06c028b 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
open Eval
-open Evast
+open Eva_ast
open Locations
let dkey = Self.register_category "d-symblocs"
@@ -146,10 +146,10 @@ let vars_to_bases vi_set =
|> Base.Set.of_seq
let vars_lv lv =
- vars_to_bases (Evast.vars_in_lval lv)
+ vars_to_bases (Eva_ast.vars_in_lval lv)
let vars_exp (e: exp) =
- vars_to_bases (Evast.vars_in_exp e)
+ vars_to_bases (Eva_ast.vars_in_exp e)
(* Legacy names *)
module B2K = K.BaseToHCESet
@@ -367,12 +367,12 @@ module Memory = struct
(* Add the the mapping [lv --> v] to [state] when possible.
[get_z] is a function that computes dependencies. *)
let add_lv state get_z lv v =
- if Evast.lval_contains_volatile lv then
+ if Eva_ast.lval_contains_volatile lv then
state
else
let k = K.HCE.of_lval lv in
let z_lv = Precise_locs.enumerate_valid_bits Locations.Read (get_z lv) in
- let z_lv_indirect = Evast.indirect_zone_of_lval get_z lv in
+ let z_lv_indirect = Eva_ast.indirect_zone_of_lval get_z lv in
if Locations.Zone.intersects z_lv z_lv_indirect then
(* The location of [lv] intersects with the zones needed to compute
itself, the equality would not hold. *)
@@ -384,11 +384,11 @@ module Memory = struct
(* Add the mapping [e --> v] to [state] when possible and useful.
[get_z] is a function that computes dependencies. *)
let add_exp state get_z e v =
- if Evast.exp_contains_volatile e then
+ if Eva_ast.exp_contains_volatile e then
state
else
let k = K.HCE.of_exp e in
- let z = Evast.zone_of_exp get_z e in
+ let z = Eva_ast.zone_of_exp get_z e in
add_key k v z state
let find k state =
@@ -485,7 +485,7 @@ module D : Abstract_domain.Leaf
| `Value loc -> loc.Eval.loc
in
if Precise_locs.(equal_loc loc_top r) then
- Self.fatal "Unknown location for %a" Evast.pp_lval lv
+ Self.fatal "Unknown location for %a" Eva_ast.pp_lval lv
else r
let get_val valuation = fun lv ->
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index be49880df44..e434f1c04cb 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -186,7 +186,7 @@ module TransferTaint = struct
- its indirect dependencies, i.e. the memory zone its location depends on;
- whether its location is a singleton. *)
let compute_zones lval to_loc =
- match (lval : Evast.lval).node with
+ match (lval : Eva_ast.lval).node with
| Var vi, NoOffset ->
(* Special case for direct access to variable: do not use [to_loc] here,
as it will fail for the formal parameters of calls. *)
@@ -199,13 +199,13 @@ module TransferTaint = struct
let loc = Precise_locs.imprecise_location ploc in
Locations.enumerate_valid_bits Write loc
in
- let lv_indirect_zone = Evast.indirect_zone_of_lval to_loc lval in
+ let lv_indirect_zone = Eva_ast.indirect_zone_of_lval to_loc lval in
lv_zone, lv_indirect_zone, singleton
(* Propagates data- and control-taints for an assignement [lval = exp]. *)
let assign_aux lval exp to_loc state =
let lv_zone, lv_indirect_zone, singleton = compute_zones lval to_loc in
- let exp_zone = Evast.zone_of_exp to_loc exp in
+ let exp_zone = Eva_ast.zone_of_exp to_loc exp in
(* [lv] becomes data-tainted if a memory location on which the value of
[exp] depends on is data-tainted. *)
let data_tainted = Zone.intersects state.locs_data exp_zone in
@@ -246,7 +246,7 @@ module TransferTaint = struct
let state = filter_active_tainted_assumes stmt state in
(* Add [stmt] as assume statement in [state] as soon as [exp] is tainted. *)
let to_loc = loc_of_lval valuation in
- let exp_zone = Evast.zone_of_exp to_loc exp in
+ let exp_zone = Eva_ast.zone_of_exp to_loc exp in
let state =
if not state.dependent_call && LatticeTaint.intersects state exp_zone
then { state with assume_stmts = Stmt.Set.add stmt state.assume_stmts; }
@@ -265,7 +265,7 @@ module TransferTaint = struct
let to_loc = loc_of_lval valuation in
List.fold_left
(fun s { Eval.concrete; formal; _ } ->
- assign_aux (Evast.Build.var formal) concrete to_loc s)
+ assign_aux (Eva_ast.Build.var formal) concrete to_loc s)
state
call.Eval.arguments
in
@@ -279,7 +279,7 @@ module TransferTaint = struct
let show_expr valuation state fmt exp =
let to_loc = loc_of_lval valuation in
- let exp_zone = Evast.zone_of_exp to_loc exp in
+ let exp_zone = Eva_ast.zone_of_exp to_loc exp in
Format.fprintf fmt "%B" (LatticeTaint.intersects state exp_zone)
end
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index b86171afadb..72a5125eee1 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -1102,13 +1102,13 @@ module D = struct
let log_category = Self.register_category "d-traces"
let assign ki lv e _v _valuation state =
- let cil_lval = Evast.to_cil_lval lv.Eval.lval in
- let cil_exp = Evast.to_cil_exp e in
+ let cil_lval = Eva_ast.to_cil_lval lv.Eval.lval in
+ let cil_exp = Eva_ast.to_cil_exp e in
let trans = Assign (ki, cil_lval, lv.lval.typ, cil_exp) in
`Value (Traces.add_trans state trans)
let assume stmt e pos _valuation state =
- let cil_exp = Evast.to_cil_exp e in
+ let cil_exp = Eva_ast.to_cil_exp e in
let trans = Assume (stmt, cil_exp, pos) in
`Value (Traces.add_trans state trans)
@@ -1124,7 +1124,7 @@ module D = struct
Traces.add_trans state
(Assign (Kstmt stmt, Cil.var arg.Eval.formal,
arg.Eval.formal.Cil_types.vtype,
- Evast.to_cil_exp arg.Eval.concrete)))
+ Eva_ast.to_cil_exp arg.Eval.concrete)))
state call.Eval.arguments in
`Value state
else
@@ -1135,7 +1135,7 @@ module D = struct
| None -> state in
let exps =
List.map
- (fun arg -> Evast.to_cil_exp arg.Eval.concrete)
+ (fun arg -> Eva_ast.to_cil_exp arg.Eval.concrete)
call.Eval.arguments
in
let state = Traces.add_trans state
@@ -1158,7 +1158,7 @@ module D = struct
let empty () = Traces.empty
let initialize_variable lv _ ~initialized:_ _ state =
- Traces.add_trans state (Msg(Format.asprintf "initialize variable: %a" Evast.pp_lval lv ))
+ Traces.add_trans state (Msg(Format.asprintf "initialize variable: %a" Eva_ast.pp_lval lv ))
let initialize_variable_using_type var_kind varinfo state =
let kind_str =
match var_kind with
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index cfe99726cc9..261690521d2 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -119,7 +119,7 @@
(mode (promote (only Eva.mli)))
(deps
gen_api/Eva.header
- engine/analysis.mli types/callstack.mli types/deps.mli ast/evast.mli
+ engine/analysis.mli types/callstack.mli types/deps.mli ast/eva_ast.mli
utils/results.mli parameters.mli
utils/eva_annotations.mli eval.mli types/assigns.mli
domains/cvalue/builtins.mli utils/cvalue_callbacks.mli legacy/logic_inout.mli
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index fb66e58aa64..aa085ed66b3 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -24,7 +24,7 @@
open Cil_types
open Eval
-open Evast
+open Eva_ast
(* The forward evaluation of an expression [e] gives a value to each subterm
of [e], from its variables to the root expression [e]. It also computes the
@@ -172,7 +172,7 @@ let rec signed_counterpart typ =
let exp_alarm_signed_converted_downcast exp =
let src_typ = exp.typ in
let signed_typ = signed_counterpart src_typ in
- Evast.Build.(cast signed_typ exp)
+ Eva_ast.Build.(cast signed_typ exp)
let return t = `Value t, Alarmset.none
@@ -247,8 +247,8 @@ module Make
type origin = Domain.origin
type loc = Loc.location
- module ECache = Evast.Exp.Map
- module LCache = Evast.Lval.Map
+ module ECache = Eva_ast.Exp.Map
+ module LCache = Eva_ast.Lval.Map
(* Imperative cache for the evaluation:
all intermediate results of an evaluation are cached here.
@@ -394,7 +394,7 @@ module Make
let truncate_bound overflow_kind bound bound_kind expr value =
let alarm () =
- let cil_expr = Evast.to_cil_exp expr in (* The expression does not necessary come from the original program *)
+ let cil_expr = Eva_ast.to_cil_exp expr in (* The expression does not necessary come from the original program *)
Alarms.Overflow (overflow_kind, cil_expr, bound, bound_kind)
in
let bound = Abstract_value.Int bound in
@@ -432,7 +432,7 @@ module Make
let restrict_float ?(reduce=false) ~assume_finite expr fkind value =
let truth = Value.assume_not_nan ~assume_finite fkind value in
let alarm () =
- let cil_expr = Evast.to_cil_exp expr in
+ let cil_expr = Eva_ast.to_cil_exp expr in
if assume_finite
then Alarms.Is_nan_or_infinite (cil_expr, fkind)
else Alarms.Is_nan (cil_expr, fkind)
@@ -453,7 +453,7 @@ module Make
let+ value =
if Kernel.InvalidPointer.get () then
let truth = Value.assume_pointer value in
- let cil_expr = Evast.to_cil_exp expr in
+ let cil_expr = Eva_ast.to_cil_exp expr in
let alarm () = Alarms.Invalid_pointer cil_expr in
interpret_truth ~alarm value truth
else return value
@@ -485,17 +485,17 @@ module Make
let* value, origin = res in
match lval.typ with
| TFloat (fkind, _) ->
- let expr = Evast.Build.lval lval in
+ let expr = Eva_ast.Build.lval lval in
let+ new_value = remove_special_float expr fkind value in
new_value, origin
| TInt (IBool, _) when Kernel.InvalidBool.get () ->
let one = Abstract_value.Int Integer.one in
let truth = Value.assume_bounded Alarms.Upper_bound one value in
- let alarm () = Alarms.Invalid_bool (Evast.to_cil_lval lval) in
+ let alarm () = Alarms.Invalid_bool (Eva_ast.to_cil_lval lval) in
let+ new_value = interpret_truth ~alarm value truth in
new_value, origin
| TPtr _ ->
- let expr = Evast.Build.lval lval in
+ let expr = Eva_ast.Build.lval lval in
let+ new_value = assume_pointer context expr value in
new_value, origin
| _ -> res
@@ -507,7 +507,7 @@ module Make
let size_int = Abstract_value.Int (Integer.of_int (size - 1)) in
let zero_int = Abstract_value.Int Integer.zero in
let alarm () =
- Alarms.Invalid_shift (Evast.to_cil_exp expr, Some size)
+ Alarms.Invalid_shift (Eva_ast.to_cil_exp expr, Some size)
in
let truth = Value.assume_bounded Alarms.Lower_bound zero_int value in
let* value = reduce_by_truth ~alarm (expr, value) truth in
@@ -523,7 +523,7 @@ module Make
(* Cannot shift a negative value *)
let zero_int = Abstract_value.Int Integer.zero in
let alarm () =
- Alarms.Invalid_shift (Evast.to_cil_exp e1, None)
+ Alarms.Invalid_shift (Eva_ast.to_cil_exp e1, None)
in
let truth = Value.assume_bounded Alarms.Lower_bound zero_int v1 in
let+ v1 = reduce_by_truth ~alarm (e1, v1) truth in
@@ -535,7 +535,7 @@ module Make
let open Evaluated.Operators in
let size_int = Abstract_value.Int (Integer.pred size) in
let zero_int = Abstract_value.Int Integer.zero in
- let alarm_index_expr () = Evast.to_cil_exp index_expr in
+ let alarm_index_expr () = Eva_ast.to_cil_exp index_expr in
let alarm () = Alarms.Index_out_of_bound (alarm_index_expr (), None) in
let truth = Value.assume_bounded Alarms.Lower_bound zero_int value in
let* value = reduce_by_truth ~alarm (index_expr, value) truth in
@@ -551,7 +551,7 @@ module Make
match op with
| Div | Mod ->
let truth = Value.assume_non_zero v2 in
- let alarm () = Alarms.Division_by_zero (Evast.to_cil_exp e2) in
+ let alarm () = Alarms.Division_by_zero (Eva_ast.to_cil_exp e2) in
let+ v2 = reduce_by_truth ~alarm arg2 truth in
v1, v2
| Shiftrt ->
@@ -565,8 +565,8 @@ module Make
let truth = Value.assume_comparable kind v1 v2 in
let alarm () =
Alarms.Differing_blocks (
- Evast.to_cil_exp e1,
- Evast.to_cil_exp e2)
+ Eva_ast.to_cil_exp e1,
+ Eva_ast.to_cil_exp e2)
in
let arg1 = Some e1, v1 in
reduce_by_double_truth ~alarm arg1 arg2 truth
@@ -585,8 +585,8 @@ module Make
let truth = Value.assume_comparable kind v1 v2 in
let alarm () =
Alarms.Pointer_comparison (
- Option.map Evast.to_cil_exp e1,
- Evast.to_cil_exp e2)
+ Option.map Eva_ast.to_cil_exp e1,
+ Eva_ast.to_cil_exp e2)
in
let propagate_all = propagate_all_pointer_comparison typ in
let args, alarms =
@@ -619,7 +619,7 @@ module Make
| Some kind ->
let compute v1 v2 = Value.forward_binop context typ_e1 op v1 v2 in
(* Detect zero expressions created by the evaluator *)
- let e1 = if Evast.is_zero_ptr e1 then None else Some e1 in
+ let e1 = if Eva_ast.is_zero_ptr e1 then None else Some e1 in
forward_comparison ~compute typ_e1 kind (e1, v1) arg2
| None ->
let& v1, v2 = assume_valid_binop typ arg1 op arg2 in
@@ -711,7 +711,7 @@ module Make
then prev_float (Fval.kind fkind) fbound
else fbound
in
- let cil_expr = Evast.to_cil_exp expr in
+ let cil_expr = Eva_ast.to_cil_exp expr in
let alarm () = Alarms.Float_to_int (cil_expr, bound, bound_kind) in
let bound = Abstract_value.Float (float_bound, fkind) in
let truth = Value.assume_bounded bound_kind bound value in
@@ -973,10 +973,10 @@ module Make
let lval_to_loc = internal_lval_to_loc env ~for_writing ~reduction in
let* loc, volatile = lval_to_loc lval in
if reduction then
- let bitfield = Evast.is_bitfield lval in
+ let bitfield = Eva_ast.is_bitfield lval in
let truth = Loc.assume_valid_location ~for_writing ~bitfield loc in
let access = Alarms.(if for_writing then For_writing else For_reading) in
- let cil_lval = Evast.to_cil_lval lval in
+ let cil_lval = Eva_ast.to_cil_lval lval in
let alarm () = Alarms.Memory_access (cil_lval, access) in
let+ valid_loc = interpret_truth ~alarm loc truth in
let reduction = if Loc.equal_loc valid_loc loc then Neither else Forward in
@@ -989,12 +989,12 @@ module Make
and internal_lval_to_loc env ~for_writing ~reduction lval =
let open Evaluated.Operators in
let host, offset = lval.node in
- let basetyp = Evast.type_of_lhost host in
+ let basetyp = Eva_ast.type_of_lhost host in
let reduce_valid_index = reduction in
let evaluated = eval_offset env ~reduce_valid_index basetyp offset in
let* (offs, offset_volatile) = evaluated in
if for_writing && Eva_utils.is_const_write_invalid lval.typ then
- let cil_lval = Evast.to_cil_lval lval in
+ let cil_lval = Eva_ast.to_cil_lval lval in
let alarm = Alarms.(Memory_access (cil_lval, For_writing)) in
`Bottom, Alarmset.singleton ~status:Alarmset.False alarm
else
@@ -1069,7 +1069,7 @@ module Make
- if it contains a sub-expression which is volatile (volatile_expr)
*)
let volatile = volatile_expr || Cil.typeHasQualifier "volatile" lval.typ in
- let cil_lval = Evast.to_cil_lval lval in
+ let cil_lval = Eva_ast.to_cil_lval lval in
(* Find the value of the location, if not bottom. *)
let v, alarms = domain_query lval loc in
let alarms = close_dereference_alarms cil_lval alarms in
@@ -1284,7 +1284,7 @@ module Make
match expr.node with
| Lval _lv -> assert false
| UnOp (LNot, e, _) ->
- let cond = Evast.normalize_condition e false in
+ let cond = Eva_ast.normalize_condition e false in
(* TODO: should we compute the meet with the result of the call to
Value.backward_unop? *)
backward_eval fuel context state cond (Some value)
@@ -1537,7 +1537,7 @@ module Make
let copy_lvalue ?(valuation=Cache.empty) ?subdivnb state lval =
let open Evaluated.Operators in
- let expr = Evast.Build.lval lval in
+ let expr = Eva_ast.Build.lval lval in
let* env = root_environment ?subdivnb state, Alarmset.none in
try
let record, report = Cache.find' valuation expr in
@@ -1575,7 +1575,7 @@ module Make
(* If [for_writing] is true, the location of [lval] is reduced by removing
const bases. Use [for_writing:false] if const bases can be written
through a mutable field or an initializing function. *)
- let mutable_or_init = Evast.(is_mutable lval || is_initialized lval) in
+ let mutable_or_init = Eva_ast.(is_mutable lval || is_initialized lval) in
let for_writing = for_writing && not mutable_or_init in
let (host, offset) = lval.node in
let* valuation = evaluate_host valuation ?subdivnb state host in
@@ -1592,7 +1592,7 @@ module Make
let reduce ?valuation:(valuation=Cache.empty) state expr positive =
let open Evaluated.Operators in
(* Generate [e == 0] *)
- let expr = Evast.normalize_condition expr (not positive) in
+ let expr = Eva_ast.normalize_condition expr (not positive) in
cache := valuation;
(* Currently, no subdivisions are performed during the forward evaluation
in this function, which is used to evaluate the conditions of if(…)
@@ -1636,7 +1636,7 @@ module Make
else
Self.fatal ~current:true
"Function pointer evaluates to anything. function %a"
- Evast.pp_exp funcexp
+ Eva_ast.pp_exp funcexp
(* For pointer calls, we retro-propagate which function is being called
in the abstract state. This may be useful:
@@ -1647,7 +1647,7 @@ module Make
let backward_function_pointer valuation state expr kf =
(* Builds the expression [exp_f != &f], and assumes it is false. *)
let vi_f = Kernel_function.get_vi kf in
- let expr = Evast.Build.(ne expr (addr (var vi_f))) in
+ let expr = Eva_ast.Build.(ne expr (addr (var vi_f))) in
fst (reduce ~valuation state expr false)
let eval_function_exp ?subdivnb funcexp ?args state =
@@ -1677,8 +1677,8 @@ module Make
else if alarm || alarm' then Alarmset.Unknown
else Alarmset.True
in
- let cil_v = Evast.to_cil_exp v in
- let cil_args = Option.map (List.map (Evast.to_cil_exp)) args in
+ let cil_v = Eva_ast.to_cil_exp v in
+ let cil_args = Option.map (List.map (Eva_ast.to_cil_exp)) args in
let alarm = Alarms.Function_pointer (cil_v, cil_args) in
let alarms = Alarmset.singleton ~status alarm in
Bottom.bot_of_list list, alarms
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index af795a414b7..b7e8df368b5 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -24,7 +24,7 @@
open Cil_types
open Eval
-open Evast
+open Eva_ast
module type S = sig
type state
@@ -107,7 +107,7 @@ module Make
(* Initializes an entire variable [vi], in particular padding bits,
according to [local] and [lib_entry] mode. *)
let initialize_var_padding ~local ~lib_entry vi state =
- let lval = Evast.Build.var vi in
+ let lval = Eva_ast.Build.var vi in
match padding_initialization ~local with
| `Uninitialized -> state
| `Initialized | `MaybeInitialized as i ->
@@ -133,7 +133,7 @@ module Make
| `Bottom ->
if kinstr = Kglobal then
Self.warning ~once:true ~source
- "evaluation of initializer '%a' failed@." Evast.pp_exp expr;
+ "evaluation of initializer '%a' failed@." Eva_ast.pp_exp expr;
raise Initialization_failed
| `Value v -> v
@@ -150,7 +150,7 @@ module Make
apply_evast_single_initializer ~source kinstr state lval exp
| CompoundInit (_typ, l) ->
let doinit state (off, init) =
- let lval = Evast.add_offset lval off in
+ let lval = Eva_ast.add_offset lval off in
apply_evast_initializer ~top_volatile kinstr lval init state
in
List.fold_left doinit state l
@@ -159,8 +159,8 @@ module Make
Very inefficient. *)
let initialize_var_zero_or_volatile kinstr vi state =
let loc = Cil_datatype.Location.unknown in
- let init = Evast.translate_init (Cil.makeZeroInit ~loc vi.vtype) in
- let lval = Evast.Build.var vi in
+ let init = Eva_ast.translate_init (Cil.makeZeroInit ~loc vi.vtype) in
+ let lval = Eva_ast.Build.var vi in
apply_evast_initializer ~top_volatile:true kinstr lval init state
(* ----------------------- Non Lib-entry mode ----------------------------- *)
@@ -169,7 +169,7 @@ module Make
let initialize_var_not_lib_entry kinstr ~local vi init state =
ignore (warn_unknown_size vi);
let typ = vi.vtype in
- let lval = Evast.Build.var vi in
+ let lval = Eva_ast.Build.var vi in
let volatile_everywhere = Cil.typeHasQualifier "volatile" typ in
let state =
if volatile_everywhere && padding_initialization ~local = `Initialized
@@ -205,8 +205,8 @@ module Make
not (Cil.typeHasQualifier "volatile" typ_lval)
&& not (Cil.is_mutable_or_initialized lval)
then
- let lval = Evast.translate_lval lval
- and exp = Evast.translate_exp exp
+ let lval = Eva_ast.translate_lval lval
+ and exp = Eva_ast.translate_exp exp
and source = fst exp.eloc in
apply_evast_single_initializer ~source kinstr state lval exp
else state
@@ -227,14 +227,14 @@ module Make
if Cil.typeHasQualifier "const" vi.vtype && not (vi.vstorage = Extern)
&& not (Cil.typeHasAttributeMemoryBlock Cil.frama_c_mutable vi.vtype)
then (* Fully const base. Ignore -lib-entry altogether. *)
- let init = Option.map Evast.translate_init init in
+ let init = Option.map Eva_ast.translate_init init in
initialize_var_not_lib_entry kinstr ~local:false vi init state
else
let unknown_size = warn_unknown_size vi in
let state =
if unknown_size then
(* the type is unknown, initialize everything to Top *)
- let lval = Evast.Build.var vi in
+ let lval = Eva_ast.Build.var vi in
let loc = lval_to_loc lval in
let v = Abstract_domain.Top in
Domain.initialize_variable lval loc ~initialized:true v state
@@ -333,7 +333,7 @@ module Make
initialize_var_lib_entry
else
fun ki vi init state ->
- let init = Option.map Evast.translate_init init in
+ let init = Option.map Eva_ast.translate_init init in
initialize_var_not_lib_entry ki ~local:false vi init state
in
initialize Kglobal vi init.init state
diff --git a/src/plugins/eva/engine/initialization.mli b/src/plugins/eva/engine/initialization.mli
index 1fdfe47cdf9..a5dadc07209 100644
--- a/src/plugins/eva/engine/initialization.mli
+++ b/src/plugins/eva/engine/initialization.mli
@@ -22,7 +22,7 @@
(** Creation of the initial state of abstract domain. *)
-open Evast
+open Eva_ast
open Lattice_bounds
module type S = sig
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 7a8e9a88d0e..1d8ec33fa9b 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
open Cil_types
-open Evast
+open Eva_ast
open Eva_automata
open Lattice_bounds
open Bottom.Operators
@@ -327,7 +327,7 @@ module Make_Dataflow
| None -> fun state -> [state]
| Some return_exp ->
let vi_ret = Option.get (Library_functions.get_retres_vi kf) in
- let return_lval = Evast.Build.var vi_ret in
+ let return_lval = Eva_ast.Build.var vi_ret in
let kstmt = Kstmt stmt in
fun state ->
let kind = Abstract_domain.Result kf in
@@ -387,9 +387,9 @@ module Make_Dataflow
| UnspecifiedSequence seq when Kernel.UnspecifiedAccess.get () ->
let seq = List.map (fun (stmt, modified, writes, reads, refs) ->
stmt,
- List.map Evast.translate_lval modified,
- List.map Evast.translate_lval writes,
- List.map Evast.translate_lval reads,
+ List.map Eva_ast.translate_lval modified,
+ List.map Eva_ast.translate_lval writes,
+ List.map Eva_ast.translate_lval reads,
refs) seq in
let check s =
Transfer.check_unspecified_sequence stmt s seq = `Value ()
diff --git a/src/plugins/eva/engine/subdivided_evaluation.ml b/src/plugins/eva/engine/subdivided_evaluation.ml
index c412c011b85..7e7623da15f 100644
--- a/src/plugins/eva/engine/subdivided_evaluation.ml
+++ b/src/plugins/eva/engine/subdivided_evaluation.ml
@@ -26,8 +26,8 @@ let dkey = Self.register_category "nonlin"
(* ----------------- Occurrences of lvalues in expressions ------------------ *)
-module LvalMap = Evast.Lval.Map
-module LvalSet = Evast.Lval.Set
+module LvalMap = Eva_ast.Lval.Map
+module LvalSet = Eva_ast.Lval.Set
(* An expression [e] is non-linear on [x] if [x] appears multiple times in [e].
When evaluating such an expression, a disjunction over the possible values of
@@ -87,7 +87,7 @@ let union expr depth map1 map2 =
If a lvalue is bound to itself, then it appears only once in [expr].
Otherwise, we say that the expression is non linear on this lvalue. *)
let gather_non_linear expr =
- let rec compute depth (expr : Evast.exp) =
+ let rec compute depth (expr : Eva_ast.exp) =
match expr.node with
| Lval ({ node = host, offset } as lv) ->
let d = succ depth in
@@ -117,7 +117,7 @@ let gather_non_linear expr =
(* Map from subexpressions to the list of their non-linear lvalues. *)
module ExpMap = struct
- include Evast.Exp.Map
+ include Eva_ast.Exp.Map
let add expr lv map =
try
let list = find expr map in
@@ -138,8 +138,8 @@ module DepthMap = struct
add depth expmap map
end
-let same lval (expr : Evast.exp) = match expr.node with
- | Lval lv -> Evast.Lval.equal lv lval
+let same lval (expr : Eva_ast.exp) = match expr.node with
+ | Lval lv -> Eva_ast.Lval.equal lv lval
| _ -> false
(* Converts a map from lvalues to expressions and depth into an association
@@ -155,12 +155,12 @@ let reverse_map map =
DepthMap.fold concat depthmap []
-module LvalList = Datatype.List (Evast.Lval)
-module NonLinear = Datatype.Pair (Evast.Exp) (LvalList)
+module LvalList = Datatype.List (Eva_ast.Lval)
+module NonLinear = Datatype.Pair (Eva_ast.Exp) (LvalList)
module NonLinears = Datatype.List (NonLinear)
module Non_linear_expressions =
- State_builder.Hashtbl (Evast.Exp.Hashtbl) (NonLinears)
+ State_builder.Hashtbl (Eva_ast.Exp.Hashtbl) (NonLinears)
(struct
let name = "Value.Subdivided_evaluation.Non_linear_expressions"
let size = 16
@@ -179,8 +179,8 @@ let compute_non_linear expr =
List.iter
(fun (e, lval) ->
Self.result ~current:true ~once:true ~dkey
- "non-linear '%a', lv '%a'" Evast.pp_exp e
- (Pretty_utils.pp_list ~sep:", " Evast.pp_lval) lval)
+ "non-linear '%a', lv '%a'" Eva_ast.pp_exp e
+ (Pretty_utils.pp_list ~sep:", " Eva_ast.pp_lval) lval)
list;
Non_linear_expressions.replace expr list;
list
@@ -655,7 +655,7 @@ module Make
Clear.clear_englobing_exprs valuation ~expr ~subexpr:lv_info.lv_expr
in
let cleared_valuation = Hypotheses.fold clear variables valuation in
- let eq_equal_subexpr = Evast.Exp.equal expr subexpr in
+ let eq_equal_subexpr = Eva_ast.Exp.equal expr subexpr in
(* Computes a disjunct from subvalues for [lvals]. *)
let compute subvalues =
(* Updates [variables] with their new [subvalues]. *)
@@ -705,7 +705,7 @@ module Make
(* Builds the information for an lvalue. *)
let get_info environment valuation lval =
- let lv_expr = Evast.Build.lval lval in
+ let lv_expr = Eva_ast.Build.lval lval in
(* Reevaluates the lvalue in the initial state, as its value could have
been reduced in the evaluation of the complete expression, and we cannot
omit the alarms for the removed values. *)
@@ -770,7 +770,7 @@ module Make
in
Self.result ~current:true ~once:true ~dkey
"subdividing on %a"
- (Pretty_utils.pp_list ~sep:", " Evast.pp_lval) lvals;
+ (Pretty_utils.pp_list ~sep:", " Eva_ast.pp_lval) lvals;
let subdivide =
subdivide_lvals environment valuation subdivnb lvals_info
in
@@ -846,7 +846,7 @@ module Make
(* Find locations on which it is interesting to proceed by case disjunction
to evaluate the expression: locations which are singletons (on which the
cvalue domain can reduce) and has an enumerable value. *)
- let rec get_influential_vars valuation (exp : Evast.exp) acc =
+ let rec get_influential_vars valuation (exp : Eva_ast.exp) acc =
match exp.node with
| Lval ({ node = host, off } as lval) ->
if Cil.typeHasQualifier "volatile" lval.typ then `Value acc
@@ -873,11 +873,11 @@ module Make
| CastE (_, exp) -> get_influential_vars valuation exp acc
| _ -> `Value acc
- and get_vars_host valuation (host : Evast.lhost) acc = match host with
+ and get_vars_host valuation (host : Eva_ast.lhost) acc = match host with
| Var _v -> `Value acc
| Mem e -> get_influential_vars valuation e acc
- and get_vars_offset valuation (offset : Evast.offset) acc = match offset with
+ and get_vars_offset valuation (offset : Eva_ast.offset) acc = match offset with
| NoOffset -> `Value acc
| Field (_, off) -> get_vars_offset valuation off acc
| Index (ind, off) ->
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index d4ffc39ca0a..3e0a22e0b0c 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -109,7 +109,7 @@ let substitution_visitor table =
| None -> vi
| Some vi' -> vi'
in
- { Evast.Rewrite.default with rewrite_varinfo }
+ { Eva_ast.Rewrite.default with rewrite_varinfo }
module Make (Abstract: Abstractions.S_with_evaluation) = struct
@@ -163,19 +163,19 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let evaluate_and_check ?valuation ~subdivnb state expr =
let res = Eval.evaluate ?valuation ~subdivnb state expr in
report_unreachability state res "the expression %a"
- Evast.pp_exp expr;
+ Eva_ast.pp_exp expr;
res
let lvaluate_and_check ?valuation ~subdivnb ~for_writing state lval =
let res = Eval.lvaluate ?valuation ~subdivnb ~for_writing state lval in
report_unreachability state res "the lvalue %a"
- Evast.pp_lval lval;
+ Eva_ast.pp_lval lval;
res
let copy_lvalue_and_check ?valuation ~subdivnb state lval =
let res = Eval.copy_lvalue ?valuation ~subdivnb state lval in
report_unreachability state res "the copy of %a"
- Evast.pp_lval lval;
+ Eva_ast.pp_lval lval;
res
(* ------------------------------------------------------------------------ *)
@@ -219,8 +219,8 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
if Cil.isStructOrUnionType typ
then
let truth = Location.assume_no_overlap ~partial:true loc right_loc in
- let lval' = Evast.to_cil_lval lval in
- let right_lval' = Evast.to_cil_lval right_lval in
+ let lval' = Eva_ast.to_cil_lval lval in
+ let right_lval' = Eva_ast.to_cil_lval right_lval in
let alarm () = Alarms.Overlap (lval', right_lval') in
Eval.interpret_truth ~alarm (loc, right_loc) truth
else `Value (loc, right_loc), Alarmset.none
@@ -355,7 +355,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
| `Top -> Precise_locs.loc_top
| `Value record -> get record.loc
in
- let expr_zone = Evast.zone_of_exp find_loc expr in
+ let expr_zone = Eva_ast.zone_of_exp find_loc expr in
let written_zone = inout.Inout_type.over_outputs_if_termination in
not (Locations.Zone.intersects expr_zone written_zone)
@@ -391,7 +391,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
| Assign pre_value -> `Value pre_value
| Copy (_lv, pre_value) -> pre_value.v
in
- let lval = Evast.Build.var argument.formal in
+ let lval = Eva_ast.Build.var argument.formal in
(* We use copy_lvalue instead of evaluate to get the escaping flag:
if a formal is escaping at the end of the called function, it may
have been freed, which is not detected as a write. We prevent the
@@ -432,7 +432,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
| None, Some vi_ret -> `Value (Domain.leave_scope kf_callee [vi_ret] state)
| Some _, None -> assert false
| Some lval, Some vi_ret ->
- let exp_ret_caller = Evast.Build.var_exp vi_ret in
+ let exp_ret_caller = Eva_ast.Build.var_exp vi_ret in
let+ state = assign_ret state (Kstmt stmt) lval exp_ret_caller in
Domain.leave_scope kf_callee [vi_ret] state
@@ -496,7 +496,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
then
Self.abort ~current:true
"Function argument %a has unknown size. Aborting"
- Evast.pp_exp expr;
+ Eva_ast.pp_exp expr;
if determinate && Cil.isArithmeticOrPointerType lv.typ
then assign_by_eval ~subdivnb state valuation expr
else assign_by_copy ~subdivnb state valuation lv loc
@@ -541,7 +541,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let v = flagged.v >>-: Value.replace_base substitution in
let flagged = { flagged with v } in
let lloc = Location.replace_base substitution loc.lloc in
- let lval = Evast.Rewrite.visit_lval visitor loc.lval in
+ let lval = Eva_ast.Rewrite.visit_lval visitor loc.lval in
let loc = { lval; lloc } in
Copy (loc, flagged)
@@ -551,7 +551,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let visitor = substitution_visitor tbl in
let base_substitution = recursion.base_substitution in
let replace_arg argument =
- let concrete = Evast.Rewrite.visit_exp visitor argument.concrete in
+ let concrete = Eva_ast.Rewrite.visit_exp visitor argument.concrete in
let avalue = replace_value visitor base_substitution argument.avalue in
{ argument with concrete; avalue }
in
@@ -610,7 +610,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
| `Value (valuation, _v) ->
show_expr (Eval.to_domain_valuation valuation) state fmt expr
in
- Format.fprintf fmt "%a : @[<h>%t@]" Evast.pp_exp expr pp
+ Format.fprintf fmt "%a : @[<h>%t@]" Eva_ast.pp_exp expr pp
in
let pp = Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@ " ~suf:"@]" pretty in
Self.result ~current:true
@@ -646,8 +646,8 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(Bottom.pretty Cvalue.V.pretty) fmt value
let pretty_arguments ~subdivnb state arguments =
- let is_scalar lval = Cil.isArithmeticOrPointerType lval.Evast.typ in
- let pretty fmt (expr : Evast.exp) =
+ let is_scalar lval = Cil.isArithmeticOrPointerType lval.Eva_ast.typ in
+ let pretty fmt (expr : Eva_ast.exp) =
match expr.node with
| Lval lval | StartOf lval when not (is_scalar lval) ->
show_offsm fmt subdivnb lval state
@@ -797,8 +797,8 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let list2, _ = eval_list valuation lvs2 in
let check acc (lval1, loc1) (lval2, loc2) =
let truth = Location.assume_no_overlap ~partial:false loc1 loc2 in
- let lval1' = Evast.to_cil_lval lval1
- and lval2' = Evast.to_cil_lval lval2 in
+ let lval1' = Eva_ast.to_cil_lval lval1
+ and lval2' = Eva_ast.to_cil_lval lval2 in
let alarm () = Alarms.Not_separated (lval1', lval2') in
let alarm = process_truth ~alarm truth in
Alarmset.combine alarm acc
@@ -817,7 +817,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let unauthorized_reads =
List.filter
(fun x -> List.for_all
- (fun y -> not (Evast.Lval.equal x y)) modified2)
+ (fun y -> not (Eva_ast.Lval.equal x y)) modified2)
writes1
in
let alarms1 = check_non_overlapping state unauthorized_reads reads2 in
@@ -850,7 +850,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let initialized = false in
let init_value = Abstract_domain.Top in
let initialize_volatile state varinfo =
- let lval = Evast.Build.var varinfo in
+ let lval = Eva_ast.Build.var varinfo in
let location = Location.eval_varinfo varinfo in
Domain.initialize_variable lval location ~initialized init_value state
in
diff --git a/src/plugins/eva/eval.ml b/src/plugins/eva/eval.ml
index c28c2053f8e..e1f63ce8320 100644
--- a/src/plugins/eva/eval.ml
+++ b/src/plugins/eva/eval.ml
@@ -22,8 +22,8 @@
open Cil_types
-type lval = Evast.lval
-type exp = Evast.exp
+type lval = Eva_ast.lval
+type exp = Eva_ast.exp
(** *)
@@ -155,7 +155,7 @@ let compute_englobing_subexpr ~subexpr ~expr =
[subexpr], apart [subexpr] itself, or [None] if [subexpr] does not appear
in [expr]. *)
let rec compute expr =
- if Evast.Exp.equal expr subexpr
+ if Eva_ast.Exp.equal expr subexpr
then Some []
else
let sublist = match expr.node with
@@ -181,9 +181,9 @@ let compute_englobing_subexpr ~subexpr ~expr =
Option.value ~default:[] (compute expr)
module Englobing =
- Datatype.Pair_with_collections (Evast.Exp) (Evast.Exp)
+ Datatype.Pair_with_collections (Eva_ast.Exp) (Eva_ast.Exp)
(struct let module_name = "Subexpressions" end)
-module SubExprs = Datatype.List (Evast.Exp)
+module SubExprs = Datatype.List (Eva_ast.Exp)
module EnglobingSubexpr =
State_builder.Hashtbl (Englobing.Hashtbl) (SubExprs)
diff --git a/src/plugins/eva/eval.mli b/src/plugins/eva/eval.mli
index 936ccdae4f8..1e40ede6cad 100644
--- a/src/plugins/eva/eval.mli
+++ b/src/plugins/eva/eval.mli
@@ -22,8 +22,8 @@
open Cil_types
-type lval = Evast.lval
-type exp = Evast.exp
+type lval = Eva_ast.lval
+type exp = Eva_ast.exp
(** Types and functions related to evaluations.
Heavily used by abstract values and domains, evaluation of expressions,
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index 5d6cdefbd6a..05999668da4 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -201,7 +201,7 @@ module Make (X: Analysis.S) = struct
GO_Bottom, true
let lval_to_offsetmap state lv =
- let lv = Evast.translate_lval lv in
+ let lv = Eva_ast.translate_lval lv in
let loc, alarms = X.eval_lval_to_loc state lv in
let ok = Alarmset.is_empty alarms in
let state = get_cvalue_or_top state in
@@ -249,7 +249,7 @@ module Make (X: Analysis.S) = struct
let lval_zone_ev =
let lv_to_zone state lv =
- let lv = Evast.translate_lval lv in
+ let lv = Eva_ast.translate_lval lv in
let loc, _alarms = X.eval_lval_to_loc state lv in
match loc with
| `Bottom -> Locations.Zone.bottom, false, false
@@ -286,7 +286,7 @@ module Make (X: Analysis.S) = struct
let exp_ev =
let eval_exp_and_warn state e =
- let e = Evast.translate_exp e in
+ let e = Eva_ast.translate_exp e in
let r = X.eval_expr state e in
fst r, Alarmset.is_empty (snd r), false
in
@@ -305,7 +305,7 @@ module Make (X: Analysis.S) = struct
let lval_ev =
let eval_and_warn state lval =
- let lval = Evast.translate_lval lval in
+ let lval = Eva_ast.translate_lval lval in
let r = X.copy_lvalue state lval in
let flagged_value = match fst r with
| `Bottom -> Eval.Flagged_Value.bottom
diff --git a/src/plugins/eva/gui/register_gui.ml b/src/plugins/eva/gui/register_gui.ml
index 3b1ea7d33c1..5935ba6a686 100644
--- a/src/plugins/eva/gui/register_gui.ml
+++ b/src/plugins/eva/gui/register_gui.ml
@@ -518,7 +518,7 @@ module Select (Eval: Eval) = struct
| Mem _, NoOffset when Cil.isFunctionType ty -> begin
(* Function pointers *)
(* get the list of functions in the values *)
- let e = Evast.(Build.lval (translate_lval lv)) in
+ let e = Eva_ast.(Build.lval (translate_lval lv)) in
let state =
match ki with
| Kglobal -> Eval.Analysis.get_global_state ()
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 533813a639d..62539f594e4 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -995,8 +995,8 @@ let forward_binop_by_type typ =
let forward_binop typ v1 op v2 =
match op with
- | Evast.Eq | Ne | Le | Lt | Ge | Gt ->
- let comp = Evast.conv_relation op in
+ | Eva_ast.Eq | Ne | Le | Lt | Ge | Gt ->
+ let comp = Eva_ast.conv_relation op in
if Cil.isPointerType typ || Cvalue_forward.are_comparable comp v1 v2
then forward_binop_by_type typ v1 op v2
else Cvalue.V.zero_or_one
@@ -1097,7 +1097,7 @@ let rec eval_term ~alarm_mode env t =
| BNot -> r.etype (* can only be used on an integer type *)
| LNot -> Cil.intType
in
- let op = Evast.translate_unop op in
+ let op = Eva_ast.translate_unop op in
let v = Cvalue_forward.forward_unop r.etype op r.eover in
let eover = v in
{ etype = typ';
@@ -1364,7 +1364,7 @@ and eval_binop ~alarm_mode env op t1 t2 =
let te1 = Cil.unrollType r1.etype in
check_logic_alarms ~alarm_mode te1 r1 op r2;
let typ_res = infer_binop_res_type op te1 in
- let op = Evast.translate_binop op in
+ let op = Eva_ast.translate_binop op in
let eover = forward_binop te1 r1.eover op r2.eover in
let default _r1 _r2 = under_from_over eover in
let add_untyped_op factor =
diff --git a/src/plugins/eva/partitioning/auto_loop_unroll.ml b/src/plugins/eva/partitioning/auto_loop_unroll.ml
index 09f63efa77a..de9277c7430 100644
--- a/src/plugins/eva/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/eva/partitioning/auto_loop_unroll.ml
@@ -142,7 +142,7 @@ module Graph = struct
expression must be zero or not-zero to exit the loop. *)
module Condition = struct
module Info = struct let module_name = "Condition" end
- include Datatype.Pair_with_collections (Evast.Exp) (Datatype.Bool) (Info)
+ include Datatype.Pair_with_collections (Eva_ast.Exp) (Datatype.Bool) (Info)
end
(* Returns a list of loop exit conditions. *)
@@ -170,7 +170,7 @@ let add_written_var vi effect =
let written_vars = Cil_datatype.Varinfo.Set.add vi effect.written_vars in
{ effect with written_vars }
-let is_frama_c_builtin (exp : Evast.exp) =
+let is_frama_c_builtin (exp : Eva_ast.exp) =
match exp.node with
| Lval { node = Var vi, NoOffset } ->
Ast_info.start_with_frama_c_builtin vi.vname
@@ -212,16 +212,16 @@ type var_status =
in the loop. *)
| Unsuitable (* Cannot be used for the heuristic. *)
-let is_integer lval = Cil.isIntegralType lval.Evast.typ
+let is_integer lval = Cil.isIntegralType lval.Eva_ast.typ
(* Computes the status of a lvalue for the heuristic, according to the
loop effects. Uses [eval_ptr] to compute the bases pointed by pointer
expressions. *)
-let classify eval_ptr loop_effect (lval : Evast.lval) =
+let classify eval_ptr loop_effect (lval : Eva_ast.lval) =
let is_written varinfo =
Cil_datatype.Varinfo.Set.mem varinfo loop_effect.written_vars
in
- let rec is_const_expr (expr : Evast.exp) =
+ let rec is_const_expr (expr : Eva_ast.exp) =
match expr.node with
| Lval lval -> classify_lval lval = Constant
| UnOp (_, e, _) | CastE (_, e) -> is_const_expr e
@@ -256,7 +256,7 @@ let classify eval_ptr loop_effect (lval : Evast.lval) =
classify_lval lval
(* Returns the list of all lvalues appearing in an expression. *)
-let rec get_lvalues (expr : Evast.exp) =
+let rec get_lvalues (expr : Eva_ast.exp) =
match expr.node with
| Lval lval -> [ lval ]
| UnOp (_, e, _) | CastE (_, e) -> get_lvalues e
@@ -283,25 +283,25 @@ let find_lonely_candidate eval_ptr loop_effect expr =
- to the value of an expression [expr], it applies [f expr acc];
- to a function call, or if [inner_loop] is true, it raises [exn]. *)
let transfer_assign lval exn f ~inner_loop acc transition =
- let is_lval = Evast.Lval.equal lval in
+ let is_lval = Eva_ast.Lval.equal lval in
match transition with
| Eva_automata.Assign (lv, expr, _loc)
when is_lval lv ->
if inner_loop then raise exn else f expr acc
| Init (vi, SingleInit (expr, _loc), _loc')
- when is_lval (Evast.Build.var vi) && not inner_loop ->
+ when is_lval (Eva_ast.Build.var vi) && not inner_loop ->
f expr acc
- | Init (vi, _, _) when is_lval (Evast.Build.var vi) -> raise exn
+ | Init (vi, _, _) when is_lval (Eva_ast.Build.var vi) -> raise exn
| Call (Some lv, _, _, _) when is_lval lv ->
raise exn
| _ -> acc
(* If in the [loop], [lval] is always assigned to the value of another
lvalue, returns this new lvalue. Otherwise, returns [lval]. *)
-let cross_equality loop (lval : Evast.lval) =
+let cross_equality loop (lval : Eva_ast.lval) =
(* If no such single equality can be found, return [lval] unchanged. *)
let exception No_equality in
- let find_lval (expr : Evast.exp) _x =
+ let find_lval (expr : Eva_ast.exp) _x =
match expr.node with
| Lval lval -> lval
| _ -> raise No_equality
@@ -310,7 +310,7 @@ let cross_equality loop (lval : Evast.lval) =
transfer_assign lval No_equality find_lval ~inner_loop lval transition
in
let join lv1 lv2 =
- if Evast.Lval.equal lv1 lv2 then lv1 else raise No_equality
+ if Eva_ast.Lval.equal lv1 lv2 then lv1 else raise No_equality
in
match Graph.compute ~backward:true loop transfer join lval with
| Some lval -> lval
@@ -342,9 +342,9 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Adds or subtracts the integer value of [expr] to the current increment
[acc.delta], according to [binop] which can be PlusA or MinusA.
Raises NoIncrement if [expr] is not a constant integer expression. *)
- let add_to_delta context binop acc (expr : Evast.exp) =
+ let add_to_delta context binop acc (expr : Eva_ast.exp) =
let typ = expr.typ in
- match Evast.fold_to_integer expr with
+ match Eva_ast.fold_to_integer expr with
| None -> raise NoIncrement
| Some i ->
let inject i = Val.inject_int typ i in
@@ -355,12 +355,12 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
of [expr]. Raises NoIncrement if this is not an increment of [lval]. *)
let rec delta_assign context lval expr acc =
(* Is the expression [e] equal to the lvalue [lval] (modulo cast)? *)
- let rec is_lval (e : Evast.exp) = match e.node with
- | Lval lv -> Evast.Lval.equal lval lv
+ let rec is_lval (e : Eva_ast.exp) = match e.node with
+ | Lval lv -> Eva_ast.Lval.equal lval lv
| CastE (typ, e) -> Cil.isIntegralType typ && is_lval e
| _ -> false
in
- match Evast.fold_to_integer expr with
+ match Eva_ast.fold_to_integer expr with
| Some i ->
let v = Val.inject_int expr.typ i in
{ value = `Value v; delta = `Bottom; }
@@ -448,7 +448,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* If [lval] is a varinfo out-of-scope at statement [stmt] of function [kf],
introduces it to the [state]. *)
- let enter_scope state kf stmt (lval : Evast.lval) =
+ let enter_scope state kf stmt (lval : Eva_ast.lval) =
match lval.node with
| Var vi, _ ->
let state =
@@ -469,7 +469,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* If [lval] is not in scope at [stmt], introduces it into [state] so that
the [condition] can be properly evaluated in [state]. *)
let state = enter_scope state kf stmt lval in
- let expr = Evast.Build.lval lval in
+ let expr = Eva_ast.Build.lval lval in
(* Evaluate the [condition] in the given [state]. *)
fst (Eval.evaluate state condition) >> fun (valuation, _v) ->
(* In the resulting valuation, replace the value of [expr] by [top_int]
diff --git a/src/plugins/eva/partitioning/partition.ml b/src/plugins/eva/partitioning/partition.ml
index 410cee78215..58fe60edd4e 100644
--- a/src/plugins/eva/partitioning/partition.ml
+++ b/src/plugins/eva/partitioning/partition.ml
@@ -28,9 +28,9 @@ open Bottom.Operators
type split_kind = Eva_annotations.split_kind = Static | Dynamic
[@@deriving eq,ord]
-(* Same as Eva_annotations.split_term but with Evast. *)
+(* Same as Eva_annotations.split_term but with Eva_ast. *)
type split_term =
- | Expression of Evast.Exp.t
+ | Expression of Eva_ast.Exp.t
| Predicate of (Cil_datatype.Predicate.t
[@compare Logic_utils.compare_predicate]
[@equal Datatype.from_compare])
@@ -40,7 +40,7 @@ let translate_split_term
(term : Eva_annotations.split_term) : split_term * Cil_types.location =
match term with
| Expression cil_exp ->
- Expression (Evast.translate_exp cil_exp), cil_exp.eloc
+ Expression (Eva_ast.translate_exp cil_exp), cil_exp.eloc
| Predicate pred ->
Predicate pred, pred.pred_loc
@@ -69,7 +69,7 @@ let new_monitor
module SplitTerm = Datatype.Make_with_collections (struct
include Datatype.Serializable_undefined
- module Exp = Evast.Exp
+ module Exp = Eva_ast.Exp
module Predicate = Cil_datatype.PredicateStructEq
type t = split_term [@@deriving eq, ord]
@@ -81,7 +81,7 @@ module SplitTerm = Datatype.Make_with_collections (struct
Stdlib.List.map (fun p -> Predicate p) Predicate.reprs
let pretty fmt = function
- | Expression e -> Evast.pp_exp fmt e
+ | Expression e -> Eva_ast.pp_exp fmt e
| Predicate p -> Printer.pp_predicate fmt p
let hash = function
@@ -99,7 +99,7 @@ module SplitMonitor = Datatype.Make_with_collections (
let name = "Partition.SplitMonitor"
let reprs = [{
- split_term = Expression (List.hd Evast.Exp.reprs);
+ split_term = Expression (List.hd Eva_ast.Exp.reprs);
split_kind = Static;
split_loc = Cil_datatype.Location.unknown;
split_limit = 0;
@@ -326,7 +326,7 @@ type action =
| Incr_loop
| Branch of branch * int
| Ration of rationing
- | Restrict of Evast.exp * Integer.t list
+ | Restrict of Eva_ast.exp * Integer.t list
| Split of split_monitor
| Merge of Eva_annotations.split_term
| Update_dynamic_splits
@@ -507,7 +507,7 @@ struct
let stamp_by_value = match Abstract.Val.get Main_values.CVal.key with
| None -> fun _ _ _ -> None
| Some get -> fun expr expected_values state ->
- let typ = expr.Evast.typ in
+ let typ = expr.Eva_ast.typ in
let make stamp i = stamp, i, Abstract.Val.inject_int typ i in
let expected_values = List.mapi make expected_values in
match fst (evaluate state expr) with
@@ -584,7 +584,7 @@ struct
| Enter_loop limit_kind -> fun k x ->
let limit = try match limit_kind with
| ExpLimit cil_exp ->
- let exp = Evast.translate_exp cil_exp
+ let exp = Eva_ast.translate_exp cil_exp
and source = fst cil_exp.eloc in
eval_exp_to_int ~source x exp
| IntLimit i -> i
diff --git a/src/plugins/eva/partitioning/partition.mli b/src/plugins/eva/partitioning/partition.mli
index c974eb98373..96be3ce67be 100644
--- a/src/plugins/eva/partitioning/partition.mli
+++ b/src/plugins/eva/partitioning/partition.mli
@@ -143,7 +143,7 @@ type action =
If the rationing has been created with [merge:true], all the states from
each flow receive the same stamp, but states from different flows receive
different stamps, until [limit] states have been tagged. *)
- | Restrict of Evast.exp * Integer.t list
+ | Restrict of Eva_ast.exp * Integer.t list
(** [Restrict (exp, list)] restricts the rationing according to the evaluation
of the expression [exp]:
– for each integer [i] in [list], states in which [exp] evaluates exactly
diff --git a/src/plugins/eva/partitioning/trace_partitioning.ml b/src/plugins/eva/partitioning/trace_partitioning.ml
index 99d87b42ce9..c9930c43e30 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.ml
+++ b/src/plugins/eva/partitioning/trace_partitioning.ml
@@ -173,7 +173,7 @@ struct
let empty_rationing = new_rationing ~limit:0 ~merge:false
- let split_return (flow : flow) (return_exp : Evast.exp option) : flow =
+ let split_return (flow : flow) (return_exp : Eva_ast.exp option) : flow =
let strategy = Split_return.kf_strategy kf in
if strategy = Split_strategy.FullSplit
then flow
diff --git a/src/plugins/eva/partitioning/trace_partitioning.mli b/src/plugins/eva/partitioning/trace_partitioning.mli
index 8b93fd07da9..e4683b370c3 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.mli
+++ b/src/plugins/eva/partitioning/trace_partitioning.mli
@@ -85,7 +85,7 @@ sig
val enter_loop : flow -> Cil_types.stmt -> flow
val leave_loop : flow -> Cil_types.stmt -> flow
val next_loop_iteration : flow -> Cil_types.stmt -> flow
- val split_return : flow -> Evast.exp option -> flow
+ val split_return : flow -> Eva_ast.exp option -> flow
(** After the analysis of a function call, recombines callee partitioning keys
with the caller key. *)
diff --git a/src/plugins/eva/utils/backward_formals.ml b/src/plugins/eva/utils/backward_formals.ml
index 8e98d6d87a7..985d86ee7fe 100644
--- a/src/plugins/eva/utils/backward_formals.ml
+++ b/src/plugins/eva/utils/backward_formals.ml
@@ -29,7 +29,7 @@ open Cil_types
be changed by the callee. *)
let safe_argument expr =
let exception Unsafe in
- let f (lv : Evast.lval) =
+ let f (lv : Eva_ast.lval) =
match lv.node with
| Var vi, NoOffset ->
if vi.vaddrof || Cil.typeHasQualifier "volatile" vi.vtype || vi.vglob
@@ -37,7 +37,7 @@ let safe_argument expr =
| _, _ -> raise Unsafe
in
try
- Evast.iter_lvals f expr;
+ Eva_ast.iter_lvals f expr;
true
with Unsafe -> false
diff --git a/src/plugins/eva/utils/backward_formals.mli b/src/plugins/eva/utils/backward_formals.mli
index 204928a5ff3..4f419e671e1 100644
--- a/src/plugins/eva/utils/backward_formals.mli
+++ b/src/plugins/eva/utils/backward_formals.mli
@@ -30,7 +30,7 @@ val written_formals: Cil_types.kernel_function -> Cil_datatype.Varinfo.Set.t
which may be internally overwritten by [kf] during its call. *)
-val safe_argument: Evast.exp -> bool
+val safe_argument: Eva_ast.exp -> bool
(** [safe_argument e] returns [true] if [e] (which is supposed to be
an actual parameter) is guaranteed to evaluate in the same way before and
after the call. *)
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index cb062b115b3..dbd77b93c4f 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -100,7 +100,7 @@ let get_subdivision stmt =
x
let pretty_actuals fmt actuals =
- let pp fmt (e,x) = Cvalue.V.pretty_typ (Some (e.Evast.typ)) fmt x in
+ let pp fmt (e,x) = Cvalue.V.pretty_typ (Some (e.Eva_ast.typ)) fmt x in
Pretty_utils.pp_flowlist pp fmt actuals
let pretty_current_cfunction_name fmt =
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index b8220fa51a5..bddb29411b4 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/src/plugins/eva/utils/eva_utils.mli
@@ -61,7 +61,7 @@ val emitter : Emitter.t
val get_slevel : Kernel_function.t -> Parameters.SlevelFunction.value
val get_subdivision: stmt -> int
val pretty_actuals :
- Format.formatter -> (Evast.exp * Cvalue.V.t) list -> unit
+ Format.formatter -> (Eva_ast.exp * Cvalue.V.t) list -> unit
val pretty_current_cfunction_name : Format.formatter -> unit
val warning_once_current : ('a, Format.formatter, unit) format -> 'a
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index b129c4b1749..48470709471 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -43,7 +43,7 @@ module Eval_annots = Eval_annots
module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
-module Evast = Evast
+module Eva_ast = Eva_ast
module Function_calls = Function_calls
module Logic_inout = Logic_inout
module Main_locations = Main_locations
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index 75108decc58..2db3103b845 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -47,7 +47,7 @@ module Eval_annots = Eval_annots
module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
-module Evast = Evast
+module Eva_ast = Eva_ast
module Function_calls = Function_calls
module Logic_inout = Logic_inout
module Main_locations = Main_locations
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index 348f0d15f24..cd45963fd53 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -577,13 +577,13 @@ let build_eval_lval_and_exp () =
eval_lval, eval_exp
let eval_lval lval req =
- let lval = Evast.translate_lval lval in
+ let lval = Eva_ast.translate_lval lval in
Value ((fst @@ build_eval_lval_and_exp ()) lval req)
let eval_var vi req = eval_lval (Cil.var vi) req
let eval_exp exp req =
- let exp = Evast.translate_exp exp in
+ let exp = Eva_ast.translate_exp exp in
Value ((snd @@ build_eval_lval_and_exp ()) exp req)
let eval_address' ?(for_writing=false) lval req =
@@ -596,7 +596,7 @@ let eval_address' ?(for_writing=false) lval req =
end : Lvaluation)
let eval_address ?(for_writing=false) lval req =
- let lval = Evast.translate_lval lval in
+ let lval = Eva_ast.translate_lval lval in
eval_address' ~for_writing lval req
let eval_callee exp req =
@@ -607,7 +607,7 @@ let eval_callee exp req =
invalid_arg "The callee must be an lvalue with no offset"
end;
let module M = Make () in
- let exp = Evast.translate_exp exp in
+ let exp = Eva_ast.translate_exp exp in
M.eval_callee exp req
let callee stmt =
@@ -732,19 +732,19 @@ let alarms : type a. a evaluation -> Alarms.t list =
let expr_deps expr request =
let lval_to_loc lv = eval_address' lv request |> as_precise_loc in
- Evast.zone_of_exp lval_to_loc (Evast.translate_exp expr)
+ Eva_ast.zone_of_exp lval_to_loc (Eva_ast.translate_exp expr)
let lval_deps lval request =
let lval_to_loc lv = eval_address' lv request |> as_precise_loc in
- Evast.zone_of_lval lval_to_loc (Evast.translate_lval lval)
+ Eva_ast.zone_of_lval lval_to_loc (Eva_ast.translate_lval lval)
let address_deps lval request =
let lval_to_loc lv = eval_address' lv request |> as_precise_loc in
- Evast.indirect_zone_of_lval lval_to_loc (Evast.translate_lval lval)
+ Eva_ast.indirect_zone_of_lval lval_to_loc (Eva_ast.translate_lval lval)
let expr_dependencies expr request =
let lval_to_loc lv = eval_address' lv request |> as_precise_loc in
- Evast.deps_of_exp lval_to_loc (Evast.translate_exp expr)
+ Eva_ast.deps_of_exp lval_to_loc (Eva_ast.translate_exp expr)
(* Taint *)
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index 3eb4898279e..427c8cc9d24 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -148,7 +148,7 @@ val by_callstack : request -> (Callstack.t * request) list
(** Returns the list of expressions which have been inferred to be equal to
the given expression by the Equality domain. *)
-val equality_class : Evast.exp -> request -> Evast.exp list result
+val equality_class : Eva_ast.exp -> request -> Eva_ast.exp list result
(** Returns the Cvalue state. Error cases are converted into the bottom or top
cvalue state accordingly. *)
diff --git a/src/plugins/eva/utils/unit_tests.ml b/src/plugins/eva/utils/unit_tests.ml
index 6ba8af66c79..aa6f0b876a2 100644
--- a/src/plugins/eva/utils/unit_tests.ml
+++ b/src/plugins/eva/utils/unit_tests.ml
@@ -99,8 +99,8 @@ module Sign = struct
let sign_res = Sign.forward_unop context typ unop sign in
let bug = not (Bottom.is_included is_included cval_res sign_res) in
report bug "%a %a = %a while %a %a = %a"
- Evast.pp_unop unop Cval.pretty cval (Bottom.pretty Cval.pretty) cval_res
- Evast.pp_unop unop Sign.pretty sign (Bottom.pretty Sign.pretty) sign_res
+ Eva_ast.pp_unop unop Cval.pretty cval (Bottom.pretty Cval.pretty) cval_res
+ Eva_ast.pp_unop unop Sign.pretty sign (Bottom.pretty Sign.pretty) sign_res
in
List.iter test values
@@ -111,9 +111,9 @@ module Sign = struct
let sign_res = Sign.forward_binop context typ binop sign1 sign2 in
let bug = not (Bottom.is_included is_included cval_res sign_res) in
report bug "%a %a %a = %a while %a %a %a = %a"
- Cval.pretty cval1 Evast.pp_binop binop Cval.pretty cval2
+ Cval.pretty cval1 Eva_ast.pp_binop binop Cval.pretty cval2
(Bottom.pretty Cval.pretty) cval_res
- Sign.pretty sign1 Evast.pp_binop binop Sign.pretty sign2
+ Sign.pretty sign1 Eva_ast.pp_binop binop Sign.pretty sign2
(Bottom.pretty Sign.pretty) sign_res
in
List.iter (fun x -> List.iter (test x) values) values
diff --git a/src/plugins/eva/utils/widen.ml b/src/plugins/eva/utils/widen.ml
index f0421ee6b84..0bb8593600e 100644
--- a/src/plugins/eva/utils/widen.ml
+++ b/src/plugins/eva/utils/widen.ml
@@ -437,7 +437,7 @@ module Parsed_Dynamic_Hints =
end)
let dynamic_bases_of_lval states e offset =
- let lv = Evast.mk_lval (Mem e, offset) in
+ let lv = Eva_ast.mk_lval (Mem e, offset) in
List.fold_left (fun acc' state ->
let location = Cvalue_queries.lval_to_loc state lv in
Locations.Location_Bits.fold_bases
@@ -510,8 +510,8 @@ let dynamic_widen_hints_hook _callstack stmt states =
List.fold_right (fun dhint (_acc_modified, acc_hints as acc) ->
let old_bases = dhint.bases in
let exp, offset = dhint.lv in
- let exp = Evast.translate_exp exp
- and offset = Evast.translate_offset offset in
+ let exp = Eva_ast.translate_exp exp
+ and offset = Eva_ast.translate_offset offset in
let bases = dynamic_bases_of_lval states exp offset in
let new_bases = Base.Hptset.diff bases old_bases in
if Base.Hptset.is_empty new_bases then
diff --git a/src/plugins/eva/values/abstract_value.ml b/src/plugins/eva/values/abstract_value.ml
index 8643761001a..4ea54f0223b 100644
--- a/src/plugins/eva/values/abstract_value.ml
+++ b/src/plugins/eva/values/abstract_value.ml
@@ -25,7 +25,7 @@
open Cil_types
open Eval
-type constant = Evast.constant
+type constant = Eva_ast.constant
(** Type for the truth value of an assertion in a value abstraction. The two
last tags should be used only for a product of value abstractions. *)
@@ -140,13 +140,13 @@ module type S = sig
(** [forward_unop typ unop v] evaluates the value [unop v], resulting from the
application of the unary operator [unop] to the value [v]. [typ] is the
type of [v]. *)
- val forward_unop : context enriched -> typ -> Evast.unop -> t -> t or_bottom
+ val forward_unop : context enriched -> typ -> Eva_ast.unop -> t -> t or_bottom
(** [forward_binop typ binop v1 v2] evaluates the value [v1 binop v2],
resulting from the application of the binary operator [binop] to the
values [v1] and [v2]. [typ] is the type of [v1]. *)
val forward_binop :
- context enriched -> typ -> Evast.binop -> t -> t -> t or_bottom
+ context enriched -> typ -> Eva_ast.binop -> t -> t -> t or_bottom
(** [rewrap_integer irange t] wraps around the abstract value [t] to fit the
integer range [irange], assuming 2's complement. Also used on absolute
@@ -183,14 +183,14 @@ module type S = sig
[input_type] is the type of [left], [resulting_type] the type of [result]. *)
val backward_binop :
context enriched -> input_type:typ -> resulting_type:typ ->
- Evast.binop -> left:t -> right:t -> result:t ->
+ Eva_ast.binop -> left:t -> right:t -> result:t ->
(t option * t option) or_bottom
(** Backward evaluation of the unary operation [unop arg = res];
tries to reduce the argument [arg] according to [res].
[typ_arg] is the type of [arg]. *)
val backward_unop :
- context enriched -> typ_arg:typ -> Evast.unop ->
+ context enriched -> typ_arg:typ -> Eva_ast.unop ->
arg:t -> res:t -> t option or_bottom
(** Backward evaluation of the cast of the value [src_val] of type [src_typ]
diff --git a/src/plugins/eva/values/cvalue_backward.ml b/src/plugins/eva/values/cvalue_backward.ml
index 7f63d24c51d..b4ba8bff308 100644
--- a/src/plugins/eva/values/cvalue_backward.ml
+++ b/src/plugins/eva/values/cvalue_backward.ml
@@ -260,7 +260,7 @@ let backward_lor ~v1 ~v2 ~res =
let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
let typ = Cil.unrollType typ_res in
match binop, typ with
- | Evast.PlusA, TInt _ -> backward_add_int typ ~res_value ~v1 ~v2 true
+ | Eva_ast.PlusA, TInt _ -> backward_add_int typ ~res_value ~v1 ~v2 true
| MinusA, TInt _ -> backward_add_int typ ~res_value ~v1 ~v2 false
| PlusA, TFloat (fk, _) -> backward_add_float (Fval.kind fk) ~res_value ~v1 ~v2 `Add
@@ -277,7 +277,7 @@ let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
(* comparison operators *)
| (Eq | Ne | Le | Lt | Ge | Gt), _ -> begin
- let binop = Evast.conv_relation binop in
+ let binop = Eva_ast.conv_relation binop in
match V.is_included V.singleton_zero res_value,
V.is_included V.singleton_one res_value with
| true, true ->
@@ -339,7 +339,7 @@ let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
let backward_unop ~typ_arg op ~arg:_ ~res =
match op with
- | Evast.LNot -> None (* handled by the generic mechanism *)
+ | Eva_ast.LNot -> None (* handled by the generic mechanism *)
| BNot -> None (* No real idea of what should be done *)
| Neg ->
try
diff --git a/src/plugins/eva/values/cvalue_backward.mli b/src/plugins/eva/values/cvalue_backward.mli
index a965e6f21e4..a6f35d23a96 100644
--- a/src/plugins/eva/values/cvalue_backward.mli
+++ b/src/plugins/eva/values/cvalue_backward.mli
@@ -34,13 +34,13 @@ val backward_binop:
typ_res:typ ->
res_value: V.t ->
typ_e1:typ ->
- V.t -> Evast.binop -> V.t -> (V.t * V.t) option
+ V.t -> Eva_ast.binop -> V.t -> (V.t * V.t) option
(** This function tries to reduce the argument value of an unary operation,
given its result. [typ_arg] is the type of [arg]. *)
val backward_unop:
typ_arg:typ ->
- Evast.unop ->
+ Eva_ast.unop ->
arg: V.t ->
res: V.t ->
V.t option
diff --git a/src/plugins/eva/values/cvalue_forward.ml b/src/plugins/eva/values/cvalue_forward.ml
index 2ff1bc2be22..4ecec4b55d3 100644
--- a/src/plugins/eva/values/cvalue_forward.ml
+++ b/src/plugins/eva/values/cvalue_forward.ml
@@ -377,7 +377,7 @@ let forward_minus_pp ~typ ev1 ev2 =
The function must behave as if it was acting on unbounded integers *)
let forward_binop_int ~typ ev1 op ev2 =
match op with
- | Evast.PlusPI -> V.add_untyped ~factor:(Bit_utils.osizeof_pointed typ) ev1 ev2
+ | Eva_ast.PlusPI -> V.add_untyped ~factor:(Bit_utils.osizeof_pointed typ) ev1 ev2
| MinusPI ->
let int_base = Int_Base.neg (Bit_utils.osizeof_pointed typ) in
V.add_untyped ~factor:int_base ev1 ev2
@@ -403,7 +403,7 @@ let forward_binop_int ~typ ev1 op ev2 =
~contains_zero: (V.contains_zero ev1 || V.contains_zero ev2)
~contains_non_zero:(V.contains_non_zero ev1 && V.contains_non_zero ev2)
| Eq | Ne | Ge | Le | Gt | Lt ->
- let op = Evast.conv_relation op in
+ let op = Eva_ast.conv_relation op in
let signed = Bit_utils.is_signed_int_enum_pointer (Cil.unrollType typ) in
V.inject_comp_result (V.forward_comp_int ~signed op ev1 ev2)
@@ -416,12 +416,12 @@ let forward_binop_float fkind ev1 op ev2 =
V.inject_float (f fkind f1 f2)
in
match op with
- | Evast.PlusA -> binary_float_floats "+." Fval.add
+ | Eva_ast.PlusA -> binary_float_floats "+." Fval.add
| MinusA -> binary_float_floats "-." Fval.sub
| Mult -> binary_float_floats "*." Fval.mul
| Div -> binary_float_floats "/." Fval.div
| Eq | Ne | Lt | Gt | Le | Ge ->
- let op = Evast.conv_relation op in
+ let op = Eva_ast.conv_relation op in
V.inject_comp_result (Fval.forward_comp op f1 f2)
| _ -> assert false
@@ -448,7 +448,7 @@ let forward_uneg v t =
let forward_unop typ op value =
match op with
- | Evast.Neg -> forward_uneg value typ
+ | Eva_ast.Neg -> forward_uneg value typ
| BNot -> begin
match Cil.unrollType typ with
| TInt (ik, _) | TEnum ({ekind=ik}, _) ->
diff --git a/src/plugins/eva/values/cvalue_forward.mli b/src/plugins/eva/values/cvalue_forward.mli
index ddc38eeff74..a68b0078467 100644
--- a/src/plugins/eva/values/cvalue_forward.mli
+++ b/src/plugins/eva/values/cvalue_forward.mli
@@ -34,11 +34,11 @@ val assume_not_nan: assume_finite:bool -> fkind -> V.t -> V.t truth
val assume_pointer: V.t -> V.t truth
val assume_comparable: pointer_comparison -> V.t -> V.t -> (V.t * V.t) truth
-val forward_binop_int: typ: typ -> V.t -> Evast.binop -> V.t -> V.t
+val forward_binop_int: typ: typ -> V.t -> Eva_ast.binop -> V.t -> V.t
-val forward_binop_float: Fval.kind -> V.t -> Evast.binop -> V.t -> V.t
+val forward_binop_float: Fval.kind -> V.t -> Eva_ast.binop -> V.t -> V.t
-val forward_unop: typ -> Evast.unop -> V.t -> V.t
+val forward_unop: typ -> Eva_ast.unop -> V.t -> V.t
val rewrap_integer: Eval_typ.integer_range -> V.t -> V.t
diff --git a/src/plugins/eva/values/main_values.ml b/src/plugins/eva/values/main_values.ml
index 313fad45edf..f6469c32437 100644
--- a/src/plugins/eva/values/main_values.ml
+++ b/src/plugins/eva/values/main_values.ml
@@ -49,7 +49,7 @@ module CVal = struct
let assume_comparable = Cvalue_forward.assume_comparable
let constant _context _exp = function
- | Evast.CTopInt _ -> Cvalue.V.top_int
+ | Eva_ast.CTopInt _ -> Cvalue.V.top_int
| CInt64 (i,_k,_s) -> Cvalue.V.inject_int i
| CChr c -> Cvalue.V.inject_int (Cil.charConstToInt c)
| CString base ->
diff --git a/src/plugins/eva/values/offsm_value.ml b/src/plugins/eva/values/offsm_value.ml
index 1012e531197..fd657c92ee4 100644
--- a/src/plugins/eva/values/offsm_value.ml
+++ b/src/plugins/eva/values/offsm_value.ml
@@ -419,7 +419,7 @@ module Offsm
let constant _context e _c =
if store_redundant then
- match Evast.fold_to_integer e with
+ match Eva_ast.fold_to_integer e with
| Some i -> inject_int e.typ i
| None -> Top
else Top
@@ -433,7 +433,7 @@ module Offsm
let forward_unop _context _typ op o =
let o' = match o, op with
- | Top, _ | _, (Evast.Neg | LNot) -> Top
+ | Top, _ | _, (Eva_ast.Neg | LNot) -> Top
| O o, BNot -> O (bnot o)
in
`Value o'
@@ -441,7 +441,7 @@ module Offsm
let forward_binop _context _typ op o1 o2 =
let o' =
match o1, o2, op with
- | O _o1, O _o2, (Evast.Shiftlt | Shiftrt) ->
+ | O _o1, O _o2, (Eva_ast.Shiftlt | Shiftrt) ->
(* It is inconvenient to handle shift here, because we need a
constant for o2 *)
Top
@@ -523,7 +523,7 @@ let () = Abstractions.Hooks.register @@ fun (module Abstraction) ->
let forward_unop context typ op t =
match op with
- | Evast.BNot ->
+ | Eva_ast.BNot ->
let t = strengthen_offsm typ t in
let* t = forward_unop context typ op t in
strengthen_v typ t
@@ -531,7 +531,7 @@ let () = Abstractions.Hooks.register @@ fun (module Abstraction) ->
let forward_binop context typ op l r =
match op with
- | Evast.BAnd | BOr | BXor ->
+ | Eva_ast.BAnd | BOr | BXor ->
let l = strengthen_offsm typ l
and r = strengthen_offsm typ r in
let* t = forward_binop context typ op l r in
diff --git a/src/plugins/eva/values/sign_value.ml b/src/plugins/eva/values/sign_value.ml
index aded4e6650c..04ab54aa224 100644
--- a/src/plugins/eva/values/sign_value.ml
+++ b/src/plugins/eva/values/sign_value.ml
@@ -103,7 +103,7 @@ let inject_int _ i =
else zero
let constant _context _expr = function
- | Evast.CInt64 (i, _, _) -> inject_int () i
+ | Eva_ast.CInt64 (i, _, _) -> inject_int () i
| _ -> top
(* Extracting function pointers from an abstraction. Not implemented
@@ -149,7 +149,7 @@ let logical_not v = { pos = v.zero; neg = false; zero = v.pos || v.neg }
let forward_unop _context typ op v =
match op with
- | Evast.Neg -> `Value (neg_unop v)
+ | Eva_ast.Neg -> `Value (neg_unop v)
| BNot -> `Value (bitwise_not typ v)
| LNot -> `Value (logical_not v)
@@ -228,7 +228,7 @@ let logical_or v1 v2 =
let forward_binop _context _typ op v1 v2 =
match op with
- | Evast.PlusA -> `Value (plus v1 v2)
+ | Eva_ast.PlusA -> `Value (plus v1 v2)
| MinusA -> `Value (plus v1 (neg_unop v2))
| Mult -> `Value (mul v1 v2)
| Div -> if equal zero v2 then `Bottom else `Value (div v1 v2)
@@ -317,8 +317,8 @@ let backward_comp_right op ~left ~right =
for comparison operators. *)
let backward_binop _ctx ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
match op with
- | Evast.Ne | Eq | Le | Lt | Ge | Gt ->
- let op = Evast.conv_relation op in
+ | Eva_ast.Ne | Eq | Le | Lt | Ge | Gt ->
+ let op = Eva_ast.conv_relation op in
if equal zero result then
(* The comparison is false, as it always evaluate to false. Reduce by the
fact that the inverse comparison is true. *)
--
GitLab