diff --git a/Makefile b/Makefile
index fc57451b0098a4e6a322ba70a38a37da3ba5a4a5..228828bb6112600704996a2ce46dea573c3d90eb 100644
--- a/Makefile
+++ b/Makefile
@@ -925,6 +925,19 @@ PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(VALUE_TYPES))
$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
+#########
+# Reduc #
+#########
+PLUGIN_ENABLE:=$(ENABLE_REDUC)
+PLUGIN_DYNAMIC:=$(DYNAMIC_REDUC)
+PLUGIN_NAME:=Reduc
+PLUGIN_DISTRIBUTED:=yes
+PLUGIN_DIR:=src/plugins/reduc
+PLUGIN_CMO:=reduc_options misc value2acsl collect hyp register
+PLUGIN_DEPENDENCIES:=Eva
+
+$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
+
##################
# Occurrence #
##################
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index c62c5c099a76660fec06a6564f5e8d89e710add8..1ba479e563c1051806697fb923ff0dd0f39c15d5 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1119,6 +1119,18 @@ src/plugins/qed/pretty.ml: CEA_WP
src/plugins/qed/pretty.mli: CEA_WP
src/plugins/qed/term.ml: CEA_WP
src/plugins/qed/term.mli: CEA_WP
+src/plugins/reduc/Reduc.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/collect.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/collect.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/hyp.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/hyp.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/misc.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/misc.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/reduc_options.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/reduc_options.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/value2acsl.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/value2acsl.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/.gitignore: .ignore
src/plugins/report/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/Report.mli: CEA_LGPL_OR_PROPRIETARY
@@ -1579,6 +1591,8 @@ src/plugins/wp/Matrix.ml: CEA_WP
src/plugins/wp/Matrix.mli: CEA_WP
src/plugins/wp/MemoryContext.ml: CEA_WP
src/plugins/wp/MemoryContext.mli: CEA_WP
+src/plugins/wp/MemDebug.ml: CEA_WP
+src/plugins/wp/MemDebug.mli: CEA_WP
src/plugins/wp/MemEmpty.ml: CEA_WP
src/plugins/wp/MemEmpty.mli: CEA_WP
src/plugins/wp/MemLoader.ml: CEA_WP
@@ -1589,6 +1603,8 @@ src/plugins/wp/MemRegion.ml: CEA_WP
src/plugins/wp/MemRegion.mli: CEA_WP
src/plugins/wp/MemTyped.ml: CEA_WP
src/plugins/wp/MemTyped.mli: CEA_WP
+src/plugins/wp/MemVal.ml: CEA_WP
+src/plugins/wp/MemVal.mli: CEA_WP
src/plugins/wp/MemVar.ml: CEA_WP
src/plugins/wp/MemVar.mli: CEA_WP
src/plugins/wp/MemZeroAlias.ml: CEA_WP
diff --git a/src/plugins/reduc/Reduc.mli b/src/plugins/reduc/Reduc.mli
new file mode 100644
index 0000000000000000000000000000000000000000..cce51dc83ef23f10bb7ed95d5a93dfc632b91896
--- /dev/null
+++ b/src/plugins/reduc/Reduc.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
diff --git a/src/plugins/reduc/collect.ml b/src/plugins/reduc/collect.ml
new file mode 100644
index 0000000000000000000000000000000000000000..427d97ecb56435975f7d248801908446f790ac7a
--- /dev/null
+++ b/src/plugins/reduc/collect.ml
@@ -0,0 +1,206 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Cil_datatype
+
+module Options = Reduc_options
+
+exception Alarm_reached
+
+let dkey = Options.register_category "collect"
+let debug = Options.debug ~dkey
+
+type 'a alarm_component = Emitter.t ->
+ kernel_function ->
+ stmt ->
+ rank:int -> Alarms.alarm -> code_annotation -> 'a -> 'a
+
+type varh = VarAll
+type annoth = AnnotAll | AnnotInout
+
+type env = {
+ rel_varh: varh;
+ rel_annoth: annoth;
+ rel_stmts: Stmt.Set.t;
+ rel_vars: LvalStructEq.Set.t Stmt.Map.t;
+}
+
+let empty_env varh annoth = {
+ rel_varh = varh;
+ rel_annoth = annoth;
+ rel_stmts = Stmt.Set.empty;
+ rel_vars = Stmt.Map.empty;
+}
+
+let env_with_stmt env stmt =
+ { env with rel_stmts = Stmt.Set.add stmt env.rel_stmts }
+
+let env_with_stmt_vars env stmt lvs =
+ let vars =
+ try
+ Stmt.Map.find stmt env.rel_vars
+ with Not_found -> LvalStructEq.Set.empty in
+ let new_vars = LvalStructEq.Set.(union vars (of_list lvs)) in
+ { env with rel_vars = Stmt.Map.add stmt new_vars env.rel_vars }
+
+(* ************************************************************************ *)
+(** Alarms to relevant locations *)
+(* ************************************************************************ *)
+
+class stmts_vis
+ (alarm_stmt : stmt)
+ (env: env ref) = object(_)
+ inherit Cil.nopCilVisitor
+
+ method! vstmt stmt =
+ env := env_with_stmt !env stmt;
+ if Stmt.equal stmt alarm_stmt then begin
+ raise Alarm_reached
+ end;
+ Cil.DoChildren
+end
+
+let rec collect_off typ =
+ match typ with
+ | TInt _ | TFloat _ -> [ NoOffset ]
+ | TComp ({cfields = Some flds}, _, _) ->
+ List.fold_left collect_fields [] flds
+ | TArray (arrtyp, e_opt, _, _) ->
+ debug "Array of length %a" (Pretty_utils.pp_opt Printer.pp_exp) e_opt;
+ begin try collect_array arrtyp [] (Cil.lenOfArray64 e_opt)
+ with Cil.LenOfArray -> [] end
+ | TVoid _ | TFun _ | TPtr _ | TEnum _ | TNamed _ | TBuiltin_va_list _
+ | TComp ({cfields = None}, _, _)-> []
+
+and collect_fields acc fld =
+ let offs = collect_off fld.ftype in
+ List.map (fun off -> Field (fld, off)) offs @ acc
+
+and collect_array typ acc = function
+ | x when Integer.is_zero x -> acc
+ | x ->
+ let offs = collect_off typ in
+ let exp = Cil.kinteger64 ~loc:Location.unknown x in
+ let acc' = acc @ List.map (fun off -> Index(exp ,off)) offs in
+ collect_array typ acc' (Integer.add x Integer.minus_one)
+
+let collect_varinfo acc x =
+ let offs = collect_off x.vtype in
+ List.map (fun off -> (Var x, off)) offs @ acc
+
+class inout_vis
+ (alarm_stmt : stmt)
+ (kf : Kernel_function.t)
+ (env : env ref) = object(self)
+ inherit stmts_vis alarm_stmt env as super
+
+ val mutable vars = []
+
+ method !vfunc _ =
+ vars <- Kernel_function.((get_locals kf) @ (get_formals kf));
+ Cil.DoChildren
+
+ method private is_first_stmt stmt =
+ try Stmt.equal stmt (Kernel_function.find_first_stmt kf)
+ with Kernel_function.No_Statement -> assert false
+
+ method !vstmt stmt =
+ let out = !Db.Outputs.statement stmt in
+ let filter_out vi =
+ let open Locations in
+ let zone = enumerate_bits (loc_of_varinfo vi) in
+ Zone.intersects out zone
+ in
+ let effect =
+ if self#is_first_stmt stmt then vars
+ else List.filter filter_out vars
+ in
+ let vars = List.fold_left collect_varinfo [] effect in
+ env := env_with_stmt_vars !env stmt vars;
+ super#vstmt stmt
+end
+
+let get_relevant_stmts kf stmt env =
+ let do_visit ref_env = match !ref_env.rel_annoth with
+ | AnnotAll -> Cil.visitCilFunction (new stmts_vis stmt ref_env)
+ | AnnotInout ->
+ Cil.visitCilFunction (new inout_vis stmt kf ref_env :> Cil.cilVisitor)
+ in
+ let renv = ref env in
+ try
+ let fundec = Kernel_function.get_definition kf in
+ ignore (do_visit renv fundec);
+ !renv
+ with Alarm_reached ->
+ !renv
+
+let get_relevant _emit kf stmt ~rank:_ _a _annot env =
+ get_relevant_stmts kf stmt env
+
+let should_annotate_stmt env stmt =
+ Stmt.Set.mem stmt env.rel_stmts
+
+(* ************************************************************************ *)
+(** Relevant locations to relevant variables *)
+(* ************************************************************************ *)
+
+class relevant_stmt_vars_visitor
+ (vars: LvalStructEq.Set.t ref) = object(_)
+ inherit Cil.nopCilVisitor
+
+ method! vstmt stmt =
+ match stmt.skind with
+ | Goto _ | UnspecifiedSequence _ -> Cil.SkipChildren
+ | _ -> Cil.DoChildren
+
+ method! vblock _ = Cil.SkipChildren
+
+ method !vexpr e =
+ begin match e.enode with
+ | Lval lv | AddrOf lv | StartOf lv ->
+ vars := LvalStructEq.Set.add lv !vars
+ | _ -> ()
+ end;
+ Cil.DoChildren
+end
+
+let get_relevant_all_vars_stmt kf stmt =
+ let do_visit ref_vars =
+ Cil.visitCilStmt (new relevant_stmt_vars_visitor ref_vars)
+ in
+ let ref_vars = ref LvalStructEq.Set.empty in
+ ignore (do_visit ref_vars stmt);
+ let locals = Kernel_function.get_locals kf in
+ let formals = Kernel_function.get_formals kf in
+ let vars = List.map Cil.var (locals @ formals) in
+ vars @ LvalStructEq.Set.elements !ref_vars
+
+let get_relevant_inout_vars_stmt env stmt =
+ try
+ let vars = Stmt.Map.find stmt env.rel_vars in
+ LvalStructEq.Set.elements vars
+ with Not_found -> assert false
+
+let get_relevant_vars_stmt env kf stmt = match env.rel_annoth with
+ | AnnotAll -> get_relevant_all_vars_stmt kf stmt
+ | AnnotInout -> get_relevant_inout_vars_stmt env stmt
diff --git a/src/plugins/reduc/collect.mli b/src/plugins/reduc/collect.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bfbf024ec5622880024e6bd13d4f1f6021953aab
--- /dev/null
+++ b/src/plugins/reduc/collect.mli
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+type 'a alarm_component = Emitter.t ->
+ kernel_function ->
+ stmt ->
+ rank:int -> Alarms.alarm -> code_annotation -> 'a -> 'a
+
+type env
+
+type varh = VarAll
+type annoth = AnnotAll | AnnotInout
+
+val empty_env: varh -> annoth -> env
+
+val get_relevant: env alarm_component (* Set(loc) * Set(exp) ? *)
+
+val should_annotate_stmt: env -> stmt -> bool
+val get_relevant_vars_stmt: env -> kernel_function -> stmt -> lval list
diff --git a/src/plugins/reduc/hyp.ml b/src/plugins/reduc/hyp.ml
new file mode 100644
index 0000000000000000000000000000000000000000..fc4fabf2763c7db2b26efafaf8ff26481de7d763
--- /dev/null
+++ b/src/plugins/reduc/hyp.ml
@@ -0,0 +1,54 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+let pred_opt_from_expr_state state e =
+ try
+ Value2acsl.lval_to_predicate state e
+ with
+ | Cvalue.V.Not_based_on_null ->
+ Misc.not_implemented ~what:"Value not based on null";
+ None
+ | Misc.Not_implemented what ->
+ Misc.not_implemented ~what;
+ None
+
+class hypotheses_visitor (env: Collect.env) = object(self)
+ inherit Visitor.generic_frama_c_visitor (Visitor_behavior.inplace ())
+
+ method! vstmt_aux stmt =
+ let kf = Option.get (self#current_kf) in
+ let state = Db.Value.get_stmt_state stmt in
+ if Collect.should_annotate_stmt env stmt then begin
+ let vars = Collect.get_relevant_vars_stmt env kf stmt in
+ List.iter
+ (fun e ->
+ let p_opt = pred_opt_from_expr_state state e in
+ Option.iter (Misc.assert_and_validate ~kf stmt) p_opt)
+ vars
+ end;
+ Cil.DoChildren
+end
+
+
+let generate_hypotheses env =
+ let visitor = new hypotheses_visitor env in
+ Cil.visitCilFileSameGlobals (visitor :> Cil.cilVisitor) (Ast.get ())
diff --git a/src/plugins/reduc/hyp.mli b/src/plugins/reduc/hyp.mli
new file mode 100644
index 0000000000000000000000000000000000000000..7f19f530cd30f6008af7aad8aa08992adf70b246
--- /dev/null
+++ b/src/plugins/reduc/hyp.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+val generate_hypotheses: Collect.env -> unit
diff --git a/src/plugins/reduc/misc.ml b/src/plugins/reduc/misc.ml
new file mode 100644
index 0000000000000000000000000000000000000000..1e5fda8a19eb7cb3465560d5b045e573068d7f4e
--- /dev/null
+++ b/src/plugins/reduc/misc.ml
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+module Options = Reduc_options
+
+
+exception Not_implemented of string
+
+let not_implemented ~what =
+ Options.warning "Not implemented: `%s'. Ignoring." what
+
+
+let emitter =
+ Emitter.create
+ "Reduc"
+ [ Emitter.Code_annot; Emitter.Property_status ]
+ ~correctness:[]
+ ~tuning:[]
+
+(* ******************************************************)
+(* Annotations and function contracts helpers *)
+(* ******************************************************)
+let validate_ip ip =
+ Property_status.emit emitter ~hyps:[] ip Property_status.True
+
+let assert_and_validate ~kf stmt p =
+ let p = { tp_kind = Assert ; tp_statement = p } in
+ let annot = Logic_const.new_code_annotation (AAssert([], p)) in
+ Annotations.add_code_annot emitter ~kf stmt annot ;
+ List.iter
+ validate_ip
+ (Property.ip_of_code_annot kf stmt annot)
diff --git a/src/plugins/reduc/misc.mli b/src/plugins/reduc/misc.mli
new file mode 100644
index 0000000000000000000000000000000000000000..6bf9d91a6d7d8c3c4f18dd939411df059c24d1b4
--- /dev/null
+++ b/src/plugins/reduc/misc.mli
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+exception Not_implemented of string
+val not_implemented: what:string -> unit
+
+(* [emitter] of the reduc plugin. *)
+val emitter: Emitter.t
+
+(* ******************************************************)
+(* Annotations and function contracts helpers *)
+(* ******************************************************)
+val assert_and_validate: kf:Kernel_function.t -> stmt -> predicate -> unit
diff --git a/src/plugins/reduc/reduc_options.ml b/src/plugins/reduc/reduc_options.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3a5910a067fcc4f274525d17f72f889457fc8db4
--- /dev/null
+++ b/src/plugins/reduc/reduc_options.ml
@@ -0,0 +1,54 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include Plugin.Register
+ (struct
+ let name = "Reduction"
+ let shortname = "reduc"
+ let help = "Generate ACSL annotations from Value Analysis informations"
+ end)
+
+module Reduc =
+ Bool
+ (struct
+ let option_name = "-reduc"
+ let help = "Use reduc"
+ let default = false
+ end)
+
+module GenAnnot =
+ String
+ (struct
+ let option_name = "-reduc-gen-annot"
+ let arg_name = "gen-annot-heuristic"
+ let help = "Heuristic to generate annotations from Value"
+ let default = "inout"
+ end)
+
+module GenVars =
+ String
+ (struct
+ let option_name = "-reduc-gen-vars"
+ let arg_name = "gen-vars-heuristic"
+ let help = "Heuristic to generate annotations for variables"
+ let default = "all"
+ end)
diff --git a/src/plugins/reduc/reduc_options.mli b/src/plugins/reduc/reduc_options.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5eeb81c7c625e0d4e0b958149aad6ed6f64b62e8
--- /dev/null
+++ b/src/plugins/reduc/reduc_options.mli
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include Plugin.General_services
+
+module Reduc: Parameter_sig.Bool
+
+module GenAnnot: Parameter_sig.String
+module GenVars: Parameter_sig.String
diff --git a/src/plugins/reduc/register.ml b/src/plugins/reduc/register.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0274d1458579037b452eaf4e8053ecb67610aa81
--- /dev/null
+++ b/src/plugins/reduc/register.ml
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module Options = Reduc_options
+
+let command_line () =
+ let varh = match Options.GenVars.get () with
+ | "all" -> Collect.VarAll
+ | _ -> Options.fatal "Not a valid variable heuristic" in
+ let annoth = match Options.GenAnnot.get () with
+ | "all" -> Collect.AnnotAll
+ | "inout" -> Collect.AnnotInout
+ | _ -> Options.fatal "Not a valid annotation heuristic"
+ in
+ varh, annoth
+
+let main () =
+ if (Options.Reduc.get ()) then begin
+ let varh, annoth = command_line () in
+ let env = Alarms.fold Collect.get_relevant (Collect.empty_env varh annoth) in
+ Hyp.generate_hypotheses env;
+ ()
+ end
+
+let () = Db.Main.extend main
diff --git a/src/plugins/reduc/value2acsl.ml b/src/plugins/reduc/value2acsl.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c91d1ba6992418ffebcea1371b2b587aa9d5ea36
--- /dev/null
+++ b/src/plugins/reduc/value2acsl.ml
@@ -0,0 +1,179 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_datatype
+open Cil_types
+
+open Misc
+
+module AI = Abstract_interp
+
+module Options = Reduc_options
+
+let not_yet ~what =
+ Options.warning "Not yet: %s" what
+
+(* [int_to_predicate ~loc lop te i] create a predicate where [te] [lop] [i]. *)
+let int_to_predicate ~loc ~lop te (i: Integer.t) =
+ let ti = Logic_const.tint i in
+ Logic_const.prel ~loc (lop, te, ti)
+
+(* [float_to_predicate ~loc lop te f] create a predicate where [te] [lop] [f]. *)
+let float_to_predicate ~loc ~lop t f =
+ let tf = Logic_const.treal ~loc f in
+ Logic_const.prel ~loc (lop, t, tf)
+
+(* [interval_to_predicate_opt ~loc te min max] may create an interval
+ predicate where [min] <= [te] <= [max]. *)
+let interval_to_predicate_opt ~loc te min max =
+ let min_predicate =
+ int_to_predicate ~loc ~lop:Rge te
+ and max_predicate =
+ int_to_predicate ~loc ~lop:Rle te
+ in
+ Extlib.merge_opt
+ (fun _ pmin pmax -> Logic_const.pand ~loc (pmin, pmax))
+ ()
+ (Option.map min_predicate min)
+ (Option.map max_predicate max)
+
+(* [congruence_to_predicate_opt ~loc te rem modulo] may create a congruence
+ predicate where [te] mod [modulo] equals [rem] *)
+let congruence_to_predicate_opt ~loc te rem modulo =
+ if Integer.(equal modulo one) then None
+ else
+ let tmodulo = Logic_const.tint ~loc modulo in
+ let tbinop = TBinOp(Mod, te, tmodulo) in
+ (* since 0 <= rem < mod *)
+ let tmodop = Logic_const.term ~loc tbinop (Linteger) in
+ let p = int_to_predicate ~loc ~lop:Req tmodop rem in
+ Some p
+
+let fval_to_predicate ~loc t f =
+ match Ival.min_and_max_float f with
+ | None, false -> assert false
+ | _, true -> Logic_const.pfalse (* todo *)
+ | Some (fmn, fmx), _ ->
+ let mn = Fval.F.to_float fmn in
+ let mx = Fval.F.to_float fmx in
+ let pmn = float_to_predicate ~loc ~lop:Rge t mn in
+ let pmx = float_to_predicate ~loc ~lop:Rle t mx in
+ Logic_const.pand ~loc (pmn, pmx)
+
+(* [ival_to_predicate_opt ~loc t ival] may create a predicate from different
+ domains contained in [ival]. *)
+let ival_to_predicate_opt ~loc t ival =
+ if Ival.is_float ival
+ then Some (fval_to_predicate ~loc t ival)
+ else
+ match Ival.project_small_set ival with
+ | Some is ->
+ let ps = List.map (int_to_predicate ~loc ~lop:Req t) is in
+ let pors = Logic_const.pors ps in
+ Some pors
+ | None ->
+ match Ival.min_max_r_mod ival with
+ | (None, None, _, modulo) when AI.Int.is_one modulo ->(*Top*) None
+ | (min, max, rem, modulo) ->
+ let pint = interval_to_predicate_opt ~loc t min max in
+ let pcon = congruence_to_predicate_opt ~loc t rem modulo in
+ Extlib.merge_opt
+ (fun _ pint pcon -> Logic_const.pand ~loc (pint, pcon))
+ ()
+ pint
+ pcon
+
+
+(* [valid_to_predicate_opt ~loc t valid] may create validity predicate *only*
+ for valid locations. *)
+let valid_to_predicate_opt ~loc t valid =
+ let here_lbl = BuiltinLabel Here in
+ match valid with
+ | Base.Empty -> None
+ | Base.Known (bmn, bmx) | Base.Unknown (bmn, Some bmx, _) ->
+ let tbmn = Cil.lconstant ~loc bmn in
+ let tbmx = Cil.lconstant ~loc bmx in
+ let p = Logic_const.pvalid_range ~loc (here_lbl, t, tbmn, tbmx) in
+ Some p
+ | Base.Unknown (_, _, _) -> None
+ | Base.Variable { Base.min_alloc = bmn } when Integer.(equal bmn minus_one) ->
+ not_yet "Invalid Base.Variable above max_alloc";
+ None
+ | Base.Variable { Base.min_alloc = bmn; Base.max_alloc = bmx } ->
+ not_yet "Invalid Base.Variable above max_alloc";
+ let tbmn = Cil.lconstant ~loc bmn in
+ let tbmx = Cil.lconstant ~loc bmx in
+ let p = Logic_const.pvalid_range ~loc (here_lbl, t, tbmn, tbmx) in
+ Some p
+ | Base.Invalid ->
+ not_yet "Invalid Base";
+ None
+
+let base_to_predicate ~loc t (b: Base.t) =
+ match b with
+ | Base.Var (_vi, valid) | Base.Allocated (_vi, _, valid) ->
+ valid_to_predicate_opt ~loc t valid
+ | Base.CLogic_Var (_lvi, _typ, _) -> raise (Not_implemented "Base.CLogic_Var")
+ | Base.Null -> assert false (*by projecting ival*)
+ | Base.String _ -> raise (Not_implemented "Base.String")
+
+
+let base_offset_to_predicate ~loc t b o =
+ if Ival.equal Ival.zero o then
+ base_to_predicate ~loc t b
+ else begin
+ not_yet ~what:"Base w/ offsets";
+ None
+ end
+
+let _base_offsets_to_predicate ~loc t (m: Cvalue.V.M.t) =
+ let aux b o (acc: predicate list) =
+ let p_opt = base_offset_to_predicate ~loc t b o in
+ (Option.to_list p_opt) @ acc
+ in
+ match Cvalue.V.M.fold aux m [] with
+ | [] -> None
+ | ps -> Some (Logic_const.pands ps)
+
+let value_to_predicate_opt ?(loc=Location.unknown) t v =
+ let open Cvalue.V in
+ match v with
+ | Top _ -> None
+ | Map _m ->
+ try
+ let ival = project_ival v in
+ ival_to_predicate_opt ~loc t ival
+ with
+ | Not_based_on_null -> (* base_offsets_to_predicate ~loc t m *) None
+
+let exp_to_predicate ?(loc=Location.unknown) state e =
+ let value = !Db.Value.eval_expr ~with_alarms:CilE.warn_none_mode state e in
+ let te = Logic_utils.expr_to_term ~coerce:false e in
+ value_to_predicate_opt ~loc te value
+
+let lval_to_predicate ?(loc=Location.unknown) state lv =
+ let value = snd(!Db.Value.eval_lval
+ ~with_alarms:CilE.warn_none_mode None state lv)
+ in
+ let e = Cil.new_exp ~loc (Lval lv) in
+ let te = Logic_utils.expr_to_term ~coerce:false e in
+ value_to_predicate_opt ~loc te value
diff --git a/src/plugins/reduc/value2acsl.mli b/src/plugins/reduc/value2acsl.mli
new file mode 100644
index 0000000000000000000000000000000000000000..17546299c2191a9c2c5ea076b463904ccd48ed60
--- /dev/null
+++ b/src/plugins/reduc/value2acsl.mli
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(* [value_to_predicate_opt loc t value] may create a predicate given a [value]
+ about some [term].
+ @return None if no such predicate can be created. *)
+val value_to_predicate_opt: ?loc:location -> term -> Cvalue.V.t -> predicate option
+
+val lval_to_predicate: ?loc:location -> Cvalue.Model.t -> lval -> predicate option
+val exp_to_predicate: ?loc:location -> Cvalue.Model.t -> exp -> predicate option
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 668610d8cfccda532eb16e76f332df7ef6875d5a..2661b7572e3ec5d2ce5155fbca313e9155c447ed 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer
+type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer | Eva
type mvar = Raw | Var | Ref | Caveat
type setup = {
@@ -68,6 +68,7 @@ let descr_mheap d = function
| ZeroAlias -> main d "zeroalias"
| Hoare -> main d "hoare"
| Typed p -> main d "typed" ; descr_mtyped d p
+ | Eva -> main d "eva"
let descr_mvar d = function
| Var -> ()
@@ -238,6 +239,8 @@ module Model_Typed_Var = Register(Var)(MemTyped)
module Model_Typed_Ref = Register(Ref)(MemTyped)
module Model_Caveat = Register(Caveat)(MemTyped)
+module MemVal = MemVal.Make(MemVal.Eva)
+
module MakeCompiler(M:Sigs.Model) = struct
module M = M
module C = CodeSemantics.Make(M)
@@ -253,6 +256,7 @@ module Comp_MemTyped = MakeCompiler(MemTyped)
module Comp_Typed_Var = MakeCompiler(Model_Typed_Var)
module Comp_Typed_Ref = MakeCompiler(Model_Typed_Ref)
module Comp_Caveat = MakeCompiler(Model_Caveat)
+module Comp_MemVal = MakeCompiler(MemVal)
let compiler mheap mvar : (module Sigs.Compiler) =
@@ -265,6 +269,7 @@ let compiler mheap mvar : (module Sigs.Compiler) =
| Typed _ , Raw -> (module Comp_MemTyped)
| Typed _ , Var -> (module Comp_Typed_Var)
| Typed _ , Ref -> (module Comp_Typed_Ref)
+ | Eva, _ -> (module Comp_MemVal)
(* -------------------------------------------------------------------------- *)
(* --- Tuning --- *)
@@ -274,6 +279,7 @@ let configure_mheap = function
| Hoare -> MemEmpty.configure ()
| ZeroAlias -> MemZeroAlias.configure ()
| Region -> MemRegion.configure ()
+ | Eva -> MemVal.configure ()
| Typed p ->
let rollback_memtyped = MemTyped.configure () in
let orig_memtyped_pointer = Context.push MemTyped.pointer p in
@@ -343,6 +349,7 @@ let split ~warning (m:string) : string list =
(fun c ->
match c with
| 'A' .. 'Z' -> Buffer.add_char buffer c
+ | '0' .. '9' -> Buffer.add_char buffer c
| '_' | ',' | '@' | '+' | ' ' | '\t' | '\n' | '(' | ')' -> flush ()
| _ -> warning (Printf.sprintf
"In model spec %S : unexpected character '%c'" m c)
@@ -357,6 +364,7 @@ let update_config ~warning m s = function
| "TYPED" -> { s with mheap = Typed MemTyped.Fits }
| "CAST" -> { s with mheap = Typed MemTyped.Unsafe }
| "NOCAST" -> { s with mheap = Typed MemTyped.NoCast }
+ | "EVA" -> { s with mheap = Eva }
| "CAVEAT" -> { s with mvar = Caveat }
| "RAW" -> { s with mvar = Raw }
| "REF" -> { s with mvar = Ref }
diff --git a/src/plugins/wp/Factory.mli b/src/plugins/wp/Factory.mli
index 07df6d8730678c5a7341340e388aafc76db23630..9dbd3daf115a1e3e43a46896375f0b121227f388 100644
--- a/src/plugins/wp/Factory.mli
+++ b/src/plugins/wp/Factory.mli
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer
+type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer | Eva
type mvar = Raw | Var | Ref | Caveat
type setup = {
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index aebf56abb66ae105467c5a63c4667bcc9c9f9fed..8a0983e0ea936065024d4df7c5acb185158fc92e 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -128,7 +128,7 @@ let run_and_prove
(* --- Model Panel --- *)
(* ------------------------------------------------------------------------ *)
-type memory = TREE | HOARE | TYPED | REGION
+type memory = TREE | HOARE | TYPED | REGION | EVA
class model_selector (main : Design.main_window_extension_points) =
let dialog = new Wpane.dialog
@@ -136,6 +136,7 @@ class model_selector (main : Design.main_window_extension_points) =
let memory = new Widget.group HOARE in
let r_hoare = memory#add_radio ~label:"Hoare Memory Model" ~value:HOARE () in
let r_typed = memory#add_radio ~label:"Typed Memory Model" ~value:TYPED () in
+ let r_eva = memory#add_radio ~label:"Eva Memory Model" ~value:EVA () in
let c_casts = new Widget.checkbox ~label:"Unsafe casts" () in
let c_byref = new Widget.checkbox ~label:"Reference Arguments" () in
let c_ctxt = new Widget.checkbox ~label:"Context Arguments (Caveat)" () in
@@ -148,6 +149,7 @@ class model_selector (main : Design.main_window_extension_points) =
begin
dialog#add_row r_hoare#coerce ;
dialog#add_row r_typed#coerce ;
+ dialog#add_row r_eva#coerce ;
dialog#add_row c_casts#coerce ;
dialog#add_row c_byref#coerce ;
dialog#add_row c_ctxt#coerce ;
@@ -174,7 +176,9 @@ class model_selector (main : Design.main_window_extension_points) =
| ZeroAlias -> memory#set TREE
| Region -> memory#set REGION
| Hoare -> memory#set HOARE
- | Typed m -> memory#set TYPED ; c_casts#set (m = MemTyped.Unsafe)) ;
+ | Typed m -> memory#set TYPED ; c_casts#set (m = MemTyped.Unsafe)
+ | Eva -> memory#set EVA
+ ) ;
c_byref#set (s.mvar = Ref) ;
c_ctxt#set (s.mvar = Caveat) ;
c_cint#set (s.cint = Cint.Machine) ;
@@ -188,6 +192,7 @@ class model_selector (main : Design.main_window_extension_points) =
| HOARE -> Hoare
| TYPED -> Typed
(if c_casts#get then MemTyped.Unsafe else MemTyped.Fits)
+ | EVA -> Eva
in {
mheap = m ;
mvar = if c_ctxt#get then Caveat else if c_byref#get then Ref else Var ;
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index ffba8070d60ca2f3a44b4fcd662f65f7047ee3f3..a4b18ac20739034825c65368744722c99554305f 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -79,9 +79,9 @@ PLUGIN_CMO:= \
CodeSemantics \
LogicCompiler \
LogicSemantics LogicAssigns \
- Sigma MemLoader \
+ Sigma MemLoader MemDebug \
MemEmpty MemZeroAlias MemVar \
- MemMemory MemTyped MemRegion \
+ MemMemory MemTyped MemRegion MemVal \
wpReached wpRTE wpAnnot wpTarget \
CfgCompiler StmtSemantics \
VCS script proof wpo wpReport \
@@ -246,7 +246,7 @@ WP_API_BASE= \
Plang.mli Pcfg.mli Pcond.mli \
CodeSemantics.mli \
LogicCompiler.mli LogicSemantics.mli \
- Sigma.mli MemVar.mli MemTyped.mli \
+ Sigma.mli MemVar.mli MemTyped.mli MemVal.mli \
CfgCompiler.mli StmtSemantics.mli \
Factory.mli driver.mli VCS.mli Tactical.mli Strategy.mli Auto.mli \
VC.mli wpo.mli ProverTask.mli prover.mli
diff --git a/src/plugins/wp/MemDebug.ml b/src/plugins/wp/MemDebug.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3bbb3ce1476182a5820cf93b52e51fffb1582d48
--- /dev/null
+++ b/src/plugins/wp/MemDebug.ml
@@ -0,0 +1,279 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_datatype
+open Lang.F
+open Sigs
+
+(* ------------------------------------------------------------------------ *)
+(* ---- Pretty-printers ---- *)
+(* ------------------------------------------------------------------------ *)
+
+let pp_sequence pp_val fmt seq =
+ Format.fprintf fmt "@[{pre=%a,@,post=%a}@]"
+ pp_val seq.pre pp_val seq.post
+
+let pp_equation fmt = function
+ | Set (lt, rt) -> Format.fprintf fmt "@[%a =@, %a@]" pp_term lt pp_term rt
+ | Assert pred -> pp_pred fmt pred
+
+let pp_acs fmt = function
+ | RW -> Format.pp_print_string fmt "RW"
+ | RD -> Format.pp_print_string fmt "RD"
+ | OBJ -> Format.pp_print_string fmt "OBJ"
+
+let pp_value pp_loc fmt = function
+ | Val t -> pp_term fmt t
+ | Loc l -> pp_loc fmt l
+
+let pp_rloc pp_loc fmt = function
+ | Rloc(_obj,l) -> Format.fprintf fmt "[@{%a}@]" pp_loc l
+ | Rrange(l,_obj,tmin,tmax) ->
+ Format.fprintf fmt "@[%a+(%a..%a)@]" pp_loc l
+ (Pretty_utils.pp_opt pp_term) tmin (Pretty_utils.pp_opt pp_term) tmax
+
+let pp_sloc pp_loc fmt = function
+ | Sloc l -> Format.fprintf fmt "@[{%a}@]" pp_loc l
+ | Sarray(l,_obj,size) -> Format.fprintf fmt "@[%a+(0..%d)@]" pp_loc l size
+ | Srange(l,_obj,tmin,tmax) ->
+ Format.fprintf fmt "@[%a+(%a..%a)@]" pp_loc l
+ (Pretty_utils.pp_opt pp_term) tmin (Pretty_utils.pp_opt pp_term) tmax
+ | Sdescr(xs,l,p) ->
+ Format.fprintf fmt "@[{ %a @,| %a@,; %a }@]" pp_loc l
+ (Pretty_utils.pp_list pp_var) xs pp_pred p
+
+(* ------------------------------------------------------------------------ *)
+(* ---- Debug Memory Model ---- *)
+(* ------------------------------------------------------------------------ *)
+
+let dkey_cons = Wp_parameters.register_category "memdebug:cons"
+let dkey_loc = Wp_parameters.register_category "memdebug:loc"
+let dkey_cast = Wp_parameters.register_category "memdebug:cast"
+let dkey_access = Wp_parameters.register_category "memdebug:access"
+let dkey_valid = Wp_parameters.register_category "memdebug:valid"
+let dkey_alias = Wp_parameters.register_category "memdebug:alias"
+
+let debug_cons = Wp_parameters.debug ~dkey:dkey_cons
+let debug_loc = Wp_parameters.debug ~dkey:dkey_loc
+let debug_cast = Wp_parameters.debug ~dkey:dkey_cast
+let debug_access = Wp_parameters.debug ~dkey:dkey_access
+let debug_valid = Wp_parameters.debug ~dkey:dkey_valid
+let debug_alias = Wp_parameters.debug ~dkey:dkey_alias
+
+module Make(M : Sigs.Model) =
+struct
+ let datatype = "MemDebug." ^ M.datatype
+ let configure = M.configure
+
+ let hypotheses = M.hypotheses
+
+ module Chunk = M.Chunk
+
+ module Heap = M.Heap
+ module Sigma = M.Sigma
+
+ type loc = M.loc
+ type chunk = M.chunk
+ type sigma = M.sigma
+ type segment = M.segment
+ type state = M.state
+
+ (* ---------------------------------------------------------------------- *)
+ (* ---- Pretty-printing ---- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let pretty = M.pretty
+
+ let state = M.state
+ let iter = M.iter
+ let lookup = M.lookup
+ let updates = M.updates
+ let apply = M.apply
+
+ let vars = M.vars
+ let occurs = M.occurs
+
+ (* ---------------------------------------------------------------------- *)
+ (* ---- Constructors ----- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let null =
+ let l = M.null in debug_cons "null:@, %a" pretty l;
+ M.null
+
+ let literal ~eid cstr =
+ let l = M.literal ~eid cstr in
+ debug_cons "literal ~eid:%d ->@, %a" eid pretty l;
+ l
+
+ let cvar x =
+ let l = M.cvar x in
+ debug_cons "cvar %a ->@, %a" Varinfo.pretty x pretty l;
+ l
+
+ let pointer_loc e =
+ let l = M.pointer_loc e in
+ debug_cons "term2loc %a ->@, %a" pp_term e pretty l;
+ l
+ let pointer_val l =
+ let e = M.pointer_val l in
+ debug_cons "loc2term %a ->@, %a" pretty l pp_term e;
+ e
+
+ (* ---------------------------------------------------------------------- *)
+ (* ---- Operations ---- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let field l fd =
+ let l' = M.field l fd in
+ debug_loc "@[%a.%a ->@, %a@]" pretty l Fieldinfo.pretty fd pretty l';
+ l'
+ let shift l obj e =
+ let l' = M.shift l obj e in
+ debug_loc "@[%a+%a ->@, %a@]" pretty l pp_term e pretty l';
+ l'
+
+ let base_addr l =
+ let l' = M.base_addr l in
+ debug_loc "@[base_addr: %a -> %a@]" pretty l pretty l';
+ l'
+
+ let block_length = M.block_length
+
+ (* ---------------------------------------------------------------------- *)
+ (* ---- Casting ----- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let cast ty l =
+ let l' = M.cast ty l in
+ debug_cast "(%a)%a -> %a" Ctypes.pretty ty.post pretty l pretty l';
+ l'
+
+ let loc_of_int obj e =
+ let l = M.loc_of_int obj e in
+ debug_cast "(%a)%a -> %a" Ctypes.pretty obj pp_term e pretty l;
+ l
+ let int_of_loc cint l =
+ let e = M.int_of_loc cint l in
+ debug_cast "(%a)%a -> %a" Ctypes.pp_int cint pretty l pp_term e;
+ e
+
+ (* ---------------------------------------------------------------------- *)
+ (* ---- Domain ----- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let domain = M.domain
+
+ (* ---------------------------------------------------------------------- *)
+ (* ---- Memory Access ----- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let load s obj l =
+ let v = M.load s obj l in
+ debug_access "@[load %a @, %a @, %a ->@, %a@]@."
+ Sigma.pretty s Ctypes.pretty obj pretty l (pp_value pretty) v;
+ v
+
+ let load_init _s _obj _l = e_false
+
+ let stored seq obj l t =
+ let preds = M.stored seq obj l t in
+ debug_access "@[stored %a@, %a@, %a@, %a ->@, %a@]@."
+ (pp_sequence Sigma.pretty) seq Ctypes.pretty obj pretty l pp_term t
+ (Pretty_utils.pp_list pp_equation) preds;
+ preds
+
+ let stored_init _seq _obj _l _v = []
+
+ let copied seq obj ll rl =
+ let preds = M.copied seq obj ll rl in
+ debug_access "@[copied %a@, %a@, %a@, %a ->@, %a@]@."
+ (pp_sequence Sigma.pretty) seq Ctypes.pretty obj pretty ll pretty rl
+ (Pretty_utils.pp_list pp_equation) preds;
+ preds
+
+ let copied_init _seq _obj _ll _rl = []
+
+ let assigned seq obj sloc =
+ let preds = M.assigned seq obj sloc in
+ debug_access "@[assigned %a@, %a@, %a ->@, %a@]@."
+ (pp_sequence Sigma.pretty) seq Ctypes.pretty obj (pp_sloc pretty) sloc
+ (Pretty_utils.pp_list pp_equation) preds;
+ preds
+
+ (* ---------------------------------------------------------------------- *)
+ (* ---- Pointer Comparison ----- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let is_null = M.is_null
+ let loc_eq = M.loc_eq
+ let loc_lt = M.loc_lt
+ let loc_leq = M.loc_leq
+ let loc_neq = M.loc_neq
+ let loc_diff = M.loc_diff
+
+ (* ---------------------------------------------------------------------- *)
+ (* ---- Validity ----- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let valid s acs seg =
+ let p = M.valid s acs seg in
+ debug_valid "@[valid %a@, %a@, %a ->@, %a@]@."
+ Sigma.pretty s pp_acs acs (pp_rloc pretty) seg pp_pred p;
+ p
+
+ let invalid s seg =
+ let p = M.invalid s seg in
+ debug_valid "@[invalid %a@, %a ->@, %a@]@."
+ Sigma.pretty s (pp_rloc pretty) seg pp_pred p;
+ p
+
+ let scope = M.scope
+ let global = M.global
+
+ (* ---------------------------------------------------------------------- *)
+ (* ---- Separation ----- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let included seg1 seg2 =
+ let p = M.included seg1 seg2 in
+ debug_alias "@[included %a@, %a ->@, %a@]@."
+ (pp_rloc pretty) seg1 (pp_rloc pretty) seg2 pp_pred p;
+ p
+
+ let separated seg1 seg2 =
+ let p = M.separated seg1 seg2 in
+ debug_alias "@[separated %a@, %a ->@, %a@]@."
+ (pp_rloc pretty) seg1 (pp_rloc pretty) seg2 pp_pred p;
+ p
+
+
+ (** todo *)
+ let initialized = M.initialized
+ let alloc = M.alloc
+ let frame = M.frame
+ let is_well_formed = M.is_well_formed
+ let base_offset = M.base_offset
+ type domain = M.domain
+ let configure_ia = M.configure_ia
+
+end
diff --git a/src/plugins/wp/MemDebug.mli b/src/plugins/wp/MemDebug.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d38816004981795e510d88783c5c9d1205c5ab1f
--- /dev/null
+++ b/src/plugins/wp/MemDebug.mli
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Debug Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+val pp_sequence : 'a Pretty_utils.formatter -> Format.formatter ->
+ 'a Sigs.sequence -> unit
+val pp_equation : Format.formatter -> Sigs.equation -> unit
+val pp_acs : Format.formatter -> Sigs.acs -> unit
+val pp_value : 'a Pretty_utils.formatter -> Format.formatter ->
+ 'a Sigs.value -> unit
+val pp_rloc : 'a Pretty_utils.formatter -> Format.formatter ->
+ 'a Sigs.rloc -> unit
+val pp_sloc : 'a Pretty_utils.formatter -> Format.formatter ->
+ 'a Sigs.sloc -> unit
+
+module Make(M : Sigs.Model) : Sigs.Model
diff --git a/src/plugins/wp/MemVal.ml b/src/plugins/wp/MemVal.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7b1be408b07648a8895a84cdf628a9c21d6e2aef
--- /dev/null
+++ b/src/plugins/wp/MemVal.ml
@@ -0,0 +1,869 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Value Separation Analysis' Based Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+open Cil_types
+open Cil_datatype
+open Ctypes
+open Lang
+open Lang.F
+open Sigs
+open Definitions
+
+module Logic = Qed.Logic
+
+module type State =
+sig
+ type t
+
+ val bottom : t
+ val join : t -> t -> t
+
+ val of_kinstr : Cil_types.kinstr -> t
+ val of_stmt : Cil_types.stmt -> t
+ val of_kf : Cil_types.kernel_function -> t
+
+ val pretty : Format.formatter -> t -> unit
+end
+
+module type Value =
+sig
+ val configure : unit -> WpContext.rollback
+ val datatype : string
+
+ module State : State
+
+ type t
+ type state = State.t
+
+ val null : t
+ val literal: eid:int -> Cstring.cst -> int * t
+ val cvar : varinfo -> t
+
+ val field : t -> Cil_types.fieldinfo -> t
+ val shift : t -> Ctypes.c_object -> term -> t
+ val base_addr : t -> t
+
+ val load : state -> t -> Ctypes.c_object -> t
+
+ val domain : t -> Base.t list
+ val offset : t -> (term -> pred)
+
+ val pretty : Format.formatter -> t -> unit
+end
+
+module type Base =
+sig
+end
+
+let dkey = Wp_parameters.register_category "memval" (* Debugging key *)
+let dkey_val = Wp_parameters.register_category "memval:val"
+
+let debug fmt = Wp_parameters.debug ~dkey fmt
+let debug_val = Wp_parameters.debug ~dkey:dkey_val
+
+
+(* -------------------------------------------------------------------------- *)
+(* --- Logic Memory Wrapper --- *)
+(* -------------------------------------------------------------------------- *)
+let library = "memory"
+
+let a_addr = Lang.datatype ~library "addr"
+let t_addr = Logic.Data(a_addr,[])
+let f_base = Lang.extern_f ~library ~result:Logic.Int
+ ~link:{altergo = Qed.Engine.F_subst("%1.base");
+ why3 = Qed.Engine.F_subst("%1.base");
+ coq = Qed.Engine.F_subst("(base %1)");
+ } "base"
+let f_offset = Lang.extern_f ~library ~result:Logic.Int
+ ~link:{altergo = Qed.Engine.F_subst("%1.offset");
+ why3 = Qed.Engine.F_subst("%1.offset");
+ coq = Qed.Engine.F_subst("(offset %1)");
+ } "offset"
+let f_shift = Lang.extern_f ~library ~result:t_addr "shift"
+let f_global = Lang.extern_f ~library ~result:t_addr "global"
+let f_null = Lang.extern_f ~library ~result:t_addr "null"
+
+let a_null = F.constant (e_fun f_null []) (* { base = 0; offset = 0 } *)
+let a_base p = e_fun f_base [p] (* p -> p.offset *)
+let a_offset p = e_fun f_offset [p] (* p -> p.base *)
+let a_global b = e_fun f_global [b] (* b -> { base = b; offset = 0 } *)
+let a_shift l k = e_fun f_shift [l;k] (* p k -> { p w/ offset = p.offset + k } *)
+let a_addr b k = a_shift (a_global b) k (* b k -> { base = b; offset = k } *)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Cmath Wrapper --- *)
+(* -------------------------------------------------------------------------- *)
+let a_iabs i = e_fun ~result:Logic.Int Cmath.f_iabs [i] (* x -> |x| *)
+
+(* -------------------------------------------------------------------------- *)
+(* --- MemValue Types --- *)
+(* -------------------------------------------------------------------------- *)
+(* Model utilities *)
+let t_words = Logic.Array (Logic.Int, Logic.Int) (* TODO: A way to abstract this ? *)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Qed Simplifiers --- *)
+(* -------------------------------------------------------------------------- *)
+let phi_base t = match F.repr t with
+ | Logic.Fun (f, [p; _]) when f == f_shift -> a_base p
+ | Logic.Fun (f, [b]) when f == f_global -> b
+ | _ -> raise Not_found
+
+let phi_offset t = match F.repr t with
+ | Logic.Fun (f, [p; k]) when f == f_shift -> e_add (a_offset p) k
+ | Logic.Fun (f, _) when f == f_global -> F.e_zero
+ | _ -> raise Not_found
+
+let phi_shift p i =
+ if F.is_zero i then p
+ else match F.repr p with
+ | Logic.Fun (f, [q; j]) when f == f_shift -> F.e_fun f [q; F.e_add i j]
+ (* | Logic.Fun (f, [b]) when f == f_global -> a_addr b i *)
+ | _ -> raise Not_found
+
+let phi_read ~obj ~read ~write mem off = match F.repr mem with
+ | Logic.Fun (f, [_; o; v]) when f == write && off == o -> v
+ (*read_tau (write_tau m o v) o == v*)
+ | Logic.Fun (f, [m; o; _]) when f == write ->
+ let offset = a_iabs (F.e_sub off o) in
+ if F.eval_leq (F.e_int (Ctypes.sizeof_object obj)) offset then
+ F.e_fun read [m; off]
+ else raise Not_found
+ (*read_tau (write_tau m o v) o' == read m o' when |o - o'| <= sizeof(tau)*)
+ | _ -> raise Not_found
+
+let () = Context.register
+ begin fun () ->
+ F.set_builtin_1 f_base phi_base;
+ F.set_builtin_1 f_offset phi_offset;
+ F.set_builtin_2 f_shift phi_shift;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Utilities --- *)
+(* -------------------------------------------------------------------------- *)
+(* Wp utilities *)
+module Cstring =
+struct
+ include Cstring
+
+ let str_cil ~eid cstr =
+ let enode = match cstr with
+ | C_str str -> Const (CStr str)
+ | W_str wstr -> Const (CWStr wstr)
+ in {
+ eid = eid;
+ enode = enode;
+ eloc = Location.unknown;
+ }
+end
+
+(* Value utilities *)
+module Base =
+struct
+ include Base
+
+ let bitsize_from_validity = function
+ | Invalid -> Integer.zero
+ | Empty -> Integer.zero
+ | Known (_, m)
+ | Unknown (_, _, m) -> Integer.succ m
+ | Variable { max_allocable } -> Integer.succ max_allocable
+
+ let size_from_validity b =
+ Integer.(e_div (bitsize_from_validity b) eight)
+end
+
+
+(* -------------------------------------------------------------------------- *)
+(* --- Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+module Make(V : Value) =
+struct
+ (* -------------------------------------------------------------------------- *)
+ (* --- Model Parameters --- *)
+ (* -------------------------------------------------------------------------- *)
+ let datatype = "MemVal." ^ V.datatype
+ let configure () =
+ let rollback = V.configure () in
+ let orig_pointer = Context.push Lang.pointer t_addr in
+ let rollback () =
+ rollback ();
+ Context.pop Lang.pointer orig_pointer;
+ in
+ rollback
+
+ module StateRef =
+ struct
+ let model : V.State.t Context.value = Context.create "Memval.model"
+ let get () = Context.get model
+ let update () =
+ try
+ (match WpContext.get_scope () with
+ | WpContext.Global -> assert false
+ | WpContext.Kf kf -> Context.set model (V.State.of_kf kf))
+ with | Invalid_argument _ -> Context.set model (V.State.of_kinstr Kglobal)
+ | Kernel_function.No_Definition -> assert false
+ end
+ (* -------------------------------------------------------------------------- *)
+ (* --- Chunk --- *)
+ (* -------------------------------------------------------------------------- *)
+ type chunk =
+ | M_base of Base.t
+
+ module Chunk =
+ struct
+ type t = chunk
+ let self = "MemVal.Chunk"
+ let hash = function
+ | M_base b -> 5 * Base.hash b
+ let equal c1 c2 = match c1, c2 with
+ | M_base b1, M_base b2 -> Base.equal b1 b2
+ let compare c1 c2 = match c1, c2 with
+ | M_base b1, M_base b2 -> Base.compare b1 b2
+ let pretty fmt = function
+ | M_base b -> Base.pretty fmt b
+ let tau_of_chunk = function
+ | M_base _ -> t_words
+ let basename_of_base = function
+ | Base.Var (vi, _) -> Format.sprintf "MVar_%s" (LogicUsage.basename vi)
+ | Base.CLogic_Var (_, _, _) -> assert false (* not supposed to append. *)
+ | Base.Null -> "MNull"
+ | Base.String (eid, _) -> Format.sprintf "MStr_%d" eid
+ | Base.Allocated (vi, _dealloc, _) ->
+ Format.sprintf "MAlloc_%s" (LogicUsage.basename vi)
+ let basename_of_chunk = function
+ | M_base b -> basename_of_base b
+ let is_framed = function
+ | M_base b ->
+ try
+ (match WpContext.get_scope () with
+ | WpContext.Global -> assert false
+ | WpContext.Kf kf -> Base.is_formal_or_local b (Kernel_function.get_definition kf))
+ with Invalid_argument _ | Kernel_function.No_Definition ->
+ assert false (* by context. *)
+ end
+
+ let cluster () = Definitions.cluster ~id:"MemVal" ()
+
+ module Heap = Qed.Collection.Make(Chunk)
+ module Sigma = Sigma.Make(Chunk)(Heap)
+
+ type loc = {
+ loc_v : V.t;
+ loc_t : term (* of type addr *)
+ }
+
+ type sigma = Sigma.t
+ type segment = loc rloc
+
+ type state = unit
+ let state _ = ()
+ let iter _ _ = ()
+ let lookup _ _ = Mterm
+ let updates _ _ = Bag.empty
+ let apply _ _ = ()
+
+ let pretty fmt l =
+ Format.fprintf fmt "([@ t:%a,@ v:%a @])"
+ F.pp_term l.loc_t
+ V.pretty l.loc_v
+
+ let vars _l = Vars.empty
+ let occurs _x _l = false
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Constructors --- *)
+ (* -------------------------------------------------------------------------- *)
+ let null = {
+ loc_v = V.null;
+ loc_t = a_null;
+ }
+
+ let literal ~eid cstr =
+ let bid, v = V.literal ~eid cstr in
+ {
+ loc_v = v;
+ loc_t = a_global (F.e_int bid)
+ }
+
+ let cvar x = {
+ loc_v = V.cvar x;
+ loc_t = a_addr (F.e_int (Base.id (Base.of_varinfo x))) (F.e_zero);
+ }
+
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Generated Axiomatization --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ module Obj =
+ struct
+ include C_object
+
+ let compare a b =
+ if a==b then 0 else
+ match a, b with
+ | C_pointer _, C_pointer _ -> 0
+ | _ -> compare a b
+ end
+
+ module Access = WpContext.Generator(Obj)
+ (struct
+ let name = "MemVal.Access"
+ type key = c_object
+ type data = lfun * lfun
+
+ let read suffix t_mem t_data =
+ let result = t_data in
+ let lfun = Lang.generated_f ~result "read_%s" suffix in
+ let xw = Lang.freshvar ~basename:"w" t_mem in
+ let xo = Lang.freshvar ~basename:"o" Logic.Int in
+ let dfun = Definitions.Logic result in
+ let cluster = cluster () in
+ Definitions.define_symbol {
+ d_lfun = lfun; d_types = 0;
+ d_params = [xw; xo];
+ d_definition = dfun;
+ d_cluster = cluster;
+ };
+ lfun
+
+ let write suffix t_mem t_data =
+ let result = t_mem in
+ let lfun = Lang.generated_f ~result "write_%s" suffix in
+ let xw = Lang.freshvar ~basename:"w" t_mem in
+ let xo = Lang.freshvar ~basename:"o" Logic.Int in
+ let xv = Lang.freshvar ~basename:"v" t_data in
+ let dfun = Definitions.Logic result in
+ let cluster = cluster () in
+ Definitions.define_symbol {
+ d_lfun = lfun; d_types = 0;
+ d_params = [xw; xo; xv];
+ d_definition = dfun;
+ d_cluster = cluster;
+ };
+ lfun
+
+ let axiomatize ~obj:_ suffix t_mem t_data f_rd f_wr =
+ let name = "axiom_" ^ suffix in
+ let xw = Lang.freshvar ~basename:"w" t_mem in
+ let w = e_var xw in
+ let xo = Lang.freshvar ~basename:"o" Logic.Int in
+ let o = e_var xo in
+ let xv = Lang.freshvar ~basename:"v" t_data in
+ let v = e_var xv in
+ let p_write = e_fun f_wr [w; o; v] ~result:t_mem in
+ let p_read = e_fun f_rd [p_write; o] ~result:t_data in
+ let lemma = p_equal p_read v in
+ let cluster = cluster () in
+ (* if not (Wp_parameters.debug_atleast 1) then begin
+ * F.set_builtin_2 f_rd (phi_read ~obj ~read:f_rd ~write:f_wr)
+ * end; *)
+ Definitions.define_lemma {
+ l_kind = Cil_types.Admit;
+ l_name = name; l_types = 0;
+ l_triggers = [];
+ l_forall = [xw; xo; xv];
+ l_lemma = lemma;
+ l_cluster = cluster;
+ }
+
+ let axiomatize2 ~obj suffix t_mem t_data f_rd f_wr =
+ let name = "axiom_" ^ suffix ^ "_2" in
+ let xw = Lang.freshvar ~basename:"w" t_mem in
+ let w = e_var xw in
+ let xwo = Lang.freshvar ~basename:"xwo" Logic.Int in
+ let wo = e_var xwo in
+ let xro = Lang.freshvar ~basename:"xro" Logic.Int in
+ let ro = e_var xro in
+ let xv = Lang.freshvar ~basename:"v" t_data in
+ let v = e_var xv in
+ let p_write = e_fun f_wr [w; wo; v] ~result:t_mem in
+ let p_read = e_fun f_rd [p_write; ro] ~result:t_data in
+ let sizeof = (F.e_int (Ctypes.sizeof_object obj)) in
+ let offset = a_iabs (F.e_sub ro wo) in
+ let lemma =
+ F.p_imply
+ (F.p_leq sizeof offset)
+ (F.p_equal p_read (e_fun f_rd [w; ro] ~result:t_data))
+ in
+ let cluster = cluster () in
+ Definitions.define_lemma {
+ l_kind = Cil_types.Admit;
+ l_name = name; l_types = 0;
+ l_triggers = [];
+ l_forall = [xw; xwo; xro; xv];
+ l_lemma = lemma;
+ l_cluster = cluster;
+ }
+
+ let generate obj =
+ let suffix = Ctypes.basename obj in
+ let t_mem = t_words in
+ let t_data = Lang.tau_of_object obj in
+ let d_read = read suffix t_mem t_data in
+ let d_write = write suffix t_mem t_data in
+ axiomatize ~obj suffix t_mem t_data d_read d_write;
+ axiomatize2 ~obj suffix t_mem t_data d_read d_write;
+ d_read, d_write
+
+ let compile = Lang.local generate
+ end)
+
+ let read obj ~mem ~offset =
+ F.e_fun (fst (Access.get obj)) [mem; offset] ~result:(Lang.tau_of_object obj)
+ let write obj ~mem ~offset ~value =
+ F.e_fun (snd (Access.get obj)) [mem; offset; value] ~result:t_words
+
+ let fold_ite f l =
+ let rec aux = function
+ | [] -> assert false
+ | [x] -> f x
+ | x :: xs ->
+ F.e_if
+ (F.e_eq (a_base l.loc_t) (F.e_int (Base.id x)))
+ (f x)
+ (aux xs)
+ in
+ aux (V.domain l.loc_v)
+
+ let fold_ite_pred f l =
+ let rec aux = function
+ | [] -> assert false
+ | [x] -> f x
+ | x :: xs ->
+ F.p_if
+ (F.p_equal (a_base l.loc_t) (F.e_int (Base.id x)))
+ (f x)
+ (aux xs)
+ in
+ aux (V.domain l.loc_v)
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Logic to Location (and resp.) --- *)
+ (* -------------------------------------------------------------------------- *)
+ let pointer_loc _ = Warning.error ~source:"MemVal" "Cannot build top from EVA"
+
+ let pointer_val l = l.loc_t
+
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Lifting --- *)
+ (* -------------------------------------------------------------------------- *)
+ let field l fd =
+ let offs = Integer.of_int (Ctypes.field_offset fd) in
+ {
+ loc_v = V.field l.loc_v fd;
+ loc_t = a_shift l.loc_t (F.e_bigint offs);
+ }
+
+ let shift l obj k =
+ let size = Integer.of_int (Ctypes.sizeof_object obj) in
+ let offs = F.e_times size k in
+ {
+ loc_v = V.shift l.loc_v obj k;
+ loc_t = a_shift l.loc_t offs;
+ }
+
+ let base_addr l =
+ {
+ loc_v = V.base_addr l.loc_v;
+ loc_t = a_addr (a_base l.loc_t) F.e_zero;
+ }
+
+ let block_length _s _obj l =
+ let size_from_base base =
+ F.e_bigint Base.(size_from_validity (validity base))
+ in
+ fold_ite size_from_base l
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Casting --- *)
+ (* -------------------------------------------------------------------------- *)
+ let cast _ l = l
+
+ let loc_of_int _ v =
+ if F.is_zero v then null
+ else
+ (*TODO: Reinterpret integer with Value *)
+ Warning.error ~source:"MemVal Model"
+ "Forbidden cast of int to pointer"
+
+ let int_of_loc _ l = pointer_val l
+
+ let domain _ l =
+ let d = V.domain l.loc_v in
+ assert (d <> []);
+ List.fold_left
+ (fun acc b -> Heap.Set.add (M_base b) acc)
+ Heap.Set.empty d
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Memory Load --- *)
+ (* -------------------------------------------------------------------------- *)
+ let load_value sigma obj l =
+ let load_base base =
+ let mem = Sigma.value sigma (M_base base) in
+ let offset = a_offset l.loc_t in
+ read obj ~mem ~offset
+ in
+ let t = fold_ite load_base l in
+ begin if Wp_parameters.has_dkey dkey_val then
+ let v = V.load (StateRef.get ()) l.loc_v obj in
+ debug_val "load: %a -> %a" V.pretty l.loc_v V.pretty v
+ end;
+ Val t
+
+ let load_loc ~assume sigma obj l =
+ let load_base v' base =
+ let mem = Sigma.value sigma (M_base base) in
+ let offset = a_offset l.loc_t in
+ let rd = read obj ~mem ~offset in
+ if assume then begin
+ let pred = V.offset v' (a_offset rd) in
+ Lang.assume pred (* Yet another mutable. *)
+ end;
+ rd
+ in
+ let v' = V.load (StateRef.get ()) l.loc_v obj in
+ let t = fold_ite (load_base v') l in
+ Loc {
+ loc_v = V.load (StateRef.get ()) l.loc_v obj;
+ loc_t = t;
+ }
+
+ let load : sigma -> c_object -> loc -> loc value = fun sigma obj l ->
+ StateRef.update ();
+ begin match obj with
+ | C_int _ | C_float _ -> load_value sigma obj l
+ | C_pointer _ -> load_loc ~assume:true sigma obj l
+ | _ -> load_loc ~assume:false sigma obj l
+ end
+
+ let load_init _sigma obj _loc =
+ e_var @@ Lang.freshvar ~basename:"i" @@ Lang.init_of_object obj
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Memory Store --- *)
+ (* -------------------------------------------------------------------------- *)
+ let stored : sigma sequence -> c_object -> loc -> term -> equation list = fun seq obj l v ->
+ let mk_write cond base =
+ let wpre = Sigma.value seq.pre (M_base base) in
+ let wpost = Sigma.value seq.post (M_base base) in
+ let write = write obj ~mem:wpre ~offset:(a_offset l.loc_t) ~value:v in
+ F.p_equal wpost (F.e_if cond write wpre)
+ in
+ let rec store acc = function
+ | [] -> assert false
+ | [c] ->
+ let cond = F.e_and ((List.map (F.e_neq (a_base l.loc_t))) acc) in
+ [ Assert (mk_write cond c) ]
+ | c :: cs ->
+ let bid = (F.e_int (Base.id c)) in
+ let cond = F.e_eq (a_base l.loc_t) bid in
+ [ Assert (mk_write cond c) ]
+ @ store (bid :: acc) cs
+ in
+ store [ ] (V.domain l.loc_v)
+
+ let stored_init _seq _obj _loc _t = []
+
+ let copied seq obj ll lr =
+ let v = match load seq.pre obj lr with
+ | Sigs.Val v -> v
+ | Sigs.Loc l -> l.loc_t
+ in
+ stored seq obj ll v
+
+ let copied_init _seq _obj _ll _lr = []
+
+ let assigned _s _obj _sloc = [ Assert F.p_true ]
+
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Pointer Comparison --- *)
+ (* -------------------------------------------------------------------------- *)
+ let is_null l = p_equal l.loc_t a_null
+
+ let loc_delta l1 l2 =
+ match F.is_equal (a_base l1.loc_t) (a_base l2.loc_t) with
+ | Logic.Yes -> F.e_sub (a_offset l1.loc_t) (a_offset l2.loc_t)
+ | Logic.Maybe | Logic.No ->
+ Warning.error "Can only compare pointers with same base."
+
+ let base_eq l1 l2 = F.p_equal (a_base l1.loc_t) (a_base l2.loc_t)
+ let offset_cmp cmpop l1 l2 = cmpop (a_offset l1.loc_t) (a_offset l2.loc_t)
+
+ let loc_diff _obj l1 l2 = loc_delta l1 l2
+ let loc_eq l1 l2 = F.p_and (base_eq l1 l2) (offset_cmp F.p_equal l1 l2)
+ let loc_lt l1 l2 = F.p_lt (loc_delta l1 l2) F.e_zero
+ let loc_leq l1 l2 = F.p_leq (loc_delta l1 l2) F.e_zero
+ let loc_neq l1 l2 = F.p_neq (loc_delta l1 l2) F.e_zero
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Segments --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ type range =
+ | LOC of loc * term (*size*)
+ | RANGE of loc * Vset.set (* offset range access from *loc* *)
+
+ let range_of_rloc = function
+ | Rloc (obj, l) ->
+ LOC (l, F.e_int (Ctypes.sizeof_object obj))
+ | Rrange (l, obj, Some a, Some b) ->
+ let la = shift l obj a in
+ let n = e_fact (Ctypes.sizeof_object obj) (F.e_range a b) in
+ LOC (la, n)
+ | Rrange (l, obj, a_opt, b_opt) ->
+ let f = F.e_fact (Ctypes.sizeof_object obj) in
+ RANGE (l, Vset.range (Option.map f a_opt) (Option.map f b_opt))
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Validity --- *)
+ (* -------------------------------------------------------------------------- *)
+ (** [vset_from_validity base] returns the logical set of all valid bytes of
+ [base]. **)
+ let vset_from_validity = function
+ | Base.Empty -> Vset.empty
+ | Base.Invalid -> Vset.singleton F.e_zero
+ | Base.Known (min_valid, max_valid)
+ | Base.Unknown (min_valid, Some max_valid, _) ->
+ (* valid between min_valid .. max_valid inclusive *)
+ let mn = F.e_bigint Integer.(e_div min_valid eight) in
+ let mx = F.e_bigint Integer.(e_div max_valid eight) in
+ Vset.range (Some mn) (Some mx)
+ | Base.Variable { Base.min_alloc = min_valid } ->
+ (* valid between 0 .. min_valid inclusive *)
+ let mn_valid = F.e_bigint Integer.(e_div min_valid eight) in
+ Vset.range (Some F.e_zero) (Some mn_valid)
+ | Base.Unknown (_, None, _) -> Vset.empty
+
+ let valid_range : sigma -> acs -> range -> pred = fun _ acs r ->
+ let for_writing = match acs with RW -> true | RD -> false
+ | OBJ -> true (* TODO: *) in
+ let l, base_offset = match r with
+ | LOC (l, n) ->
+ let a = a_offset l.loc_t in
+ let b = F.e_add a (F.e_sub n F.e_one) in
+ l, Vset.range (Some a) (Some b)
+ | RANGE (l, r) -> l, Vset.lift_add (Vset.singleton l.loc_t) r
+ in
+ let valid_base set base =
+ if for_writing && (Base.is_read_only base) then
+ F.p_false
+ else
+ let base_vset = vset_from_validity (Base.validity base) in
+ Vset.subset set base_vset
+ in
+ fold_ite_pred (valid_base base_offset) l
+
+ (** [valid sigma acs seg] returns the formula that tests if a given memory
+ segment [seg] (in bytes) is valid (according to [acs]) at memory state
+ [sigma]. **)
+ let valid : sigma -> acs -> segment -> pred = fun s acs seg ->
+ valid_range s acs (range_of_rloc seg)
+
+ let invalid = fun _ _ -> F.p_true (* TODO *)
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Scope --- *)
+ (* -------------------------------------------------------------------------- *)
+ let alloc_sigma : sigma -> varinfo list -> sigma = fun sigma xs ->
+ let alloc sigma x =
+ let havoc s c = Sigma.havoc_chunk s (M_base c) in
+ let v = V.cvar x in
+ List.fold_left havoc sigma (V.domain v)
+ in
+ List.fold_left alloc sigma xs
+
+ let alloc_pred _ _ _ = []
+
+ let alloc sigma xs =
+ if xs = [] then sigma else alloc_sigma sigma xs
+
+ let scope : sigma sequence -> scope -> varinfo list -> pred list = fun seq scope xs ->
+ match scope with
+ | Enter -> []
+ | Leave ->
+ alloc_pred seq xs ()
+
+ let scope seq sc xs =
+ let preds = scope seq sc xs in
+ debug "[scope pre:%a post:%a xs:%a] -> preds:%a"
+ Sigma.pretty seq.pre
+ Sigma.pretty seq.post
+ (Pretty_utils.pp_iter ~sep:" " List.iter Varinfo.pretty) xs
+ (Pretty_utils.pp_iter ~sep:" " List.iter pp_pred) preds;
+ preds
+
+ let global : sigma -> term (*addr*) -> pred = fun _ _ ->
+ F.p_true (* True is harmless and WP never call this function... *)
+
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Separation --- *)
+ (* -------------------------------------------------------------------------- *)
+ let range_to_base_offset = function
+ | LOC (l, n) ->
+ let a = a_offset l.loc_t in
+ let b = F.e_add a n in
+ l, Vset.range (Some a) (Some b)
+ | RANGE (l, r) -> l, Vset.lift_add (Vset.singleton l.loc_t) r
+
+ let included : segment -> segment -> pred = fun s1 s2 ->
+ (* (b1 = b2) -> (r1 \in r2) *)
+ let l1, vs1 = range_to_base_offset (range_of_rloc s1) in
+ let l2, vs2 = range_to_base_offset (range_of_rloc s2) in
+ p_and
+ (p_equal (a_base l1.loc_t) (a_base l2.loc_t))
+ (Vset.subset vs1 vs2)
+
+ let separated : segment -> segment -> pred = fun s1 s2 ->
+ (* (b1 = b2) -> (r1 \cap r2) = \empty *)
+ let l1, vs1 = range_to_base_offset (range_of_rloc s1) in
+ let l2, vs2 = range_to_base_offset (range_of_rloc s2) in
+ p_and
+ (p_equal (a_base l1.loc_t) (a_base l2.loc_t))
+ (Vset.disjoint vs1 vs2)
+
+ let initialized _sigma _l = F.p_true (* todo *)
+ let is_well_formed _ = F.p_true (* todo *)
+ let base_offset _loc = assert false (** TODO *)
+ type domain = Sigma.domain
+ let no_binder = { bind = fun _ f v -> f v }
+ let configure_ia _ = no_binder (* todo *)
+ let hypotheses x = x (* todo *)
+ let frame _sigma = [] (* todo *)
+
+end
+
+
+
+
+(* -------------------------------------------------------------------------- *)
+(* --- EVA Instance --- *)
+(* -------------------------------------------------------------------------- *)
+module Eva =
+struct
+ open Cvalue
+
+ let datatype = "Eva"
+ let configure () =
+ if not (Db.Value.is_computed ()) then
+ Wp_parameters.abort ~current:true
+ "Could not use Eva memory model without a previous run of the analysis.";
+ (fun () -> ())
+
+ module State =
+ struct
+ type t = Model.t
+
+ let bottom = Model.bottom
+ let join = Model.join
+
+ let of_kinstr k = Db.Value.get_state k
+ let of_stmt k = Db.Value.get_stmt_state k
+ let of_kf kf =
+ let state = ref bottom in
+ let vis = object
+ inherit Cil.nopCilVisitor
+ method !vstmt stmt =
+ state := join (of_stmt stmt) !state;
+ Cil.DoChildren
+ end in
+ ignore (Cil.visitCilFunction vis (Kernel_function.get_definition kf));
+ !state
+
+ let pretty = Model.pretty
+ end
+
+ type t = V.t
+ type state = Model.t
+
+ let null = V.inject Base.null Ival.zero
+ let literal ~eid cstr =
+ let b = Base.of_string_exp (Cstring.str_cil ~eid cstr) in
+ Base.id b, V.inject b Ival.zero
+ let cvar x = V.inject (Base.of_varinfo x) Ival.zero
+
+ let field v fd =
+ let bsize = Ctypes.field_offset fd |> Integer.of_int in
+ let offs = Ival.inject_singleton bsize in
+ Cvalue.V.shift offs v
+ let shift v obj t =
+ let bsize = 8 * Ctypes.sizeof_object obj |> Integer.of_int in
+ let offs = match F.repr t with
+ | Logic.Kint z -> Ival.inject_singleton (Integer.mul bsize z)
+ | _ -> Ival.top in
+ Cvalue.V.shift offs v
+ let base_addr v =
+ Cvalue.V.fold_topset_ok
+ (fun b _ v -> Cvalue.V.add b Ival.zero v)
+ v (Cvalue.V.bottom)
+
+ let load state v obj =
+ let bsize = 8 * Ctypes.sizeof_object obj in
+ let bits = Locations.loc_bytes_to_loc_bits v in
+ let int_base = bsize |> Integer.of_int |> Int_Base.inject in
+ let vloc = Locations.make_loc bits int_base in
+ Cvalue.Model.find state vloc
+
+ let domain v =
+ Cvalue.V.fold_topset_ok
+ (fun b _ acc -> b :: acc)
+ v []
+
+ let logic_ival ival = fun x ->
+ (* assert (not (Ival.is_float ival)); (* by integer offsets *) *)
+ match Ival.project_small_set ival with
+ | Some is ->
+ F.p_any
+ (fun i -> F.p_equal x (F.e_bigint i))
+ is
+ | None -> begin
+ match Ival.min_and_max ival with
+ | Some mn, Some mx ->
+ F.p_and
+ (F.p_leq (F.e_bigint mn) x)
+ (F.p_leq x (F.e_bigint mx))
+ | Some mn, None -> F.p_leq (F.e_bigint mn) x
+ | None, Some mx -> F.p_leq x (F.e_bigint mx)
+ | None, None -> F.p_true
+ end
+
+ let offset v = fun x ->
+ let ivals =
+ Cvalue.V.fold_topset_ok
+ (fun _ ival acc -> ival :: acc)
+ v []
+ in
+ F.p_any (fun ival -> logic_ival ival x) ivals
+
+ let pretty = Cvalue.V.pretty
+
+end
diff --git a/src/plugins/wp/MemVal.mli b/src/plugins/wp/MemVal.mli
new file mode 100644
index 0000000000000000000000000000000000000000..db2ffb62c6f98723e2ea7d95b48229b94eb72dc1
--- /dev/null
+++ b/src/plugins/wp/MemVal.mli
@@ -0,0 +1,85 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Lang.F
+
+module type State =
+sig
+ type t (** abstract state **)
+
+ val bottom : t
+ val join : t -> t -> t
+
+ val of_kinstr : Cil_types.kinstr -> t
+ (** [of_stmt stmt] get the abstract state of [stmt]. **)
+ val of_stmt : Cil_types.stmt -> t
+ (** [of_kf kf] get the join state of all [kf]'s statements states **)
+ val of_kf : Cil_types.kernel_function -> t
+
+ val pretty : Format.formatter -> t -> unit
+end
+
+module type Value =
+sig
+ val configure : unit -> WpContext.rollback
+ val datatype : string
+
+ module State : State
+
+ type t (** abstract value **)
+ type state = State.t
+
+ val null : t
+ (** [literal eid cstr] returns the pair of base identifier and abstract value
+ corresponding to the concrete string constant [cstr] of unique expression
+ identifier [eid]. [eid] should be a valid identifier for [cstr]. **)
+ val literal: eid:int -> Cstring.cst -> int * t
+ (** [cvar x] returns the abstract value corresponding to &[x]. **)
+ val cvar : Cil_types.varinfo -> t
+
+ (** [field v fd] returns the value obtained by access to field [fd]
+ from [v]. **)
+ val field : t -> Cil_types.fieldinfo -> t
+ (** [shift v obj k] returns the value obtained by access at an index [k]
+ with type [obj] from [v]. **)
+ val shift : t -> Ctypes.c_object -> term -> t
+ (** [base_addr v] returns the value corresponding to the base address
+ of [v]. **)
+ val base_addr : t -> t
+
+ (** [load s v obj] returns the value at the location given by [v] with type
+ [obj] within the state [s]. **)
+ val load : state -> t -> Ctypes.c_object -> t
+
+ (** [domain v] returns a list of all possible concrete bases of [v]. **)
+ val domain : t -> Base.t list
+ (** [offset v] returns a function which when applied with a term returns
+ a predicate over [v]'s offset. *)
+ val offset : t -> (term -> pred)
+
+ val pretty : Format.formatter -> t -> unit
+end
+
+module Make(V : Value) : Sigs.Model
+
+(** The glue between WP and EVA. **)
+module Eva : Value
diff --git a/src/plugins/wp/share/why3/frama_c_wp/cmath.mlw b/src/plugins/wp/share/why3/frama_c_wp/cmath.mlw
index 495ac75347b5f5e22420e96d2cf7afdf805c27e2..31243afd20dffa3c424f827d8b317fb1d2a12dd9 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cmath.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cmath.mlw
@@ -35,6 +35,14 @@ theory Cmath [@ W:non_conservative_extension:N]
end
+theory IAbs
+ use export int.Abs
+end
+
+theory RAbs
+ use export real.Abs
+end
+
theory Square [@ W:non_conservative_extension:N]
use real.RealInfix
diff --git a/src/plugins/wp/tests/wp_eva/oracle/simple.0.res.oracle b/src/plugins/wp/tests/wp_eva/oracle/simple.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a16c6af1b17c2d65b17c136241a3729c63477320
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/oracle/simple.0.res.oracle
@@ -0,0 +1,79 @@
+[kernel] Parsing tests/wp_eva/simple.c (with preprocessing)
+[eva:alarm] tests/wp_eva/simple.c:25: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:26: Warning:
+ division by zero. assert (int)(*x - 42) ≢ 0;
+[eva:alarm] tests/wp_eva/simple.c:31: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:35: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:41: Warning: assertion got status unknown.
+[wp] Running WP plugin...
+[wp] tests/wp_eva/simple.c:44: Warning:
+ Ignored 'terminates' specification:
+ \false
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function f
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_eva/simple.c, line 25):
+Let x = read_sint32(MVar_z_0, 0).
+Let x_1 = read_sint32(write_sint32(MVar_z_0, 0, 1 + x), 0).
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Assertion 'Reduc' *)
+ Have: (2 <= x) /\ (x <= 1000).
+ (* Else *)
+ Have: x != 41.
+}
+Prove: P_P(x_1).
+
+------------------------------------------------------------
+
+Goal Assertion 'Eva,division_by_zero' (file tests/wp_eva/simple.c, line 26):
+Let x = read_sint32(MVar_z_0, 0).
+Let x_1 = read_sint32(write_sint32(MVar_z_0, 0, 1 + x), 0).
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Assertion 'Reduc' *)
+ Have: (2 <= x) /\ (x <= 1000).
+ (* Else *)
+ Have: x != 41.
+ (* Assertion *)
+ Have: P_P(x_1).
+}
+Prove: to_sint32(x_1 - 42) != 0.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function g
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_eva/simple.c, line 31):
+Let x = read_sint32(MVar_x_0, 0).
+Let x_1 = read_sint32(MVar_y_0, 0).
+Let x_2 = read_sint32(MVar_z_0, 0).
+Let x_3 = read_sint32(write_sint32(MVar_x_0, 0, 1 + x), 0).
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3).
+}
+Prove: P_P(x_1) /\ P_P(x_2) /\ P_P(x_3).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function h
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_eva/simple.c, line 35):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function h2
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_eva/simple.c, line 41):
+Let x = read_sint32(MVar_z_0, 0).
+Let x_1 = read_sint32(write_sint32(MVar_x_0, 0, x), 0).
+Assume { Type: is_sint32(x) /\ is_sint32(x_1). }
+Prove: x_1 = x.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_eva/oracle/simple.1.res.oracle b/src/plugins/wp/tests/wp_eva/oracle/simple.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..06c9c1731bb77d88e397208938b785876af85f17
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/oracle/simple.1.res.oracle
@@ -0,0 +1,84 @@
+[kernel] Parsing tests/wp_eva/simple.c (with preprocessing)
+[eva:alarm] tests/wp_eva/simple.c:25: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:26: Warning:
+ division by zero. assert (int)(*x - 42) ≢ 0;
+[eva:alarm] tests/wp_eva/simple.c:31: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:35: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:41: Warning: assertion got status unknown.
+[wp] Running WP plugin...
+[wp] tests/wp_eva/simple.c:44: Warning:
+ Ignored 'terminates' specification:
+ \false
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function f
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_eva/simple.c, line 25):
+Let x = Mint_0[shift(global(Base_3_0), Offs_0)].
+Let x_1 = 1 + x.
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Assertion 'Reduc' *)
+ Have: (2 <= x) /\ (x <= 1000).
+ (* Else *)
+ Have: x != 41.
+}
+Prove: P_P(x_1).
+
+------------------------------------------------------------
+
+Goal Assertion 'Eva,division_by_zero' (file tests/wp_eva/simple.c, line 26):
+Let x = Mint_0[shift(global(Base_3_0), Offs_0)].
+Let x_1 = 1 + x.
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Assertion 'Reduc' *)
+ Have: (2 <= x) /\ (x <= 1000).
+ (* Else *)
+ Have: x != 41.
+ (* Assertion *)
+ Have: P_P(x_1).
+}
+Prove: to_sint32(x - 41) != 0.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function g
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_eva/simple.c, line 31):
+Let a = shift(global(Base_9_0), Offs_0).
+Let x = Mint_0[a].
+Let x_1 = 1 + x.
+Let m = Mint_0[a <- x_1].
+Let x_2 = m[shift(global(Base_5_0), Offs_1)].
+Let x_3 = m[shift(global(Base_7_0), Offs_2)].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3).
+}
+Prove: P_P(x_1) /\ P_P(x_2) /\ P_P(x_3).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function h
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_eva/simple.c, line 35):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function h2
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_eva/simple.c, line 41):
+Let a = shift(global(Base_16_0), Offs_0).
+Let m = Mint_0[a <- (Base_14_0 = 238) & Mvar_z_0[Offs_1]]
+ [shift(global(Base_18_0), Offs_2) <- 1].
+Let x = m[shift(global(Base_14_0), Offs_1)].
+Let x_1 = m[a].
+Assume { Type: is_sint32(x) /\ is_sint32(x_1). }
+Prove: x_1 = x.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.0.res.oracle b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..96be82db9ffdad6c079c129a01ed837085fa8563
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.0.res.oracle
@@ -0,0 +1,29 @@
+[kernel] Parsing tests/wp_eva/simple.c (with preprocessing)
+[eva:alarm] tests/wp_eva/simple.c:25: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:26: Warning:
+ division by zero. assert (int)(*x - 42) ≢ 0;
+[eva:alarm] tests/wp_eva/simple.c:31: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:35: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:41: Warning: assertion got status unknown.
+# frama-c -wp -wp-model 'Eva1' [...]
+[wp] Running WP plugin...
+[wp] tests/wp_eva/simple.c:44: Warning:
+ Ignored 'terminates' specification:
+ \false
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Alt-Ergo] Goal eva1_f_assert : Timeout (missing cache)
+[wp] [Alt-Ergo] Goal eva1_f_assert_Eva_division_by_zero : Valid (missing cache)
+[wp] [Alt-Ergo] Goal eva1_g_assert : Timeout (missing cache)
+[wp] [Qed] Goal eva1_h_assert : Valid
+[wp] [Alt-Ergo] Goal eva1_h2_assert : Valid (missing cache)
+[wp] Proved goals: 3 / 5
+ Qed: 1
+ Alt-Ergo: 2 (unsuccess: 2)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f - 1 2 50.0%
+ g - - 1 0.0%
+ h 1 - 1 100%
+ h2 - 1 1 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.1.res.oracle b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..446ecb89db8387c9d40d6657c15413446bce0e43
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.1.res.oracle
@@ -0,0 +1,30 @@
+[kernel] Parsing tests/wp_eva/simple.c (with preprocessing)
+[eva:alarm] tests/wp_eva/simple.c:25: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:26: Warning:
+ division by zero. assert (int)(*x - 42) ≢ 0;
+[eva:alarm] tests/wp_eva/simple.c:31: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:35: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:41: Warning: assertion got status unknown.
+# frama-c -wp -wp-model 'Eva2' [...]
+[wp] Running WP plugin...
+[wp] tests/wp_eva/simple.c:44: Warning:
+ Ignored 'terminates' specification:
+ \false
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Alt-Ergo] Goal eva2_f_assert : Timeout (missing cache)
+[wp] [Alt-Ergo] Goal eva2_f_assert_Eva_division_by_zero : Valid (missing cache)
+[wp] [Alt-Ergo] Goal eva2_g_assert : Timeout (missing cache)
+[wp] [Qed] Goal eva2_h_assert : Valid
+[wp] [Alt-Ergo] Goal eva2_h2_assert : Failed
+ [Why3 Error] anomaly: File "src/plugins/wp/ProverWhy3.ml", line 609, characters 9-15: Assertion failed
+[wp] Proved goals: 2 / 5
+ Qed: 1
+ Alt-Ergo: 1 (unsuccess: 2) (failed: 1)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f - 1 2 50.0%
+ g - - 1 0.0%
+ h 1 - 1 100%
+ h2 - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_eva/simple.c b/src/plugins/wp/tests/wp_eva/simple.c
new file mode 100644
index 0000000000000000000000000000000000000000..4de74124ec0da6495455fdcbee98adb3362cc826
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/simple.c
@@ -0,0 +1,52 @@
+/* run.config
+ OPT: -wp-model eva1
+ OPT: -wp-model eva2
+*/
+
+/* run.config_qualif
+ OPT: -wp-model eva1
+ OPT: -wp-model eva2
+*/
+
+#include "__fc_builtin.h"
+
+/*@
+ axiomatic P {
+ predicate P(int x);
+ }
+
+ @*/
+
+int z;
+
+void f (int *x, int *y){
+ if(z==41) return;
+ *x = *x+1;
+ /*@ assert P(*x) && P(*y) && P(z); @*/
+ int r = 1/(*x-42);
+}
+
+void g (int *x, int *y){
+ *x = *x+1;
+ /*@ assert P(*x) && P(*y) && P(z); @*/
+}
+
+void h (int *x, int *y){
+ /*@ assert *x == *y; */
+}
+
+void h2 (int *x, int *y, int *z){
+ *x = *z;
+ *y = 1;
+ /*@ assert *x == *z; */
+}
+
+void main(){
+ int x = Frama_C_interval(2,1000);
+ int y = Frama_C_interval(2,1000);
+ z = Frama_C_interval(2,1000);
+ f(&z,&z);
+ g(&x,&y);
+ h(&x,&x);
+ h2(&x,&y,&z);
+}
diff --git a/src/plugins/wp/tests/wp_eva/test_config b/src/plugins/wp/tests/wp_eva/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..8b6102546cc5b9169aa4d10d195b2ef2f5bab0b3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/test_config
@@ -0,0 +1 @@
+CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope,reduc,wp -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -wp -wp-print -wp-prover none -wp-share ./share -wp-msg-key shell
diff --git a/src/plugins/wp/tests/wp_eva/test_config_qualif b/src/plugins/wp/tests/wp_eva/test_config_qualif
new file mode 100644
index 0000000000000000000000000000000000000000..153e5ddde393c7008e0ff327852ba9b948a25e54
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/test_config_qualif
@@ -0,0 +1,2 @@
+CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope,reduc,wp -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -then -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+OPT:
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index dbb9b389fb6182b69bc1cfcf5ed68d84b3c39a96..8ec961641c448e59acd628407ce46e54f2ea59a5 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -205,7 +205,8 @@ module Model =
* '+raw' no logic variable\n\
* '+ref' by-reference-style pointers detection\n\
* '+nat/+int' natural / machine-integers arithmetics\n\
- * '+real/+float' real / IEEE floating point arithmetics"
+ * '+real/+float' real / IEEE floating point arithmetics\n\
+ * 'Eva' (experimental) based on the results from Eva plugin"
end)
let () = Parameter_customize.set_group wp_model