diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO index 7e86494adaa0b67571a02a0025b4eaf782648974..02a9b6fff510979d5dd0920d7ae14825345a1419 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 5427255fb71de682dc4b7cad12e6af7160cd8639..bc01d261970768dde8e728e976796e2f417f2aef 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 2946037d24ffde555c65650eeaf4aca39c51f117..3b119a937373b92e2a2f9889a437acfd0960b5f5 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;