From 950ee5fb5a86cf200d6c7d5da96d2c8ae6561b80 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 5 Aug 2013 15:06:58 +0000
Subject: [PATCH] [E-ACSL] was mostly unusable since the last change of quantum
Filepath.normalize
---
src/plugins/e-acsl/TODO | 6 ++++++
src/plugins/e-acsl/doc/userman/introduction.tex | 2 +-
src/plugins/e-acsl/misc.ml | 6 ++++--
3 files changed, 11 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 7e86494adaa..02a9b6fff51 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -67,10 +67,16 @@
- interprétation des tableaux logiques
[Dillon] Windows
+[to be check]: no call to full_init or initialize for the assigned result of a
+function call
+
#######
# DOC #
#######
+- E_ACSL_MACHDEP with gcc -D
+- check of runtime error in combination with RTE
+
#########
# TESTS #
#########
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index 5427255fb71..bc01d261970 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -26,7 +26,7 @@ monitoring tools and static analysis tools like
Annotations must be written in the \eacsl specification
language~\cite{eacsl,sac13} which is a subset of \acsl. This plug-in is still in
-a preliminary state: some parts of E-ACSL are not yet supported. \eacsl
+a preliminary state: some parts of \eacsl are not yet supported. \eacsl
annotations currently handled by the \eacsl plug-in are documented in a
separated document~\cite{eacsl-implem}.
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 2946037d24f..3b119a93737 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -51,8 +51,10 @@ let reset () = Datatype.String.Hashtbl.clear library_functions
let mk_call ~loc ?result fname args =
let vi =
- try Datatype.String.Hashtbl.find library_functions fname
- with Not_found -> Options.fatal "unregistered library function `%s'" fname
+ try
+ Datatype.String.Hashtbl.find library_functions (Filepath.normalize fname)
+ with Not_found ->
+ Options.fatal "unregistered library function `%s'" fname
in
let f = Cil.evar ~loc vi in
vi.vreferenced <- true;
--
GitLab