- renaming -e-acsl-runtime by -e-acsl-project

- generating project is compilable
- first test case (for assert \true and \false)

src/plugins/e-acsl/options.ml

@@ -39,7 +39,7 @@ module Check =
 module Project_name =
   EmptyString
     (struct
-      let option_name = "-e-acsl-runtime"
+      let option_name = "-e-acsl-project"
       let help = "generate a new project <prj> from the C program where E-ACSL \
  code is transformed to C code for runtime assertion checking"
       let kind = `Correctness

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.res.oracle

+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+/tmp/frama_c_project_p3cd271i:15:[value] Assertion got status valid.
+[value] Recording results for main
+[value] done for function main
+[dominators] computing for function main
+[dominators] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values for function main:
+          x ∈ {0; }
+/* Generated by Frama-C */
+/*@ terminates \false;
+    ensures \false;
+    assigns \nothing;  */
+extern void exit(int status ) ;
+/*@ assigns \nothing;  */
+extern void eprintf(char * ) ;
+void e_acsl_fail(char *msg ) 
+{
+  eprintf(msg);
+  exit(1);
+  return;
+}
+
+void main(void) 
+{
+  int x ;
+  x = 0;
+  /*@ assert \true; */ ;
+  if (x) { /*@ assert \false; */ ; e_acsl_fail((char *)"(\\false)"); }
+  return;
+}
+
+

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
+OPT: -e-acsl-project p -then-on p -print -val

src/plugins/e-acsl/tests/e-acsl-runtime/trivial.i

+/* run.config
+   COMMENT: testing assert true and false */
+void main() {
+  int x = 0;
+  /*@ assert \true; */
+  if (x) /*@ assert \false; */ ;
+}

src/plugins/e-acsl/visit.ml

@@ -30,6 +30,17 @@ let error s = raise (Typing_error s)
 let not_yet s =
   Options.not_yet_implemented "construct `%s' is not yet supported" s
 
+let e_acsl_fail () =
+ GText("/*@ terminates \\false;\n\
+assigns \\nothing;\n\
+ensures \\false; */\n\
+void exit(int status);\n\
+\n\
+/*@ assigns \\nothing; */ \n\
+extern void eprintf(char * ); \n\
+\n\
+void e_acsl_fail(char *msg) { eprintf(msg); exit(1); }")
+
 let mk_if acc e p =
   (* voidType is incorrect: will be resolved later *)
   let f =
@@ -90,6 +101,14 @@ class e_acsl_visitor prj generate = object
     prj
     ((if generate then Cil.copy_visit else Cil.inplace_visit) ())
 
+  val mutable first_global = true
+
+  method vglob g =
+    if first_global then
+      ChangeDoChildrenPost([ g ], fun l -> e_acsl_fail () :: l)
+    else
+      DoChildren
+
   method vstmt_aux stmt =
     let l = Annotations.get_all_annotations stmt in
     match