diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index ab581b9eeda972297c049863f75109f8bfe89373..ebf83c405e98bd54ad5843e0e78a56e575028ea2 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -37,8 +37,23 @@ PLUGIN_HAS_MLI:=yes
PLUGIN_DISTRIBUTED:=no
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
PLUGIN_DISTRIB_BIN:=no
-#PLUGIN_TESTS_DIRS:=security
-#PLUGIN_NO_DEFAULT_TEST:=yes
+
+###########
+# Testing #
+###########
+
+PLUGIN_TESTS_DIRS:=e-acsl-reject e-acsl-runtime
+PLUGIN_NO_DEFAULT_TEST:=yes
+
+tests/test_config: tests/test_config.in Makefile
+ $(SED) -e "s|${FRAMAC_SHARE}|$(FRAMAC_SHARE)|g" \
+ -e "s|@SEDCMD@|`which sed `|g" $< > $@
+
+tests:: tests/test_config
+
+################
+# Generic part #
+################
include $(FRAMAC_SHARE)/Makefile.dynamic
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index 670eed78384ede9ff7411162e6510ee926f4a1c4..959e309b8c046acdf381ccf62a81e8bafae19394 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -18,7 +18,7 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
-
+(*
let check () =
try
ignore (Visit.do_visit false);
@@ -46,7 +46,7 @@ let fail_check =
"fail_check"
(Datatype.func Datatype.unit Datatype.unit)
fail_check
-
+ *)
module Resulting_projects =
State_builder.Hashtbl
(Datatype.String.Hashtbl)
@@ -77,7 +77,7 @@ let generate_code =
let main () =
let s = Options.Project_name.get () in
- if s = "" then begin if Options.Check.get () then fail_check () end
+ if s = "" then begin(* if Options.Check.get () then fail_check ()*) end
else ignore (generate_code s)
let () = Db.Main.extend main
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/.gitkeep b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/.gitkeep
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/test_config b/src/plugins/e-acsl/tests/e-acsl-reject/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..61e3a7b0e535945b6e22a3d5dca55d4ce3685bd4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/test_config
@@ -0,0 +1 @@
+OPT: -e-acsl-check
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/.gitkeep b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/.gitkeep
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/simple.c b/src/plugins/e-acsl/tests/e-acsl-runtime/simple.c
new file mode 100644
index 0000000000000000000000000000000000000000..c250f87441cfa7b4be06e8f521a2e0dd00548879
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/simple.c
@@ -0,0 +1,4 @@
+void main() {
+ int x = 0;
+ /*@ assert \false; */
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..ab26b4ea81490924ecafab3a14d0177c22765bc5
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
@@ -0,0 +1 @@
+OPT: -e-acsl-runtime p -then-on p -print
diff --git a/src/plugins/e-acsl/tests/test_config.in b/src/plugins/e-acsl/tests/test_config.in
new file mode 100644
index 0000000000000000000000000000000000000000..e0309752413ccf7d3b4bc07ded592b243b9e33f6
--- /dev/null
+++ b/src/plugins/e-acsl/tests/test_config.in
@@ -0,0 +1,2 @@
+CMD: @frama-c@ -cpp-command="gcc -C -E -I. -I${FRAMAC_SHARE}"
+FILTER:@SEDCMD@ -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g"
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 305fe667dadfa8835afa86ac83e5c2bebf0f6c44..1a77b07266fd6f1285363aa79474643a230b1cac 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -19,11 +19,94 @@
(* *)
(**************************************************************************)
+open Db_types
+open Cil_types
+open Cil
+
+let unknown_loc = Cil_datatype.Location.unknown
+
exception Typing_error of string
+let error s = raise (Typing_error s)
+let not_yet s =
+ Options.not_yet_implemented "construct `%s' is not yet supported" s
+
+let mk_if acc e p =
+ (* voidType is incorrect: will be resolved later *)
+ let f =
+ new_exp unknown_loc (Lval (var (makeGlobalVar "e_acsl_fail" voidType)))
+ in
+ let msg =
+ let b = Buffer.create 97 in
+ let fmt = Format.formatter_of_buffer b in
+ Format.fprintf fmt "%a@?" Cil.d_predicate_named p;
+ Buffer.contents b
+ in
+ let s = Instr(Call(None, f, [ mkString unknown_loc msg ], unknown_loc))in
+ mkStmt(If(e, mkBlock [ mkStmt s ], mkBlock [], unknown_loc)) :: acc
+
+let convert_named_predicate acc generate p =
+ let mk_if e = mk_if acc e p in
+ match p.content with
+ | Pfalse -> if generate then mk_if (zero ~loc:unknown_loc) else acc
+ | Ptrue -> if generate then mk_if (one ~loc:unknown_loc) else acc
+ | Papp _ -> not_yet "logic function application"
+ | Pseparated _ -> not_yet "separated"
+ | Prel _ -> not_yet "relation"
+ | Pand _ -> not_yet "&&"
+ | Por _ -> not_yet "||"
+ | Pxor _ -> not_yet "xor"
+ | Pimplies _ -> not_yet "==>"
+ | Piff _ -> not_yet "<==>"
+ | Pnot _ -> not_yet "!"
+ | Pif _ -> not_yet "_ ? _ : _"
+ | Plet _ -> not_yet "let _ = _ in _"
+ | Pforall _ -> not_yet "\\forall"
+ | Pexists _ -> not_yet "\\exists"
+ | Pold _ -> not_yet "\\old"
+ | Pat _ -> not_yet "\\at"
+ | Pvalid _ -> not_yet "\\valid"
+ | Pvalid_index _ -> not_yet "\\valid_index"
+ | Pvalid_range _ -> not_yet "\\valid_range"
+ | Pfresh _ -> not_yet "\\fresh"
+ | Psubtype _ -> not_yet "subtyping relation"
+
+let convert_annotation acc generate annot = match annot.annot_content with
+ | AAssert(_l, p) -> convert_named_predicate acc generate p
+ | AStmtSpec _ -> not_yet "stmt spec"
+ | AInvariant _ -> not_yet "invariant"
+ | AVariant _ -> not_yet "variant"
+ | AAssigns _ -> not_yet "assigns"
+ | APragma _ -> not_yet "pragma"
+
+let convert_rooted acc generate (User a | AI(_, a)) =
+ convert_annotation acc generate a
+
+let convert_before_after acc generate (Before r | After r) =
+ convert_rooted acc generate r
+
+class e_acsl_visitor prj generate = object
+
+ inherit Visitor.generic_frama_c_visitor
+ prj
+ ((if generate then Cil.copy_visit else Cil.inplace_visit) ())
+
+ method vstmt_aux stmt =
+ let l = Annotations.get_all_annotations stmt in
+ match
+ List.fold_right (fun ba acc -> convert_before_after acc generate ba) l []
+ with
+ | [] -> DoChildren
+ | l ->
+ assert generate;
+ let mk_block stmt =
+ mkStmt ~valid_sid:true (Block (mkBlock (l @ [ stmt ])))
+ in
+ ChangeDoChildrenPost(stmt, mk_block)
+
+end
-let do_visit ?(prj=Project.current ()) _generate =
-(* let _p = prj in
- assert false*) new Visitor.generic_frama_c_visitor prj (Cil.copy_visit ())
+let do_visit ?(prj=Project.current ()) generate =
+ new e_acsl_visitor prj generate
(*
Local Variables: