From b3aefd555accd66a8a3ced22b9c26df8946e874b Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 28 Aug 2019 17:59:54 +0200
Subject: [PATCH] [archi] add source subdirectories
---
src/plugins/e-acsl/.gitignore | 1 +
src/plugins/e-acsl/Makefile.in | 114 ++++++++++++------
.../e-acsl/src/{ => analyses}/exit_points.ml | 0
.../e-acsl/src/{ => analyses}/exit_points.mli | 0
.../e-acsl/src/{ => analyses}/interval.ml | 6 +-
.../e-acsl/src/{ => analyses}/interval.mli | 2 +-
.../src/{ => analyses}/literal_strings.ml | 0
.../src/{ => analyses}/literal_strings.mli | 0
.../e-acsl/src/{ => analyses}/lscope.ml | 0
.../e-acsl/src/{ => analyses}/lscope.mli | 0
.../src/{ => analyses}/mmodel_analysis.ml | 0
.../src/{ => analyses}/mmodel_analysis.mli | 0
src/plugins/e-acsl/src/{ => analyses}/rte.ml | 0
src/plugins/e-acsl/src/{ => analyses}/rte.mli | 0
.../e-acsl/src/{ => analyses}/typing.ml | 8 +-
.../e-acsl/src/{ => analyses}/typing.mli | 2 +-
.../{ => code_generator}/at_with_lscope.ml | 8 +-
.../{ => code_generator}/at_with_lscope.mli | 8 +-
.../e-acsl/src/{ => code_generator}/env.ml | 70 +++--------
.../e-acsl/src/{ => code_generator}/env.mli | 15 +--
.../e-acsl/src/{ => code_generator}/gmp.ml | 109 ++---------------
.../e-acsl/src/{ => code_generator}/gmp.mli | 30 +----
.../e-acsl/src/{ => code_generator}/label.ml | 0
.../e-acsl/src/{ => code_generator}/label.mli | 0
.../{ => code_generator}/logic_functions.ml | 12 +-
.../{ => code_generator}/logic_functions.mli | 6 +
.../e-acsl/src/{ => code_generator}/loops.ml | 0
.../e-acsl/src/{ => code_generator}/loops.mli | 0
.../{ => code_generator}/mmodel_translate.ml | 2 +-
.../{ => code_generator}/mmodel_translate.mli | 0
.../src/{ => code_generator}/quantif.ml | 0
.../src/{ => code_generator}/quantif.mli | 0
.../e-acsl/src/{ => code_generator}/real.ml | 10 +-
.../e-acsl/src/{ => code_generator}/real.mli | 6 +
.../src/{ => code_generator}/temporal.ml | 23 ++--
.../src/{ => code_generator}/temporal.mli | 12 +-
.../src/{ => code_generator}/translate.ml | 28 ++---
.../src/{ => code_generator}/translate.mli | 2 +-
.../e-acsl/src/{ => code_generator}/visit.ml | 4 +-
.../e-acsl/src/{ => code_generator}/visit.mli | 2 +-
.../e-acsl/src/{ => libraries}/builtins.ml | 0
.../e-acsl/src/{ => libraries}/builtins.mli | 0
.../e-acsl/src/{ => libraries}/error.ml | 0
.../e-acsl/src/{ => libraries}/error.mli | 0
.../e-acsl/src/{ => libraries}/functions.ml | 0
.../e-acsl/src/{ => libraries}/functions.mli | 0
src/plugins/e-acsl/src/libraries/gmp_types.ml | 114 ++++++++++++++++++
.../e-acsl/src/libraries/gmp_types.mli | 55 +++++++++
.../e-acsl/src/{ => libraries}/misc.ml | 0
.../e-acsl/src/{ => libraries}/misc.mli | 0
src/plugins/e-acsl/src/libraries/varname.ml | 52 ++++++++
src/plugins/e-acsl/src/libraries/varname.mli | 41 +++++++
src/plugins/e-acsl/src/main.ml | 7 +-
.../dup_functions.ml | 4 +-
.../dup_functions.mli | 0
.../{ => project_initializer}/keep_status.ml | 0
.../{ => project_initializer}/keep_status.mli | 0
.../{ => project_initializer}/prepare_ast.ml | 8 +-
.../{ => project_initializer}/prepare_ast.mli | 6 +
59 files changed, 479 insertions(+), 288 deletions(-)
rename src/plugins/e-acsl/src/{ => analyses}/exit_points.ml (100%)
rename src/plugins/e-acsl/src/{ => analyses}/exit_points.mli (100%)
rename src/plugins/e-acsl/src/{ => analyses}/interval.ml (99%)
rename src/plugins/e-acsl/src/{ => analyses}/interval.mli (99%)
rename src/plugins/e-acsl/src/{ => analyses}/literal_strings.ml (100%)
rename src/plugins/e-acsl/src/{ => analyses}/literal_strings.mli (100%)
rename src/plugins/e-acsl/src/{ => analyses}/lscope.ml (100%)
rename src/plugins/e-acsl/src/{ => analyses}/lscope.mli (100%)
rename src/plugins/e-acsl/src/{ => analyses}/mmodel_analysis.ml (100%)
rename src/plugins/e-acsl/src/{ => analyses}/mmodel_analysis.mli (100%)
rename src/plugins/e-acsl/src/{ => analyses}/rte.ml (100%)
rename src/plugins/e-acsl/src/{ => analyses}/rte.mli (100%)
rename src/plugins/e-acsl/src/{ => analyses}/typing.ml (99%)
rename src/plugins/e-acsl/src/{ => analyses}/typing.mli (99%)
rename src/plugins/e-acsl/src/{ => code_generator}/at_with_lscope.ml (99%)
rename src/plugins/e-acsl/src/{ => code_generator}/at_with_lscope.mli (96%)
rename src/plugins/e-acsl/src/{ => code_generator}/env.ml (92%)
rename src/plugins/e-acsl/src/{ => code_generator}/env.mli (96%)
rename src/plugins/e-acsl/src/{ => code_generator}/gmp.ml (59%)
rename src/plugins/e-acsl/src/{ => code_generator}/gmp.mli (71%)
rename src/plugins/e-acsl/src/{ => code_generator}/label.ml (100%)
rename src/plugins/e-acsl/src/{ => code_generator}/label.mli (100%)
rename src/plugins/e-acsl/src/{ => code_generator}/logic_functions.ml (98%)
rename src/plugins/e-acsl/src/{ => code_generator}/logic_functions.mli (98%)
rename src/plugins/e-acsl/src/{ => code_generator}/loops.ml (100%)
rename src/plugins/e-acsl/src/{ => code_generator}/loops.mli (100%)
rename src/plugins/e-acsl/src/{ => code_generator}/mmodel_translate.ml (99%)
rename src/plugins/e-acsl/src/{ => code_generator}/mmodel_translate.mli (100%)
rename src/plugins/e-acsl/src/{ => code_generator}/quantif.ml (100%)
rename src/plugins/e-acsl/src/{ => code_generator}/quantif.mli (100%)
rename src/plugins/e-acsl/src/{ => code_generator}/real.ml (98%)
rename src/plugins/e-acsl/src/{ => code_generator}/real.mli (98%)
rename src/plugins/e-acsl/src/{ => code_generator}/temporal.ml (98%)
rename src/plugins/e-acsl/src/{ => code_generator}/temporal.mli (93%)
rename src/plugins/e-acsl/src/{ => code_generator}/translate.ml (98%)
rename src/plugins/e-acsl/src/{ => code_generator}/translate.mli (98%)
rename src/plugins/e-acsl/src/{ => code_generator}/visit.ml (99%)
rename src/plugins/e-acsl/src/{ => code_generator}/visit.mli (98%)
rename src/plugins/e-acsl/src/{ => libraries}/builtins.ml (100%)
rename src/plugins/e-acsl/src/{ => libraries}/builtins.mli (100%)
rename src/plugins/e-acsl/src/{ => libraries}/error.ml (100%)
rename src/plugins/e-acsl/src/{ => libraries}/error.mli (100%)
rename src/plugins/e-acsl/src/{ => libraries}/functions.ml (100%)
rename src/plugins/e-acsl/src/{ => libraries}/functions.mli (100%)
create mode 100644 src/plugins/e-acsl/src/libraries/gmp_types.ml
create mode 100644 src/plugins/e-acsl/src/libraries/gmp_types.mli
rename src/plugins/e-acsl/src/{ => libraries}/misc.ml (100%)
rename src/plugins/e-acsl/src/{ => libraries}/misc.mli (100%)
create mode 100644 src/plugins/e-acsl/src/libraries/varname.ml
create mode 100644 src/plugins/e-acsl/src/libraries/varname.mli
rename src/plugins/e-acsl/src/{ => project_initializer}/dup_functions.ml (99%)
rename src/plugins/e-acsl/src/{ => project_initializer}/dup_functions.mli (100%)
rename src/plugins/e-acsl/src/{ => project_initializer}/keep_status.ml (100%)
rename src/plugins/e-acsl/src/{ => project_initializer}/keep_status.mli (100%)
rename src/plugins/e-acsl/src/{ => project_initializer}/prepare_ast.ml (98%)
rename src/plugins/e-acsl/src/{ => project_initializer}/prepare_ast.mli (96%)
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 96261e25880..dbaf48cb545 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -86,3 +86,4 @@ lib/libeacsl-rtl-segment.a
lib/libeacsl-rtl-bittree-dbg.a
lib/libeacsl-rtl-segment-dbg.a
tests/csrv14/*
+src/local_config.ml
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 5803570dd00..753d292e132 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -49,43 +49,75 @@ endif
CAT?=cat
SED?=sed
+###################
+# Plug-in sources #
+###################
+
+# libraries
+SRC_LIBRARIES:= \
+ error \
+ builtins \
+ functions \
+ misc \
+ gmp_types \
+ varname
+SRC_LIBRARIES:=$(addprefix src/libraries/, $(SRC_LIBRARIES))
+
+# analyses
+SRC_ANALYSES:= \
+ rte \
+ literal_strings \
+ mmodel_analysis \
+ exit_points \
+ lscope \
+ interval \
+ typing
+SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
+
+# project initializer
+SRC_PROJECT_INITIALIZER:= \
+ keep_status \
+ prepare_ast \
+ dup_functions
+SRC_PROJECT_INITIALIZER:=\
+ $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
+
+# code generator
+SRC_CODE_GENERATOR:= \
+ gmp \
+ label \
+ env \
+ real \
+ loops \
+ quantif \
+ at_with_lscope \
+ mmodel_translate \
+ logic_functions \
+ translate \
+ temporal \
+ visit
+SRC_CODE_GENERATOR:=$(addprefix src/code_generator/, $(SRC_CODE_GENERATOR))
+
#########################
# Plug-in configuration #
#########################
PLUGIN_DIR ?=.
-PLUGIN_EXTRA_DIRS:=src
+PLUGIN_EXTRA_DIRS:=\
+ src \
+ src/libraries \
+ src/analyses \
+ src/project_initializer \
+ src/code_generator
PLUGIN_ENABLE:=@ENABLE_E_ACSL@
PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@
PLUGIN_NAME:=E_ACSL
PLUGIN_CMO:= src/local_config \
src/options \
- src/rte \
- src/error \
- src/builtins \
- src/functions \
- src/misc \
- src/gmp \
- src/literal_strings \
- src/mmodel_analysis \
- src/exit_points \
- src/label \
- src/lscope \
- src/env \
- src/real \
- src/keep_status \
- src/dup_functions \
- src/interval \
- src/typing \
- src/loops \
- src/quantif \
- src/at_with_lscope \
- src/mmodel_translate \
- src/logic_functions \
- src/translate \
- src/temporal \
- src/prepare_ast \
- src/visit \
+ $(SRC_LIBRARIES) \
+ $(SRC_ANALYSES) \
+ $(SRC_PROJECT_INITIALIZER) \
+ $(SRC_CODE_GENERATOR) \
src/main
PLUGIN_HAS_MLI:=yes
@@ -95,9 +127,9 @@ PLUGIN_DISTRIBUTED:=yes
EACSL_PLUGIN_DIR:=$(PLUGIN_DIR)
# Suppress a spurious warning with OCaml >= 4.04.0
-$(EACSL_PLUGIN_DIR)/src/mmodel_analysis.cmo \
-$(EACSL_PLUGIN_DIR)/src/mmodel_analysis.cmi: E_ACSL_BFLAGS+= -w -60
-$(EACSL_PLUGIN_DIR)/src/mmodel_analysis.cmx: E_ACSL_OFLAGS+= -w -60
+$(EACSL_PLUGIN_DIR)/src/analyses/mmodel_analysis.cmo \
+$(EACSL_PLUGIN_DIR)/src/analyses/mmodel_analysis.cmi: E_ACSL_BFLAGS+= -w -60
+$(EACSL_PLUGIN_DIR)/src/analyses/mmodel_analysis.cmx: E_ACSL_OFLAGS+= -w -60
###############
# Local Flags #
@@ -173,6 +205,9 @@ E_ACSL_DEFAULT_TESTS: \
$(EACSL_PLUGIN_DIR)/tests/print.cmo
clean::
+ for d in $(E_ACSL_EXTRA_DIRS); do \
+ $(RM) $$d/*~; \
+ done
$(PRINT_RM) cleaning generated test files
$(RM) $(E_ACSL_DIR)/tests/*.cm* $(E_ACSL_DIR)/tests/*.o
$(RM) $(E_ACSL_DIR)/tests/test_config
@@ -295,10 +330,13 @@ PLUGIN_HEADER_EXCEPTIONS:=
PLUGIN_DISTRIB_TESTS:= $(EACSL_DISTRIB_TESTS)
# for e-csl-distrib target:
-EACSL_OCAML_FILES = E_ACSL.mli src/*.mli \
- $(patsubst $(EACSL_PLUGIN_DIR)/%, %, \
- $(filter-out $(wildcard $(EACSL_PLUGIN_DIR)/src/*local_config.ml), \
- $(wildcard $(EACSL_PLUGIN_DIR)/src/*.ml)))
+EACSL_OCAML_FILES = \
+ E_ACSL.mli \
+ src/*.mli src/*/*.mli \
+ $(patsubst $(EACSL_PLUGIN_DIR)/%, %, \
+ $(filter-out $(wildcard $(EACSL_PLUGIN_DIR)/src/*local_config.ml), \
+ $(wildcard $(EACSL_PLUGIN_DIR)/src/*.ml) \
+ $(EACSL_PLUGIN_DIR/src/*/*.ml))
EACSL_DISTRIB_FILES = \
$(patsubst $(EACSL_PLUGIN_DIR)/%,%,\
@@ -372,8 +410,12 @@ EACSL_SHARE_BARE= share/e-acsl/*.[ch] share/e-acsl/*/*.[ch]
EACSL_SHARE=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_SHARE_BARE))
EACSL_CEA_SHARE=$(filter-out $(EACSL_SPARETIMELABS), $(wildcard $(EACSL_SHARE)))
-EACSL_CEA_LGPL_BARE= src/*.ml src/*.mli E_ACSL.mli Makefile.in configure.ac \
- scripts/*.sh tests/print.ml man/e-acsl-gcc.sh.1
+EACSL_CEA_LGPL_BARE= src/*.ml src/*/*.ml src/*.mli src/*/*.mli \
+ E_ACSL.mli \
+ Makefile.in configure.ac \
+ scripts/*.sh \
+ tests/print.ml \
+ man/e-acsl-gcc.sh.1
EACSL_CEA_LGPL=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_CEA_LGPL_BARE)) \
$(EACSL_CEA_SHARE)
diff --git a/src/plugins/e-acsl/src/exit_points.ml b/src/plugins/e-acsl/src/analyses/exit_points.ml
similarity index 100%
rename from src/plugins/e-acsl/src/exit_points.ml
rename to src/plugins/e-acsl/src/analyses/exit_points.ml
diff --git a/src/plugins/e-acsl/src/exit_points.mli b/src/plugins/e-acsl/src/analyses/exit_points.mli
similarity index 100%
rename from src/plugins/e-acsl/src/exit_points.mli
rename to src/plugins/e-acsl/src/analyses/exit_points.mli
diff --git a/src/plugins/e-acsl/src/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
similarity index 99%
rename from src/plugins/e-acsl/src/interval.ml
rename to src/plugins/e-acsl/src/analyses/interval.ml
index bdb28cf0ffa..948c0da9b9b 100644
--- a/src/plugins/e-acsl/src/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -220,11 +220,11 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
ival l u
| TEnum(enuminfo, _) ->
interv_of_typ (TInt(enuminfo.ekind, []))
- | _ when Gmp.Z.is_t ty ->
+ | _ when Gmp_types.Z.is_t ty ->
top_ival
| TFloat (k, _) ->
Float(k, None)
- | _ when Real.is_t ty ->
+ | _ when Gmp_types.Q.is_t ty ->
Rational (* only rationals are implemented *)
| TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ ->
Nan
@@ -593,6 +593,6 @@ include D
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/interval.mli b/src/plugins/e-acsl/src/analyses/interval.mli
similarity index 99%
rename from src/plugins/e-acsl/src/interval.mli
rename to src/plugins/e-acsl/src/analyses/interval.mli
index 4260d80f8a3..332ba399ba8 100644
--- a/src/plugins/e-acsl/src/interval.mli
+++ b/src/plugins/e-acsl/src/analyses/interval.mli
@@ -104,6 +104,6 @@ val infer: Cil_types.term -> t
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/literal_strings.ml b/src/plugins/e-acsl/src/analyses/literal_strings.ml
similarity index 100%
rename from src/plugins/e-acsl/src/literal_strings.ml
rename to src/plugins/e-acsl/src/analyses/literal_strings.ml
diff --git a/src/plugins/e-acsl/src/literal_strings.mli b/src/plugins/e-acsl/src/analyses/literal_strings.mli
similarity index 100%
rename from src/plugins/e-acsl/src/literal_strings.mli
rename to src/plugins/e-acsl/src/analyses/literal_strings.mli
diff --git a/src/plugins/e-acsl/src/lscope.ml b/src/plugins/e-acsl/src/analyses/lscope.ml
similarity index 100%
rename from src/plugins/e-acsl/src/lscope.ml
rename to src/plugins/e-acsl/src/analyses/lscope.ml
diff --git a/src/plugins/e-acsl/src/lscope.mli b/src/plugins/e-acsl/src/analyses/lscope.mli
similarity index 100%
rename from src/plugins/e-acsl/src/lscope.mli
rename to src/plugins/e-acsl/src/analyses/lscope.mli
diff --git a/src/plugins/e-acsl/src/mmodel_analysis.ml b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
similarity index 100%
rename from src/plugins/e-acsl/src/mmodel_analysis.ml
rename to src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
diff --git a/src/plugins/e-acsl/src/mmodel_analysis.mli b/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
similarity index 100%
rename from src/plugins/e-acsl/src/mmodel_analysis.mli
rename to src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
diff --git a/src/plugins/e-acsl/src/rte.ml b/src/plugins/e-acsl/src/analyses/rte.ml
similarity index 100%
rename from src/plugins/e-acsl/src/rte.ml
rename to src/plugins/e-acsl/src/analyses/rte.ml
diff --git a/src/plugins/e-acsl/src/rte.mli b/src/plugins/e-acsl/src/analyses/rte.mli
similarity index 100%
rename from src/plugins/e-acsl/src/rte.mli
rename to src/plugins/e-acsl/src/analyses/rte.mli
diff --git a/src/plugins/e-acsl/src/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
similarity index 99%
rename from src/plugins/e-acsl/src/typing.ml
rename to src/plugins/e-acsl/src/analyses/typing.ml
index 2e380924517..4d1ea2ba27e 100644
--- a/src/plugins/e-acsl/src/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -151,15 +151,15 @@ exception Not_a_number
let typ_of_number_ty = function
| C_integer ik -> TInt(ik, [])
| C_float fk -> TFloat(fk, [])
- | Gmpz -> Gmp.Z.t ()
+ | Gmpz -> Gmp_types.Z.t ()
(* for the time being, no reals but rationals instead *)
- | Rational -> Real.t ()
+ | Rational -> Gmp_types.Q.t ()
| Real -> Error.not_yet "real number type"
| Nan -> raise Not_a_number
let typ_of_lty = function
| Ctype cty -> cty
- | Linteger -> Gmp.Z.t ()
+ | Linteger -> Gmp_types.Z.t ()
| Lreal -> Error.not_yet "real type"
| Ltype _ | Lvar _ | Larrow _ -> Options.fatal "unexpected logic type"
@@ -755,6 +755,6 @@ module Datatype = D
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
similarity index 99%
rename from src/plugins/e-acsl/src/typing.mli
rename to src/plugins/e-acsl/src/analyses/typing.mli
index 29be0fa5d4e..dfef352dee0 100644
--- a/src/plugins/e-acsl/src/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -160,6 +160,6 @@ val compute_quantif_guards_ref
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/at_with_lscope.ml b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
similarity index 99%
rename from src/plugins/e-acsl/src/at_with_lscope.ml
rename to src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
index af7ff2a1f0c..d34af61bc03 100644
--- a/src/plugins/e-acsl/src/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -242,7 +242,7 @@ let to_exp ~loc kf env pot label =
let vi_at, e_at, env = Env.new_var
~loc
~name:"at"
- ~scope:Env.Function
+ ~scope:Varname.Function
env
None
ty_ptr
@@ -341,3 +341,9 @@ let to_exp ~loc kf env pot label =
let lval_at_index, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e = Cil.new_exp ~loc (Lval lval_at_index) in
e, env
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/at_with_lscope.mli b/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
similarity index 96%
rename from src/plugins/e-acsl/src/at_with_lscope.mli
rename to src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
index 3a090999252..70ad6f00677 100644
--- a/src/plugins/e-acsl/src/at_with_lscope.mli
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
@@ -66,4 +66,10 @@ val predicate_to_exp_ref:
(kernel_function -> Env.t -> predicate -> exp * Env.t) ref
val term_to_exp_ref:
- (kernel_function -> Env.t -> term -> exp * Env.t) ref
\ No newline at end of file
+ (kernel_function -> Env.t -> term -> exp * Env.t) ref
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
similarity index 92%
rename from src/plugins/e-acsl/src/env.ml
rename to src/plugins/e-acsl/src/code_generator/env.ml
index 2875f8b2248..c9d441ac976 100644
--- a/src/plugins/e-acsl/src/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -29,11 +29,6 @@ type localized_scope =
| LFunction of kernel_function
| LLocal_block of kernel_function
-type scope =
- | Global
- | Function
- | Local_block
-
type mp_tbl = {
new_exps: (varinfo * exp) Term.Map.t;
(* generated mp variables as exp from terms *)
@@ -76,33 +71,6 @@ type t = {
(* counter used when generating variables *)
}
-module Varname: sig
- val get: scope:scope -> string -> string
- val clear: unit -> unit
-end = struct
-
- module H = Datatype.String.Hashtbl
- let tbl = H.create 7
- let globals = H.create 7
-
- let get ~scope s =
- let _, u =
- Extlib.make_unique_name
- (fun s -> H.mem tbl s || H.mem globals s)
- ~sep:"_"
- s
- in
- let add = match scope with
- | Global -> H.add globals
- | Function | Local_block -> H.add tbl
- in
- add u ();
- u
-
- let clear () = H.clear tbl
-
-end
-
let empty_block =
{ new_block_vars = [];
new_stmts = [];
@@ -195,13 +163,13 @@ let generate_rte env =
(* eta-expansion required for typing generalisation *)
let acc_list_rev acc l = List.fold_left (fun acc x -> x :: acc) acc l
-let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
+let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env t ty mk_stmts =
let local_env, tl_env = top env in
let local_block = local_env.block_info in
- let is_z_t = Gmp.Z.is_t ty in
- if is_z_t then Gmp.Z.is_now_referenced ();
- let is_q_t = Gmp.Q.is_t ty in
- if is_q_t then Gmp.Q.is_now_referenced ();
+ let is_z_t = Gmp_types.Z.is_t ty in
+ if is_z_t then Gmp_types.Z.is_now_referenced ();
+ let is_q_t = Gmp_types.Q.is_t ty in
+ if is_q_t then Gmp_types.Q.is_now_referenced ();
let n = succ env.cpt in
let v =
Cil.makeVarinfo
@@ -214,17 +182,17 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
in
v.vreferenced <- true;
let lscope = match scope with
- | Global -> LGlobal
- | Function -> LFunction (Extlib.the (current_kf env))
- | Local_block -> LLocal_block (Extlib.the (current_kf env))
+ | Varname.Global -> LGlobal
+ | Varname.Function -> LFunction (Extlib.the (current_kf env))
+ | Varname.Block -> LLocal_block (Extlib.the (current_kf env))
in
(* Options.feedback "new variable %a (global? %b)" Varinfo.pretty v global;*)
let e = Cil.evar v in
let stmts = mk_stmts v e in
let new_stmts = acc_list_rev local_block.new_stmts stmts in
let new_block_vars = match scope with
- | Global | Function -> local_block.new_block_vars
- | Local_block -> v :: local_block.new_block_vars
+ | Varname.Global | Varname.Function -> local_block.new_block_vars
+ | Varname.Block -> v :: local_block.new_block_vars
in
let new_block =
{ new_block_vars = new_block_vars;
@@ -246,7 +214,7 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
| Some t -> Term.Map.add t (v, e) tbl.new_exps }
in
match scope with
- | Global | Function ->
+ | Varname.Global | Varname.Function ->
let local_env = { local_env with block_info = new_block } in
(* also memoize the new variable, but must never be used *)
{ env with
@@ -254,7 +222,7 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
new_global_vars = (v, lscope) :: env.new_global_vars;
global_mp_tbl = extend_tbl env.global_mp_tbl;
env_stack = local_env :: tl_env }
- | Local_block ->
+ | Varname.Block ->
let local_env =
{ block_info = new_block;
mp_tbl = extend_tbl local_env.mp_tbl;
@@ -278,7 +246,7 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
exception No_term
-let new_var ~loc ?(scope=Local_block) ?name env t ty mk_stmts =
+let new_var ~loc ?(scope=Varname.Block) ?name env t ty mk_stmts =
let local_env, _ = top env in
let memo tbl =
try
@@ -291,8 +259,8 @@ let new_var ~loc ?(scope=Local_block) ?name env t ty mk_stmts =
do_new_var ~loc ~scope ?name env t ty mk_stmts
in
match scope with
- | Global | Function -> memo env.global_mp_tbl
- | Local_block -> memo local_env.mp_tbl
+ | Varname.Global | Varname.Function -> memo env.global_mp_tbl
+ | Varname.Block -> memo local_env.mp_tbl
let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
new_var
@@ -301,7 +269,7 @@ let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
?name
env
t
- (Gmp.Z.t ())
+ (Gmp_types.Z.t ())
(fun v e -> Gmp.init ~loc e :: mk_stmts v e)
module Logic_binding = struct
@@ -322,7 +290,7 @@ module Logic_binding = struct
| Some ty -> ty
| None -> match logic_v.lv_type with
| Ctype ty -> ty
- | Linteger -> Gmp.Z.t ()
+ | Linteger -> Gmp_types.Z.t ()
| Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
| Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
let msg =
@@ -443,7 +411,7 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
let local_env, tl = top env in
let clear =
if global_clear then begin
- Varname.clear ();
+ Varname.clear_locals ();
env.global_mp_tbl.clear_stmts @ local_env.mp_tbl.clear_stmts
end else
local_env.mp_tbl.clear_stmts
@@ -551,6 +519,6 @@ let pretty fmt env =
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
similarity index 96%
rename from src/plugins/e-acsl/src/env.mli
rename to src/plugins/e-acsl/src/code_generator/env.mli
index 247a44cf852..6e81ceb7395 100644
--- a/src/plugins/e-acsl/src/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -41,17 +41,8 @@ type localized_scope =
| LFunction of kernel_function
| LLocal_block of kernel_function
-type scope =
- | Global
- | Function
- | Local_block
-
-module Varname: sig
- val get: scope:scope -> string -> string
-end
-
val new_var:
- loc:location -> ?scope:scope -> ?name:string ->
+ loc:location -> ?scope:Varname.scope -> ?name:string ->
t -> term option -> typ ->
(varinfo -> exp (* the var as exp *) -> stmt list) ->
varinfo * exp * t
@@ -62,7 +53,7 @@ val new_var:
initialized by applying it to [mk_stmts]. *)
val new_var_and_mpz_init:
- loc:location -> ?scope:scope -> ?name:string ->
+ loc:location -> ?scope:Varname.scope -> ?name:string ->
t -> term option ->
(varinfo -> exp (* the var as exp *) -> stmt list) ->
varinfo * exp * t
@@ -188,6 +179,6 @@ val pretty: Format.formatter -> t -> unit
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
similarity index 59%
rename from src/plugins/e-acsl/src/gmp.ml
rename to src/plugins/e-acsl/src/code_generator/gmp.ml
index 42f468554b0..c2839c8a2cc 100644
--- a/src/plugins/e-acsl/src/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -22,95 +22,6 @@
open Cil_types
-(**************************************************************************)
-(***************************** mpz types***********************************)
-(**************************************************************************)
-
-let mk_dummy_type_info_ref () =
- ref
- { torig_name = "";
- tname = "";
- ttype = TVoid [];
- treferenced = false }
-
-module type S = sig
- val t: unit -> typ
- val t_as_ptr: unit -> typ
- val is_now_referenced: unit -> unit
- val is_t: typ -> bool
-end
-
-module Make(X: sig end) = struct
-
- let t_torig_ref = mk_dummy_type_info_ref ()
- let t_struct_torig_ref = mk_dummy_type_info_ref ()
-
- let set_t ty = t_torig_ref := ty
- let set_t_struct ty = t_struct_torig_ref := ty
-
- let is_now_referenced () = !t_torig_ref.treferenced <- true
-
- let t () = TNamed(!t_torig_ref, [])
-
- (* create a unique shared representation in order to use [==] in [is_t] *)
- let t_as_ptr_info =
- lazy
- {
- torig_name = "";
- tname = !t_struct_torig_ref.tname ^ " *";
- ttype = TArray(
- TNamed(!t_struct_torig_ref, []),
- Some (Cil.one ~loc:Cil_datatype.Location.unknown),
- {scache = Not_Computed},
- []);
- treferenced = true;
- }
-
- let t_as_ptr () = TNamed (Lazy.force t_as_ptr_info, [])
-
- let is_t ty = match ty with
- | TNamed(tinfo, []) ->
- tinfo == !t_torig_ref || tinfo == Lazy.force t_as_ptr_info
- | _ -> false
-
-end
-
-module Z = Make(struct end)
-module Q = Make(struct end)
-
-(**************************************************************************)
-(******************* Initialization of mpz and mpq types ******************)
-(**************************************************************************)
-
-let init_t () =
- Options.feedback ~level:2 "initializing GMP types.";
- let set_mp_t = object (self)
- inherit Cil.nopCilVisitor
-
- (* exit after having initialized the 4 values (for Z.t and Q.t) *)
- val mutable visited = 0
- method private set f info =
- f info;
- if visited = 3 then
- raise Exit
- else begin
- visited <- visited + 1;
- Cil.SkipChildren
- end
-
- method !vglob = function
- | GType({ torig_name = name } as info, _) ->
- if name = "__e_acsl_mpz_t" then self#set Z.set_t info
- else if name = "__e_acsl_mpz_struct" then self#set Z.set_t_struct info
- else if name = "__e_acsl_mpq_t" then self#set Q.set_t info
- else if name = "__e_acsl_mpq_struct" then self#set Q.set_t_struct info
- else Cil.SkipChildren
- | _ ->
- Cil.SkipChildren
-
- end in
- try Cil.visitCilFileSameGlobals set_mp_t (Ast.get ()) with Exit -> ()
-
(**************************************************************************)
(************************* Calls to builtins ******************************)
(**************************************************************************)
@@ -118,8 +29,8 @@ let init_t () =
let apply_on_var ~loc funname e =
let prefix =
let ty = Cil.typeOf e in
- if Z.is_t ty then "__gmpz_"
- else if Q.is_t ty then "__gmpq_"
+ if Gmp_types.Z.is_t ty then "__gmpz_"
+ else if Gmp_types.Q.is_t ty then "__gmpq_"
else assert false
in
Misc.mk_call ~loc (prefix ^ funname) [ e ]
@@ -131,7 +42,7 @@ exception Longlong of ikind
let get_set_suffix_and_arg e =
let ty = Cil.typeOf e in
- if Z.is_t ty || Q.is_t ty then "", [ e ]
+ if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then "", [ e ]
else
match Cil.unrollType ty with
| TInt(IChar, _) ->
@@ -159,7 +70,7 @@ let get_set_suffix_and_arg e =
let generic_affect ~loc fname lv ev e =
let ty = Cil.typeOf ev in
- if Z.is_t ty || Q.is_t ty then begin
+ if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then begin
let suf, args = get_set_suffix_and_arg e in
Misc.mk_call ~loc (fname ^ suf) (ev :: args)
end else
@@ -168,9 +79,9 @@ let generic_affect ~loc fname lv ev e =
let init_set ~loc lv ev e =
let fname =
let ty = Cil.typeOf ev in
- if Z.is_t ty then
+ if Gmp_types.Z.is_t ty then
"__gmpz_init_set"
- else if Q.is_t ty then
+ else if Gmp_types.Q.is_t ty then
Options.fatal "no __gmpq_init_set: init then set separately"
else
""
@@ -180,7 +91,7 @@ let init_set ~loc lv ev e =
| Longlong IULongLong ->
(match e.enode with
| Lval elv ->
- assert (Z.is_t (Cil.typeOf ev));
+ assert (Gmp_types.Z.is_t (Cil.typeOf ev));
let call = Misc.mk_call
~loc
"__gmpz_import"
@@ -201,8 +112,8 @@ let init_set ~loc lv ev e =
let affect ~loc lv ev e =
let fname =
let ty = Cil.typeOf ev in
- if Z.is_t ty then "__gmpz_set"
- else if Q.is_t ty then "__gmpq_set"
+ if Gmp_types.Z.is_t ty then "__gmpz_set"
+ else if Gmp_types.Q.is_t ty then "__gmpq_set"
else ""
in
try generic_affect ~loc fname lv ev e
@@ -211,6 +122,6 @@ let affect ~loc lv ev e =
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/gmp.mli b/src/plugins/e-acsl/src/code_generator/gmp.mli
similarity index 71%
rename from src/plugins/e-acsl/src/gmp.mli
rename to src/plugins/e-acsl/src/code_generator/gmp.mli
index 4dcab5e720f..b526bda347d 100644
--- a/src/plugins/e-acsl/src/gmp.mli
+++ b/src/plugins/e-acsl/src/code_generator/gmp.mli
@@ -20,36 +20,10 @@
(* *)
(**************************************************************************)
-(** GMP Values. *)
+(** Calls to the GMP's API. *)
open Cil_types
-val init_t: unit -> unit
-(** Must be called before any use of GMP *)
-
-(**************************************************************************)
-(******************************** Types ***********************************)
-(**************************************************************************)
-
-module type S = sig
- val t: unit -> typ
- val t_as_ptr: unit -> typ (** type equivalent to [t] but seen as a pointer *)
- val is_now_referenced: unit -> unit
- val is_t: typ -> bool
-end
-
-(** Representation of the unbounded integer type at runtime *)
-module Z: sig
- include S
-end
-
-(** Representation of the rational type at runtime *)
-module Q: S
-
-(**************************************************************************)
-(************************* Calls to builtins ******************************)
-(**************************************************************************)
-
val init: loc:location -> exp -> stmt
(** build stmt [mpz_init(v)] or [mpq_init(v)] depending on typ of [v] *)
@@ -68,6 +42,6 @@ val affect: loc:location -> lval -> exp -> exp -> stmt
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/label.ml b/src/plugins/e-acsl/src/code_generator/label.ml
similarity index 100%
rename from src/plugins/e-acsl/src/label.ml
rename to src/plugins/e-acsl/src/code_generator/label.ml
diff --git a/src/plugins/e-acsl/src/label.mli b/src/plugins/e-acsl/src/code_generator/label.mli
similarity index 100%
rename from src/plugins/e-acsl/src/label.mli
rename to src/plugins/e-acsl/src/code_generator/label.mli
diff --git a/src/plugins/e-acsl/src/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
similarity index 98%
rename from src/plugins/e-acsl/src/logic_functions.ml
rename to src/plugins/e-acsl/src/code_generator/logic_functions.ml
index dfaec0c2b93..74ce5b5f95f 100644
--- a/src/plugins/e-acsl/src/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -41,7 +41,7 @@ let term_to_exp_ref
(* @return true iff the result of the function is provided by reference as the
first extra argument at each call *)
-let result_as_extra_argument = Gmp.Z.is_t
+let result_as_extra_argument = Gmp_types.Z.is_t
(* TODO: to be extended to any compound type? E.g. returning a struct is not
good practice... *)
@@ -125,11 +125,11 @@ let generate_kf ~loc fname env ret_ty params_ty li =
| Typing.Gmpz ->
(* GMP's integer are arrays: consider them as pointers in function's
parameters *)
- Gmp.Z.t_as_ptr ()
+ Gmp_types.Z.t_as_ptr ()
| Typing.C_integer ik -> TInt(ik, [])
| Typing.C_float ik -> TFloat(ik, [])
(* for the time being, no reals but rationals instead *)
- | Typing.Rational -> Real.t ()
+ | Typing.Rational -> Gmp_types.Q.t ()
| Typing.Real -> Error.not_yet "real number"
| Typing.Nan -> Typing.typ_of_lty lvi.lv_type
in
@@ -343,3 +343,9 @@ let tapp_to_exp ~loc fname env t li params_ty args =
(Some t)
ret_ty
(fun vi _ -> [ Cil.mkStmtOneInstr ~valid_sid:true (mkcall vi) ])
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/logic_functions.mli b/src/plugins/e-acsl/src/code_generator/logic_functions.mli
similarity index 98%
rename from src/plugins/e-acsl/src/logic_functions.mli
rename to src/plugins/e-acsl/src/code_generator/logic_functions.mli
index 3738f98117b..160170331fb 100644
--- a/src/plugins/e-acsl/src/logic_functions.mli
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.mli
@@ -54,3 +54,9 @@ val named_predicate_to_exp_ref:
val term_to_exp_ref:
(kernel_function -> Env.t -> term -> exp * Env.t) ref
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
similarity index 100%
rename from src/plugins/e-acsl/src/loops.ml
rename to src/plugins/e-acsl/src/code_generator/loops.ml
diff --git a/src/plugins/e-acsl/src/loops.mli b/src/plugins/e-acsl/src/code_generator/loops.mli
similarity index 100%
rename from src/plugins/e-acsl/src/loops.mli
rename to src/plugins/e-acsl/src/code_generator/loops.mli
diff --git a/src/plugins/e-acsl/src/mmodel_translate.ml b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
similarity index 99%
rename from src/plugins/e-acsl/src/mmodel_translate.ml
rename to src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
index 314f9c38c17..51ba54b1c98 100644
--- a/src/plugins/e-acsl/src/mmodel_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
@@ -70,7 +70,7 @@ let rec has_set_as_index = function
let eliminate_ranges_from_index_of_term ~loc t =
match t.term_node with
| Trange(Some n1, Some n2) ->
- let name = Env.Varname.get ~scope:Env.Local_block "range" in
+ let name = Varname.get ~scope:Varname.Block "range" in
let lv = Cil_const.make_logic_var_kind name LVQuant Linteger in
let tlv = Logic_const.tvar ~loc lv in
tlv, (n1, lv, n2)
diff --git a/src/plugins/e-acsl/src/mmodel_translate.mli b/src/plugins/e-acsl/src/code_generator/mmodel_translate.mli
similarity index 100%
rename from src/plugins/e-acsl/src/mmodel_translate.mli
rename to src/plugins/e-acsl/src/code_generator/mmodel_translate.mli
diff --git a/src/plugins/e-acsl/src/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
similarity index 100%
rename from src/plugins/e-acsl/src/quantif.ml
rename to src/plugins/e-acsl/src/code_generator/quantif.ml
diff --git a/src/plugins/e-acsl/src/quantif.mli b/src/plugins/e-acsl/src/code_generator/quantif.mli
similarity index 100%
rename from src/plugins/e-acsl/src/quantif.mli
rename to src/plugins/e-acsl/src/code_generator/quantif.mli
diff --git a/src/plugins/e-acsl/src/real.ml b/src/plugins/e-acsl/src/code_generator/real.ml
similarity index 98%
rename from src/plugins/e-acsl/src/real.ml
rename to src/plugins/e-acsl/src/code_generator/real.ml
index 8827392aaf1..7fb783c32eb 100644
--- a/src/plugins/e-acsl/src/real.ml
+++ b/src/plugins/e-acsl/src/code_generator/real.ml
@@ -27,7 +27,7 @@ let t () =
the following typ MUST be changed into a typ that can represent them.
It is sound to use GMPQ for the time being since irrationals
raise not_yet. *)
- Gmp.Q.t ()
+ Gmp_types.Q.t ()
let is_t ty = Cil_datatype.Typ.equal ty (t ())
@@ -40,7 +40,7 @@ let init_set ~loc lval vi_e e =
Gmp.affect ~loc lval vi_e e ]))
let mk_real ~loc ?name e env t_opt =
- if Gmp.Z.is_t (Cil.typeOf e) then
+ if Gmp_types.Z.is_t (Cil.typeOf e) then
(* GMPQ has no builtin for creating Q from Z. Hence:
1) Get the MPZ as a string: gmZ_get_str
2) Set the MPQ with that string: gmpQ_set_str *)
@@ -233,3 +233,9 @@ let binop ~loc bop e1 e2 env t_opt =
let name = Misc.name_of_binop bop in
let _, e, env = new_var_and_init ~loc ~name env t_opt mk_stmts in
e, env
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/real.mli b/src/plugins/e-acsl/src/code_generator/real.mli
similarity index 98%
rename from src/plugins/e-acsl/src/real.mli
rename to src/plugins/e-acsl/src/code_generator/real.mli
index cca50791d97..1a16c80aa49 100644
--- a/src/plugins/e-acsl/src/real.mli
+++ b/src/plugins/e-acsl/src/code_generator/real.mli
@@ -68,3 +68,9 @@ val cmp: loc:location -> binop -> exp -> exp -> Env.t -> term option ->
exp * Env.t
(** Compares two expressions according to the given [binop]. The optional term
indicates whether the comparison has a correspondance in the logic. *)
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
similarity index 98%
rename from src/plugins/e-acsl/src/temporal.ml
rename to src/plugins/e-acsl/src/code_generator/temporal.ml
index d624f2ebd57..828883321c4 100644
--- a/src/plugins/e-acsl/src/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -30,13 +30,6 @@ module Libc = Functions.Libc
open Cil_types
open Cil_datatype
-(* ************************************************************************** *)
-(* Configuration {{{ *)
-(* ************************************************************************** *)
-
-let generate = ref false
-(* }}} *)
-
(* ************************************************************************** *)
(* Types {{{ *)
(* ************************************************************************** *)
@@ -496,12 +489,8 @@ let mk_global_init ~loc vi off init env =
(* Public API {{{ *)
(* ************************************************************************** *)
-let enable param = generate := param
-
-let is_enabled () = !generate
-
let handle_function_parameters kf env =
- if is_enabled () then
+ if Options.Temporal_validity.get () then
let env, _ = List.fold_left
(fun (env, index) param ->
let param = Visitor_behavior.Get.varinfo (Env.get_behavior env) param in
@@ -517,7 +506,7 @@ let handle_function_parameters kf env =
env
let handle_stmt stmt env =
- if is_enabled () then begin
+ if Options.Temporal_validity.get () then begin
match stmt.skind with
| Instr instr -> handle_instruction stmt instr env
| Return(ret, loc) -> Extlib.may_map
@@ -529,8 +518,14 @@ let handle_stmt stmt env =
env
let generate_global_init vi off init env =
- if is_enabled () then
+ if Options.Temporal_validity.get () then
mk_global_init ~loc:vi.vdecl vi off init env
else
None
(* }}} *)
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/temporal.mli b/src/plugins/e-acsl/src/code_generator/temporal.mli
similarity index 93%
rename from src/plugins/e-acsl/src/temporal.mli
rename to src/plugins/e-acsl/src/code_generator/temporal.mli
index 17b419e08d9..f9604dbd2f5 100644
--- a/src/plugins/e-acsl/src/temporal.mli
+++ b/src/plugins/e-acsl/src/code_generator/temporal.mli
@@ -23,12 +23,6 @@
(** Transformations to detect temporal memory errors (e.g., dereference of
stale pointers). *)
-val enable: bool -> unit
-(** Enable/disable temporal transformations *)
-
-val is_enabled: unit -> bool
-(** Return a boolean value indicating whether temporal analysis is enabled *)
-
val handle_function_parameters: Cil_types.kernel_function -> Env.t -> Env.t
(** [handle_function_parameters kf env] updates the local environment [env],
according to the parameters of [kf], with statements allowing to track
@@ -42,3 +36,9 @@ val generate_global_init: Cil_types.varinfo -> Cil_types.offset ->
Cil_types.init -> Env.t -> Cil_types.stmt option
(** Generate [Some s], where [s] is a statement tracking global initializer
or [None] if there is no need to track it *)
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
similarity index 98%
rename from src/plugins/e-acsl/src/translate.ml
rename to src/plugins/e-acsl/src/code_generator/translate.ml
index 74770c07948..9779637e261 100644
--- a/src/plugins/e-acsl/src/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -77,7 +77,7 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
?name
env
t_opt
- (Gmp.Z.t ())
+ (Gmp_types.Z.t ())
(fun lv v -> [ Gmp.init_set ~loc (Cil.var lv) v e ])
in
e, env
@@ -92,7 +92,7 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
e, env
| Some ctx ->
let ty = Cil.typeOf e in
- match Gmp.Z.is_t ty, Gmp.Z.is_t ctx with
+ match Gmp_types.Z.is_t ty, Gmp_types.Z.is_t ctx with
| true, true ->
(* Z --> Z *)
e, env
@@ -117,7 +117,7 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
if Real.is_t ctx then
if Real.is_t (Cil.typeOf e) then (* R --> R *) e, env
else (* C integer or Z --> R *) Real.mk_real ~loc ?name e env t_opt
- else if Gmp.Z.is_t ty || strnum = Str_Z then
+ else if Gmp_types.Z.is_t ty || strnum = Str_Z then
(* Z --> C type or the integer is represented by a string:
anyway, it fits into a C integer: convert it *)
let fname, new_ty =
@@ -161,7 +161,7 @@ let constant_to_exp ~loc t c =
| Typing.C_integer kind ->
let cast = Typing.get_cast t in
match cast, kind with
- | Some ty, (ILongLong | IULongLong) when Gmp.Z.is_t ty ->
+ | Some ty, (ILongLong | IULongLong) when Gmp_types.Z.is_t ty ->
(* too large integer *)
Cil.mkString ~loc (Integer.to_string n), Str_Z
| Some ty, _ when Real.is_t ty ->
@@ -284,7 +284,7 @@ and context_insensitive_term_to_exp kf env t =
| TUnOp(Neg | BNot as op, t') ->
let ty = Typing.get_typ t in
let e, env = term_to_exp kf env t' in
- if Gmp.Z.is_t ty then
+ if Gmp_types.Z.is_t ty then
let name, vname = match op with
| Neg -> "__gmpz_neg", "neg"
| BNot -> "__gmpz_com", "bnot"
@@ -305,7 +305,7 @@ and context_insensitive_term_to_exp kf env t =
Cil.new_exp ~loc (UnOp(op, e, ty)), env, C_number, ""
| TUnOp(LNot, t) ->
let ty = Typing.get_op t in
- if Gmp.Z.is_t ty then
+ if Gmp_types.Z.is_t ty then
(* [!t] is converted into [t == 0] *)
let zero = Logic_const.tinteger 0 in
let ctx = Typing.get_number_ty t in
@@ -323,7 +323,7 @@ and context_insensitive_term_to_exp kf env t =
let ty = Typing.get_typ t in
let e1, env = term_to_exp kf env t1 in
let e2, env = term_to_exp kf env t2 in
- if Gmp.Z.is_t ty then
+ if Gmp_types.Z.is_t ty then
let name = name_of_mpz_arith_bop bop in
let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
@@ -342,7 +342,7 @@ and context_insensitive_term_to_exp kf env t =
let ty = Typing.get_typ t in
let e1, env = term_to_exp kf env t1 in
let e2, env = term_to_exp kf env t2 in
- if Gmp.Z.is_t ty then
+ if Gmp_types.Z.is_t ty then
(* TODO: preventing division by zero should not be required anymore.
RTE should do this automatically. *)
let ctx = Typing.get_number_ty t in
@@ -360,7 +360,7 @@ and context_insensitive_term_to_exp kf env t =
~loc kf env Typing.gmpz ~e1:e2 ~name Eq t2 zero t
in
let mk_stmts _v e =
- assert (Gmp.Z.is_t ty);
+ assert (Gmp_types.Z.is_t ty);
let vis = Env.get_visitor env in
let kf = Extlib.the vis#current_kf in
let cond =
@@ -500,7 +500,7 @@ and context_insensitive_term_to_exp kf env t =
([], [], env)
in
let gen_fname =
- Env.Varname.get ~scope:Env.Global (Functions.RTL.mk_gen_name fname)
+ Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname)
in
Logic_functions.tapp_to_exp ~loc gen_fname env t li params_ty args
in
@@ -626,7 +626,7 @@ and at_to_exp_no_lscope env t_opt label e =
Env.new_var
~loc
~name:"at"
- ~scope:Env.Function
+ ~scope:Varname.Function
env
t_opt
(Cil.typeOf e)
@@ -915,8 +915,8 @@ exception No_simple_translation of term
let term_to_exp typ t =
(* infer a context from the given [typ] whenever possible *)
let ctx_of_typ ty =
- if Gmp.Z.is_t ty then Typing.gmpz
- else if Real.is_t ty then Typing.rational
+ if Gmp_types.Z.is_t ty then Typing.gmpz
+ else if Gmp_types.Q.is_t ty then Typing.rational
else
match ty with
| TInt(ik, _) -> Typing.ikind ik
@@ -1127,6 +1127,6 @@ let translate_post_code_annotation kf env annot =
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/translate.mli b/src/plugins/e-acsl/src/code_generator/translate.mli
similarity index 98%
rename from src/plugins/e-acsl/src/translate.mli
rename to src/plugins/e-acsl/src/code_generator/translate.mli
index 7e58df3a032..741cd5db0f3 100644
--- a/src/plugins/e-acsl/src/translate.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate.mli
@@ -52,6 +52,6 @@ val set_original_project: Project.t -> unit
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/visit.ml b/src/plugins/e-acsl/src/code_generator/visit.ml
similarity index 99%
rename from src/plugins/e-acsl/src/visit.ml
rename to src/plugins/e-acsl/src/code_generator/visit.ml
index 67f7cc763f5..1856aea47e4 100644
--- a/src/plugins/e-acsl/src/visit.ml
+++ b/src/plugins/e-acsl/src/code_generator/visit.ml
@@ -124,7 +124,7 @@ struct
let vi, exp, env =
Env.new_var
~loc
- ~scope:Env.Global
+ ~scope:Varname.Global
~name:"literal_string"
env
None
@@ -1055,6 +1055,6 @@ let do_visit ?(prj=Project.current ()) generate =
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/visit.mli b/src/plugins/e-acsl/src/code_generator/visit.mli
similarity index 98%
rename from src/plugins/e-acsl/src/visit.mli
rename to src/plugins/e-acsl/src/code_generator/visit.mli
index ff9d8edb123..5e01f665644 100644
--- a/src/plugins/e-acsl/src/visit.mli
+++ b/src/plugins/e-acsl/src/code_generator/visit.mli
@@ -24,6 +24,6 @@ val do_visit: ?prj:Project.t -> bool -> Visitor.frama_c_visitor
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/builtins.ml b/src/plugins/e-acsl/src/libraries/builtins.ml
similarity index 100%
rename from src/plugins/e-acsl/src/builtins.ml
rename to src/plugins/e-acsl/src/libraries/builtins.ml
diff --git a/src/plugins/e-acsl/src/builtins.mli b/src/plugins/e-acsl/src/libraries/builtins.mli
similarity index 100%
rename from src/plugins/e-acsl/src/builtins.mli
rename to src/plugins/e-acsl/src/libraries/builtins.mli
diff --git a/src/plugins/e-acsl/src/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
similarity index 100%
rename from src/plugins/e-acsl/src/error.ml
rename to src/plugins/e-acsl/src/libraries/error.ml
diff --git a/src/plugins/e-acsl/src/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
similarity index 100%
rename from src/plugins/e-acsl/src/error.mli
rename to src/plugins/e-acsl/src/libraries/error.mli
diff --git a/src/plugins/e-acsl/src/functions.ml b/src/plugins/e-acsl/src/libraries/functions.ml
similarity index 100%
rename from src/plugins/e-acsl/src/functions.ml
rename to src/plugins/e-acsl/src/libraries/functions.ml
diff --git a/src/plugins/e-acsl/src/functions.mli b/src/plugins/e-acsl/src/libraries/functions.mli
similarity index 100%
rename from src/plugins/e-acsl/src/functions.mli
rename to src/plugins/e-acsl/src/libraries/functions.mli
diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.ml b/src/plugins/e-acsl/src/libraries/gmp_types.ml
new file mode 100644
index 00000000000..4a89c181276
--- /dev/null
+++ b/src/plugins/e-acsl/src/libraries/gmp_types.ml
@@ -0,0 +1,114 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** GMP Values. *)
+
+open Cil_types
+
+(**************************************************************************)
+(***************************** GMP types***********************************)
+(**************************************************************************)
+
+let mk_dummy_type_info_ref () =
+ ref
+ { torig_name = "";
+ tname = "";
+ ttype = TVoid [];
+ treferenced = false }
+
+module type S = sig
+ val t: unit -> typ
+ val t_as_ptr: unit -> typ
+ val is_now_referenced: unit -> unit
+ val is_t: typ -> bool
+end
+
+module Make(X: sig end) = struct
+
+ let t_torig_ref = mk_dummy_type_info_ref ()
+ let t_struct_torig_ref = mk_dummy_type_info_ref ()
+
+ let set_t ty = t_torig_ref := ty
+ let set_t_struct ty = t_struct_torig_ref := ty
+
+ let is_now_referenced () = !t_torig_ref.treferenced <- true
+
+ let t () = TNamed(!t_torig_ref, [])
+
+ (* create a unique shared representation in order to use [==] in [is_t] *)
+ let t_as_ptr_info =
+ lazy
+ {
+ torig_name = "";
+ tname = !t_struct_torig_ref.tname ^ " *";
+ ttype = TArray(
+ TNamed(!t_struct_torig_ref, []),
+ Some (Cil.one ~loc:Cil_datatype.Location.unknown),
+ {scache = Not_Computed},
+ []);
+ treferenced = true;
+ }
+
+ let t_as_ptr () = TNamed (Lazy.force t_as_ptr_info, [])
+
+ let is_t ty = match ty with
+ | TNamed(tinfo, []) ->
+ tinfo == !t_torig_ref || tinfo == Lazy.force t_as_ptr_info
+ | _ -> false
+
+end
+
+module Z = Make(struct end)
+module Q = Make(struct end)
+
+(**************************************************************************)
+(******************* Initialization of mpz and mpq types ******************)
+(**************************************************************************)
+
+let init () =
+ Options.feedback ~level:2 "initializing GMP types.";
+ let set_mp_t = object (self)
+ inherit Cil.nopCilVisitor
+
+ (* exit after having initialized the 4 values (for Z.t and Q.t) *)
+ val mutable visited = 0
+ method private set f info =
+ f info;
+ if visited = 3 then
+ raise Exit
+ else begin
+ visited <- visited + 1;
+ Cil.SkipChildren
+ end
+
+ method !vglob = function
+ | GType({ torig_name = name } as info, _) ->
+ if name = "__e_acsl_mpz_t" then self#set Z.set_t info
+ else if name = "__e_acsl_mpz_struct" then self#set Z.set_t_struct info
+ else if name = "__e_acsl_mpq_t" then self#set Q.set_t info
+ else if name = "__e_acsl_mpq_struct" then self#set Q.set_t_struct info
+ else Cil.SkipChildren
+ | _ ->
+ Cil.SkipChildren
+
+ end in
+ try Cil.visitCilFileSameGlobals set_mp_t (Ast.get ()) with Exit -> ()
diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.mli b/src/plugins/e-acsl/src/libraries/gmp_types.mli
new file mode 100644
index 00000000000..8c5558f3119
--- /dev/null
+++ b/src/plugins/e-acsl/src/libraries/gmp_types.mli
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** GMP Values. *)
+
+open Cil_types
+
+val init: unit -> unit
+(** Must be called before any use of GMP *)
+
+(**************************************************************************)
+(******************************** Types ***********************************)
+(**************************************************************************)
+
+(** Signature of a GMP type *)
+module type S = sig
+
+ val t: unit -> typ
+ (** @return the GMP type *)
+
+ val t_as_ptr: unit -> typ
+ (** type equivalent to [t] but seen as a pointer *)
+
+ val is_now_referenced: unit -> unit
+ (** Call this function when using this type for the first time. *)
+
+ val is_t: typ -> bool
+ (** @return true iff the given type is equivalent to the GMP type. *)
+
+end
+
+(** Representation of the unbounded integer type at runtime *)
+module Z: S
+
+(** Representation of the rational type at runtime *)
+module Q: S
diff --git a/src/plugins/e-acsl/src/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
similarity index 100%
rename from src/plugins/e-acsl/src/misc.ml
rename to src/plugins/e-acsl/src/libraries/misc.ml
diff --git a/src/plugins/e-acsl/src/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
similarity index 100%
rename from src/plugins/e-acsl/src/misc.mli
rename to src/plugins/e-acsl/src/libraries/misc.mli
diff --git a/src/plugins/e-acsl/src/libraries/varname.ml b/src/plugins/e-acsl/src/libraries/varname.ml
new file mode 100644
index 00000000000..ee620d48895
--- /dev/null
+++ b/src/plugins/e-acsl/src/libraries/varname.ml
@@ -0,0 +1,52 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+type scope =
+ | Global
+ | Function
+ | Block
+
+module H = Datatype.String.Hashtbl
+let tbl = H.create 7
+let globals = H.create 7
+
+let get ~scope s =
+ let _, u =
+ Extlib.make_unique_name
+ (fun s -> H.mem tbl s || H.mem globals s)
+ ~sep:"_"
+ s
+ in
+ let add = match scope with
+ | Global -> H.add globals
+ | Function | Block -> H.add tbl
+ in
+ add u ();
+ u
+
+let clear_locals () = H.clear tbl
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/libraries/varname.mli b/src/plugins/e-acsl/src/libraries/varname.mli
new file mode 100644
index 00000000000..bb003c54337
--- /dev/null
+++ b/src/plugins/e-acsl/src/libraries/varname.mli
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2018 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* Variable name generator wrt a lexical scope. *)
+
+type scope =
+ | Global
+ | Function
+ | Block
+
+val get: scope:scope -> string -> string
+(** @return a fresh variable name for the given scope wrt the given name. *)
+
+val clear_locals: unit -> unit
+(** Reset the generator for variables that are local to a block or a
+ function. *)
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index b506ae9f5dc..4a2f6b39ca5 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -149,7 +149,6 @@ let generate_code =
apply_on_e_acsl_ast
(fun () ->
Options.feedback "beginning translation.";
- Temporal.enable (Options.Temporal_validity.get ());
let prepared_prj = Prepare_ast.prepare () in
let res =
Project.on prepared_prj
@@ -159,7 +158,7 @@ let generate_code =
Project.on
dup_prj
(fun () ->
- Gmp.init_t ();
+ Gmp_types.init ();
Mmodel_analysis.reset ();
let visit prj = Visit.do_visit ~prj true in
let prj = File.create_project_from_visitor name visit in
@@ -257,7 +256,7 @@ let main () =
if Options.Check.get () then
apply_on_e_acsl_ast
(fun () ->
- Gmp.init_t ();
+ Gmp_types.init ();
ignore (check ()))
()
@@ -265,6 +264,6 @@ let () = Db.Main.extend main
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C .."
End:
*)
diff --git a/src/plugins/e-acsl/src/dup_functions.ml b/src/plugins/e-acsl/src/project_initializer/dup_functions.ml
similarity index 99%
rename from src/plugins/e-acsl/src/dup_functions.ml
rename to src/plugins/e-acsl/src/project_initializer/dup_functions.ml
index 3b675f434bc..205fac4cd6d 100644
--- a/src/plugins/e-acsl/src/dup_functions.ml
+++ b/src/plugins/e-acsl/src/project_initializer/dup_functions.ml
@@ -123,8 +123,8 @@ let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
if vi.vname = "" then
(* unnamed formal parameter: must generate a fresh name since a fundec
cannot have unnamed formals (see bts #2303). *)
- Env.Varname.get
- ~scope:Env.Function
+ Varname.get
+ ~scope:Varname.Function
(Functions.RTL.mk_gen_name "unamed_formal")
else
vi.vname
diff --git a/src/plugins/e-acsl/src/dup_functions.mli b/src/plugins/e-acsl/src/project_initializer/dup_functions.mli
similarity index 100%
rename from src/plugins/e-acsl/src/dup_functions.mli
rename to src/plugins/e-acsl/src/project_initializer/dup_functions.mli
diff --git a/src/plugins/e-acsl/src/keep_status.ml b/src/plugins/e-acsl/src/project_initializer/keep_status.ml
similarity index 100%
rename from src/plugins/e-acsl/src/keep_status.ml
rename to src/plugins/e-acsl/src/project_initializer/keep_status.ml
diff --git a/src/plugins/e-acsl/src/keep_status.mli b/src/plugins/e-acsl/src/project_initializer/keep_status.mli
similarity index 100%
rename from src/plugins/e-acsl/src/keep_status.mli
rename to src/plugins/e-acsl/src/project_initializer/keep_status.mli
diff --git a/src/plugins/e-acsl/src/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
similarity index 98%
rename from src/plugins/e-acsl/src/prepare_ast.ml
rename to src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 4113123a9da..602461c6e58 100644
--- a/src/plugins/e-acsl/src/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -63,7 +63,7 @@ class prepare_visitor prj = object (self)
(* Add align attributes to local variables (required by temporal analysis) *)
method !vblock _ =
- if Temporal.is_enabled () then
+ if Options.Temporal_validity.get () then
Cil.DoChildrenPost (fun blk ->
List.iter (fun vi ->
(* 4 bytes alignment is required to allow sufficient space for storage
@@ -219,3 +219,9 @@ let prepare () =
File.create_project_from_visitor
"e_acsl_prepare_ast"
(new prepare_visitor)
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
similarity index 96%
rename from src/plugins/e-acsl/src/prepare_ast.mli
rename to src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
index 9ba5b76b9a9..f46a04474c2 100644
--- a/src/plugins/e-acsl/src/prepare_ast.mli
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
@@ -28,3 +28,9 @@
- store what is necessary to translate in [Keep_status]. *)
val prepare: unit -> Project.t
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)
--
GitLab