[e-acsl] preserve property statuses again

src/plugins/e-acsl/src/analyses/rte.ml

@@ -24,17 +24,6 @@
 (** {2 Generic code} *)
 (* ************************************************************************** *)
 
-let apply_rte f x =
-  let signed = Kernel.SignedOverflow.get () in
-  let unsigned = Kernel.UnsignedOverflow.get () in
-  Kernel.SignedOverflow.off ();
-  Kernel.UnsignedOverflow.off ();
-  let finally () =
-    Kernel.SignedOverflow.set signed;
-    Kernel.UnsignedOverflow.set unsigned
-  in
-  Extlib.try_finally ~finally f x
-
 let warn_rte warn exn =
   if warn then
     Options.warning "@[@[cannot run RTE:@ %s.@]@ \
@@ -48,30 +37,24 @@ Ignoring potential runtime errors in annotations."
 open Cil_datatype
 
 let stmt ?(warn=true) =
-  try 
-    let f = 
-      Dynamic.get
-	~plugin:"RteGen" 
-	"stmt_annotations" 
-	(Datatype.func2 Kernel_function.ty Stmt.ty 
-	   (let module L = Datatype.List(Code_annotation) in L.ty))
-    in
-    (fun x y -> apply_rte (f x) y)
+  try
+    Dynamic.get
+      ~plugin:"RteGen"
+      "stmt_annotations"
+      (Datatype.func2 Kernel_function.ty Stmt.ty
+         (let module L = Datatype.List(Code_annotation) in L.ty))
   with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
     ->
       warn_rte warn exn;
       fun _ _ -> []
 
 let exp ?(warn=true) =
-  try 
-    let f = 
-      Dynamic.get
-	~plugin:"RteGen" 
-	"exp_annotations" 
-	(Datatype.func3 Kernel_function.ty Stmt.ty Exp.ty 
-	   (let module L = Datatype.List(Code_annotation) in L.ty))
-    in
-    (fun x y z -> apply_rte (f x y) z)
+  try
+    Dynamic.get
+      ~plugin:"RteGen"
+      "exp_annotations"
+      (Datatype.func3 Kernel_function.ty Stmt.ty Exp.ty
+         (let module L = Datatype.List(Code_annotation) in L.ty))
   with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
     ->
       warn_rte warn exn;
@@ -79,6 +62,6 @@ let exp ?(warn=true) =
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/analyses/rte.mli

@@ -32,6 +32,6 @@ val exp: ?warn:bool -> kernel_function -> stmt -> exp -> code_annotation list
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/main.ml

@@ -50,9 +50,6 @@ let generate_code =
     (fun name ->
        Options.feedback "beginning translation.";
        Temporal.enable (Options.Temporal_validity.get ());
-       let rtl_prj =
-         Project.create_by_copy ~last:false "E_ACSL RTL"
-       in
        if Plugin.is_present "variadic" then begin
          let opt_name = "-variadic-translation" in
          if Dynamic.Parameter.Bool.get opt_name () then begin
@@ -64,6 +61,11 @@ let generate_code =
            Dynamic.Parameter.Bool.off opt_name ();
          end
        end;
+       (* slightly more efficient to copy the project before computing the AST
+          if it is not yet computed *)
+       let rtl_prj = Project.create_by_copy ~last:false "E_ACSL RTL" in
+       (* TODO: remove [rtl_prj] after use if no debug mode *)
+       (* force AST computation before copying the project it belongs to *)
        Ast.compute ();
        let copied_prj = Project.create_by_copy ~last:true name in
        Project.on
@@ -72,7 +74,21 @@ let generate_code =
             (* preparation of the AST does not concern the E-ACSL RTL *)
             Prepare_ast.prepare ();
             Rtl.link rtl_prj;
-            Injector.inject ();
+            (* the E-ACSL type system ensures the soundness of the generated
+               arithmetic operations. Therefore, deactivate the corresponding
+               options in order to prevent RTE to generate spurious alarms. *)
+            let signed = Kernel.SignedOverflow.get () in
+            let unsigned = Kernel.UnsignedOverflow.get () in
+            (* we do know that setting these flags does not modify the program's
+               semantics: using their unsafe variants is thus safe and preserve
+               all emitted property statuses. *)
+            Kernel.SignedOverflow.unsafe_set false;
+            Kernel.UnsignedOverflow.unsafe_set false;
+            let finally () =
+              Kernel.SignedOverflow.unsafe_set signed;
+              Kernel.UnsignedOverflow.unsafe_set unsigned
+            in
+            Extlib.try_finally ~finally Injector.inject ();
             (* remove the RTE's results computed from E-ACSL: they are partial
                and associated with the wrong kernel function (the one of the old
                project). *)