[E-ACSL] was mostly unusable since the last change of quantum Filepath.normalize

src/plugins/e-acsl/TODO

@@ -67,10 +67,16 @@
 - interprtation 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 #
 #########

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}.
 

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;