From 8b037136de5080b4385b78943d111221bf4bb575 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 27 Aug 2020 13:23:54 +0200
Subject: [PATCH] [e-acsl] improves/fixes a fewTODOs
---
.../e-acsl/src/code_generator/translate.ml | 10 ++++++----
src/plugins/e-acsl/src/main.ml | 15 +++------------
.../e-acsl/src/project_initializer/prepare_ast.ml | 2 +-
3 files changed, 10 insertions(+), 17 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 66e129d1ce2..009763c7931 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1149,7 +1149,8 @@ let must_translate ppt =
(* [TODO] generating code for "valid under hypotheses" properties could be
useful for some use cases (in particular, when E-ACSL does not stop on
the very first error).
- ==> introduce a new option or modify the behavior of -e-acsl-valid *)
+ ==> introduce a new option or modify the behavior of -e-acsl-valid,
+ see e-acsl#35 *)
false
let must_translate_opt = function
@@ -1198,7 +1199,7 @@ let translate_postconditions kf kinstr env behaviors =
let env =
handle_error
(fun env ->
- let active = [] in (* TODO: 'for' behaviors *)
+ let active = [] in (* TODO: 'for' behaviors, e-acsl#109 *)
let ppt = Property.ip_assigns_of_behavior kf kinstr ~active b in
if b.b_assigns <> WritesAny && must_translate_opt ppt
then not_yet env "assigns clause in behavior";
@@ -1250,7 +1251,7 @@ let translate_pre_spec kf kinstr env spec =
let ppt = Property.ip_terminates_of_spec kf kinstr spec in
if must_translate_opt ppt then not_yet env "terminates clause")
spec;
- let active = [] in (* TODO: 'for' behaviors *)
+ let active = [] in (* TODO: 'for' behaviors, e-acsl#109 *)
let ppts = Property.ip_complete_of_spec kf kinstr ~active spec in
unsupported
(fun ppts ->
@@ -1307,7 +1308,8 @@ let translate_pre_code_annotation kf stmt env annot =
then not_yet env "variant"
else env
| AAssigns _ ->
- (* TODO: it is not a precondition *)
+ (* TODO: it is not a precondition --> should not be handled here,
+ to be fixed when implementing e-acsl#29 *)
let ppts = Property.ip_of_code_annot kf stmt annot in
List.iter
(fun ppt -> if must_translate ppt then not_yet env "assigns")
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index f5d08ec2813..703ef6b8c0d 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -20,16 +20,6 @@
(* *)
(**************************************************************************)
-let check () = assert false (* [TODO ARCHI] kill check *)
-
-let check =
- Dynamic.register
- ~plugin:"e-acsl"
- ~journalize:true
- "check"
- (Datatype.func Datatype.unit Datatype.bool)
- check
-
module Resulting_projects =
State_builder.Hashtbl
(Datatype.String.Hashtbl)
@@ -65,7 +55,6 @@ let generate_code =
if it is not yet computed *)
let rtl_prj_name = Options.Project_name.get () ^ " RTL" in
let rtl_prj = Project.create_by_copy ~last:false rtl_prj_name 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
@@ -94,7 +83,8 @@ let generate_code =
(* 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). *)
- (* [TODO ARCHI] what if RTE was already computed? *)
+ (* [TODO] what if RTE was already computed? To be fixed when
+ redoing the RTE management system *)
let selection =
State_selection.union
(State_selection.with_dependencies !Db.RteGen.self)
@@ -103,6 +93,7 @@ let generate_code =
Project.clear ~selection ~project:copied_prj ();
Resulting_projects.mark_as_computed ())
();
+ if not (Options.debug_atleast 1) then Project.remove ~project:rtl_prj ();
Options.feedback "translation done in project \"%s\"."
(Options.Project_name.get ());
copied_prj)
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 2b01ed8d9a8..2f167b55c03 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -372,7 +372,7 @@ let unduplicable_functions =
"__builtin_va_copy";
(* *alloc and free should not be duplicated. *)
(* [TODO:] it preserves the former behavior. Should be modified latter by
- checking only preconditions for any libc functions *)
+ checking only preconditions for any libc functions, see e-acsl#35 *)
"malloc";
"calloc";
"realloc";
--
GitLab