diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index a31641ec021a157d29ca3fb70e97699d17c8c147..b7ffc10c8528fb799f0efe8f452c69fcb43b000c 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -53,6 +53,7 @@ PLUGIN_CMO:= local_config \
options \
rte \
error \
+ builtins \
misc \
gmpz \
literal_strings \
diff --git a/src/plugins/e-acsl/builtins.ml b/src/plugins/e-acsl/builtins.ml
new file mode 100644
index 0000000000000000000000000000000000000000..cee0c6f68fd3ce2087979e7eb7910815a008869f
--- /dev/null
+++ b/src/plugins/e-acsl/builtins.ml
@@ -0,0 +1,88 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2016 *)
+(* 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 license/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(* store the E-ACSL built-ins by associating a varinfo to its name. *)
+let tbl
+ : varinfo ref Datatype.String.Hashtbl.t
+ = Datatype.String.Hashtbl.create 7
+
+let mem = Datatype.String.Hashtbl.mem tbl
+let find s = !(Datatype.String.Hashtbl.find tbl s)
+
+(* the initial varinfos in the table belong to the original project. At the time
+ of code generation, we need to update them to the ones of the new project. *)
+let update s vi =
+ try
+ let vref = Datatype.String.Hashtbl.find tbl s in
+ vref := vi
+ with Not_found ->
+ ()
+
+(* add [vi] in the built-in table if it is an E-ACSL built-in which is not
+ [already] registered. *)
+let add_builtin vi already =
+ if not already then
+ let bl_name = vi.vname in
+ if Options.Builtins.mem bl_name then
+ match Cil.unrollType vi.vtype with
+ | TFun(ret_typ, param_typs, _, _) ->
+ let bl_type = match Cil.unrollType ret_typ with
+ | TVoid _ ->
+ Options.fatal
+ "Expecting a non-void return type for the E-ACSL built-in %s"
+ bl_name
+ | _ -> Some (Ctype ret_typ)
+ in
+ let bl_profile = match param_typs with
+ | None -> []
+ | Some l -> List.map (fun (name, ty, _) -> (name, Ctype ty)) l
+ in
+ let bli =
+ { bl_name; bl_labels = []; bl_params = []; bl_type; bl_profile }
+ in
+ (* add the built-in locally as an E-ACSL built-in, but also as a new
+ Frama-C built-in. This way, the annotated C code will be parsed when
+ using it *)
+ Logic_builtin.add bli;
+ Datatype.String.Hashtbl.add tbl bl_name (ref vi)
+ | _ ->
+ Options.fatal "Expecting a function type for the E-ACSL built-in %s"
+ bl_name
+
+let init () =
+ Datatype.String.Hashtbl.clear tbl;
+ if not (Options.Builtins.is_empty ()) then
+ (* every time a new global is visited by [Cabs2cil], check if we must add it
+ as a new E-ACSL built-in *)
+ Cabs2cil.register_new_global_hook add_builtin
+
+(* Initialization of the database must be done before anything else, but parsing
+ the command line *)
+let () = Cmdline.run_after_configuring_stage init
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)
diff --git a/src/plugins/e-acsl/builtins.mli b/src/plugins/e-acsl/builtins.mli
new file mode 100644
index 0000000000000000000000000000000000000000..cdb585ba30847cde0e6eadab7f507436a76fff70
--- /dev/null
+++ b/src/plugins/e-acsl/builtins.mli
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2016 *)
+(* 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 license/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** E-ACSL built-in database. *)
+
+val mem: string -> bool
+(** @return true ifl the given function name is an E-ACSL built-in *)
+
+val find: string -> Cil_types.varinfo
+(** Get the varinfo corresponding to the given E-ACSL built-in name.
+ @raise Not_found if it is not a built-in *)
+
+val update: string -> Cil_types.varinfo -> unit
+(** If the given name is an E-ACSL built-in, change its old varinfo by the given
+ new one. *)
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index e77b3ffebb5989cf4feeca096bcd9f92a95332d4..7e853c2a4cf128d3a44b961783239ad82aee292b 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,7 +15,6 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
-=======
-* E-ACSL [2016/07/21] Enable reporting of stack traces during assertion
failures in instrumented programs.
-* E-ACSL [2016/07/13] Add an e-acsl-gcc.sh option (--print--models)
@@ -26,14 +25,16 @@
with E-ACSL runtime library.
-* E-ACSL [2016/07/01] Add custom implementation of malloc for use with
E-ACSL runtime library (via jemalloc library).
--* E-ACSL [2016/05/22] Add an e-acsl-gcc.sh option (--rte|-a) allowing to
- annotate the source program with memory-safety assertions prior to
- instrumentation.
->>>>>>> Changelog updates
+- E-ACSL [2016/05/31] New option -e-acsl-builtins which allows to
+ declare pure C functions which can be used in logic
+ function application.
- E-ACSL [2016/05/23] Re-implementation of the type system which
improves the efficiency of the generated code over integers.
-* E-ACSL [2016/05/23] Fix bug #2191 about complicate structs and
literate string.
+-* E-ACSL [2016/05/22] Add an e-acsl-gcc.sh option (--rte|-a) allowing to
+ annotate the source program with memory-safety assertions prior
+ to instrumentation.
-* E-ACSL [2016/05/23] Fix bug #1395 about recursive functions.
-* E-ACSL [2016/04/07] Fix 'make install' when executed within Frama-C.
-* E-ACSL [2016/03/31] Improve performance of Patricia Trie memory model.
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 1704470ba4b6d46a6d8329d5623fd311e74e8afd..aabfe55198b1d4374687278fb5a4a71b1bac5429 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -52,12 +52,14 @@ let reset () = Datatype.String.Hashtbl.clear library_functions
exception Unregistered_library_function of string
let mk_call ~loc ?result fname args =
- let vi =
+ let vi =
try Datatype.String.Hashtbl.find library_functions fname
with Not_found ->
- (* could not happen in normal mode, but coud be raised when E-ACSL is used
- as a library *)
- raise (Unregistered_library_function fname)
+ try Builtins.find fname
+ with Not_found ->
+ (* could not happen in normal mode, but coud be raised when E-ACSL is
+ used as a library *)
+ raise (Unregistered_library_function fname)
in
let f = Cil.evar ~loc vi in
vi.vreferenced <- true;
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index dbc11e59db77a31e3d42e65d56d078a7605c1836..86082642f191c8f6d0984224c43e9e7f95ffea46 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -31,7 +31,7 @@ open Cil_datatype
exception Unregistered_library_function of string
val mk_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
-(** Call an E-ACSL library function.
+(** Call an E-ACSL library function or an E-ACSL built-in.
@raise Unregistered_library_function if the given string does not represent
such a function or if these functions were never registered (only possible
when using E-ACSL through its API. *)
diff --git a/src/plugins/e-acsl/options.ml b/src/plugins/e-acsl/options.ml
index 5c1abcf44202ff3c54df5a917622a676db6523f0..1435b438bbb6e21a1a245fffaefdb0ca8a76a351 100644
--- a/src/plugins/e-acsl/options.ml
+++ b/src/plugins/e-acsl/options.ml
@@ -84,6 +84,14 @@ module Full_mmodel =
let help = "maximal memory-related instrumentation"
end)
+module Builtins =
+ String_set
+ (struct
+ let option_name = "-e-acsl-builtins"
+ let arg_name = ""
+ let help = "C functions which can be used in the E-ACSL specifications"
+ end)
+
let () = Parameter_customize.set_group help
module Version =
False
diff --git a/src/plugins/e-acsl/options.mli b/src/plugins/e-acsl/options.mli
index 9890815a8d1ff06c6523aeefbf87e888bb033b51..e3c10213e297f69a43ae5fa9fd07f6a401e8ea4b 100644
--- a/src/plugins/e-acsl/options.mli
+++ b/src/plugins/e-acsl/options.mli
@@ -29,6 +29,7 @@ module Prepare: Parameter_sig.Bool
module Gmp_only: Parameter_sig.Bool
module Full_mmodel: Parameter_sig.Bool
module Project_name: Parameter_sig.String
+module Builtins: Parameter_sig.String_set
val must_visit: unit -> bool
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 4cb1ce8ed9a2197274f1b1d2c422825b88f6e596..7a36bf78abedb29314766f173bf68a88f3749fb8 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -430,7 +430,44 @@ and context_insensitive_term_to_exp kf env t =
| TStartOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
Cil.mkAddrOrStartOf ~loc lv, env, false, "startof"
- | Tapp _ -> not_yet env "applying logic function"
+ | Tapp(li, [], args) when Builtins.mem li.l_var_info.lv_name ->
+ (* E-ACSL built-in function call *)
+ let fname = li.l_var_info.lv_name in
+ let convert_ty name = function
+ | Ctype ty -> ty
+ | lty ->
+ Options.fatal "[Tapp] expected C type for %s in %s. Got %a."
+ name
+ fname
+ Printer.pp_logic_type lty
+ in
+ let args, env = (* args computed in the reverse order *)
+ try
+ List.fold_left
+ (fun (l, env) a ->
+ let e, env = term_to_exp kf env a in
+ e :: l, env)
+ ([], env)
+ args
+ with Invalid_argument _ ->
+ Options.fatal "[Tapp] unexpected number of arguments when calling %s"
+ fname
+ in
+ (* build the varinfo (as an expression) which stores the result of the
+ function call. *)
+ let _, e, env =
+ Env.new_var
+ ~loc
+ ~name:(fname ^ "_app")
+ env
+ (Some t)
+ (convert_ty "result" (Extlib.the li.l_type))
+ (fun vi _ ->
+ [ Misc.mk_call ~loc ~result:(Cil.var vi) fname (List.rev args) ])
+ in
+ e, env, false, "app"
+ | Tapp _ ->
+ not_yet env "applying logic function"
| Tlambda _ -> not_yet env "functional"
| TDataCons _ -> not_yet env "constructor"
| Tif(t1, t2, t3) ->
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 1475fe087f00b12769a368ff3265caa6b8d5e77a..548386eb6d308f714fbbdfb3b9b6db344a10fec5 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -162,6 +162,15 @@ end
(** {2 Coercion rules} *)
(******************************************************************************)
+let ty_of_logic_ty = function
+ | Linteger -> Gmp
+ | Ctype ty -> (match Cil.unrollType ty with
+ | TInt(ik, _) -> C_type ik
+ | _ -> Other)
+ | Lreal | Larrow _ -> Other
+ | Ltype _ -> Error.not_yet "user-defined logic type"
+ | Lvar _ -> Error.not_yet "type variable"
+
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)
let ty_of_interv ?ctx i =
@@ -217,7 +226,7 @@ let rec type_term ~force ?ctx t =
(* this pattern matching implements the formal rules of the JFLA's paper
(and of course also covers the missing cases). Also enforce the invariant
that every subterm is typed, even if it is not an integer. *)
- match t.term_node with
+ match t.term_node with
| TConst (Integer _ | LChr _ | LEnum _)
| TSizeOf _
| TSizeOfStr _
@@ -401,7 +410,16 @@ let rec type_term ~force ?ctx t =
ignore (type_term ~force:true ~ctx:(size_t ()) t2);
dup Other
- | Tapp (_,_,_) -> Error.not_yet "logic function application"
+ | Tapp(li, _, args) ->
+ let typ_arg lvi arg =
+ let ctx = ty_of_logic_ty lvi.lv_type in
+ ignore (type_term ~force:true ~ctx arg)
+ in
+ List.iter2 typ_arg li.l_profile args;
+ (* [li.l_type is [None] for predicate only: not possible here.
+ Thus using [Extlib.the] is fine *)
+ dup (ty_of_logic_ty (Extlib.the li.l_type))
+
| Tunion _ -> Error.not_yet "tset union"
| Tinter _ -> Error.not_yet "tset intersection"
| Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 76f6840b162814830308c023a5df791aa9c8120a..135692ddfbd8cf6cdd8d6b019bb79a554d56c4f6 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -298,11 +298,13 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
when Misc.is_library_loc vi.vdecl ->
if generate then
Cil.JustCopyPost
- (fun l ->
- Misc.register_library_function (Cil.get_varinfo self#behavior vi);
+ (fun l ->
+ let new_vi = Cil.get_varinfo self#behavior vi in
+ Misc.register_library_function new_vi;
+ Builtins.update vi.vname new_vi;
l)
else begin
- Misc.register_library_function vi;
+ Misc.register_library_function vi;
Cil.SkipChildren
end
| GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
@@ -316,6 +318,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
vi.vghost <- false; ()
| GFun({ svar = vi } as fundec, _) ->
vi.vghost <- false;
+ Builtins.update vi.vname vi;
(* remember that we have to remove the main later (see method
[vfile]) *)
if vi.vorig_name = Kernel.MainFunction.get () then