e-acsl implem is on the beginning of the way

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
 

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

src/plugins/e-acsl/tests/e-acsl-reject/test_config

+OPT: -e-acsl-check

src/plugins/e-acsl/tests/e-acsl-runtime/simple.c

+void main() {
+  int x = 0;
+  /*@ assert \false; */
+}

src/plugins/e-acsl/tests/e-acsl-runtime/test_config

+OPT: -e-acsl-runtime p -then-on p -print

src/plugins/e-acsl/tests/test_config.in

+CMD: @frama-c@ -cpp-command="gcc -C -E -I. -I${FRAMAC_SHARE}"
+FILTER:@SEDCMD@ -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g"

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: