From b82378178899cd209de113ff39fd2b6117169359 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 14 Dec 2011 13:41:13 +0000
Subject: [PATCH] [e-acsl] license [e-acsl] do not stop anymore when detecting
an invalid/unsupported annotation [e-acsl] tests for invalid quantifications
---
src/plugins/e-acsl/Makefile.in | 2 +-
src/plugins/e-acsl/TODO | 1 -
src/plugins/e-acsl/env.ml | 2 +-
src/plugins/e-acsl/error.ml | 74 +++
src/plugins/e-acsl/error.mli | 44 ++
src/plugins/e-acsl/license/CEA_LGPL | 19 +
src/plugins/e-acsl/license/LGPLv2.1 | 458 ++++++++++++++++++
.../e-acsl/license/headache_config.txt | 79 +++
src/plugins/e-acsl/main.ml | 40 +-
src/plugins/e-acsl/misc.ml | 10 -
src/plugins/e-acsl/misc.mli | 11 -
.../e-acsl-reject/oracle/quantif.err.oracle | 0
.../e-acsl-reject/oracle/quantif.res.oracle | 29 ++
.../e-acsl-reject/oracle/valid.res.oracle | 6 +-
.../oracle/valid_index.res.oracle | 6 +-
.../oracle/valid_range.res.oracle | 6 +-
.../e-acsl/tests/e-acsl-reject/quantif.i | 15 +
.../e-acsl/tests/e-acsl-reject/test_config | 3 +-
.../e-acsl-runtime/oracle/ptr.res.oracle | 3 +-
.../e-acsl/tests/e-acsl-runtime/test_config | 2 +-
src/plugins/e-acsl/visit.ml | 166 +++----
21 files changed, 834 insertions(+), 142 deletions(-)
create mode 100644 src/plugins/e-acsl/error.ml
create mode 100644 src/plugins/e-acsl/error.mli
create mode 100644 src/plugins/e-acsl/license/CEA_LGPL
create mode 100644 src/plugins/e-acsl/license/LGPLv2.1
create mode 100644 src/plugins/e-acsl/license/headache_config.txt
create mode 100644 src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-reject/quantif.i
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 5921658b141..b088a3edf52 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -33,7 +33,7 @@ PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_E_ACSL@
PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@
PLUGIN_NAME:=E_ACSL
-PLUGIN_CMO:= local_config options read_header misc mpz env visit main
+PLUGIN_CMO:= local_config options read_header error misc mpz env visit main
PLUGIN_HAS_MLI:=yes
# Enable -warn-error, but do not distribute the plug-in with this option being
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 5ccdcdd35dd..6b2b9ea9597 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -4,7 +4,6 @@
- quantifications sur les entiers
- mixed assumes and ensures in contracts
-- pas d'arrêt brutal en cas de feature non implémentée
- utiliser Options.use_asserts
########
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 6cfb8e45018..bff968f74d4 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -283,7 +283,7 @@ let stmt_of_label env = function
| StmtLabel { contents = stmt } -> stmt
| LogicLabel(_, label) when label = "Here" ->
(match env.visitor#current_stmt with
- | None -> Misc.not_yet "label \"Here\" in function contract"
+ | None -> Error.not_yet "label \"Here\" in function contract"
| Some s -> s)
| LogicLabel(_, label) when label = "Old" || label = "Pre" ->
(try Kernel_function.find_first_stmt (Extlib.the env.visitor#current_kf)
diff --git a/src/plugins/e-acsl/error.ml b/src/plugins/e-acsl/error.ml
new file mode 100644
index 00000000000..dddcbfef537
--- /dev/null
+++ b/src/plugins/e-acsl/error.ml
@@ -0,0 +1,74 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the E-ACSL plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2011 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+exception Typing_error of string
+let untypable s = raise (Typing_error s)
+
+exception Not_yet of string
+let not_yet s = raise (Not_yet s)
+
+module Nb_typing =
+ State_builder.Ref
+ (Datatype.Int)
+ (struct
+ let name = "E_ACSL.Error.Nb_typing"
+ let default () = 0
+ let dependencies = [ Ast.self ]
+ let kind = `Correctness
+ end)
+
+let nb_untypable = Nb_typing.get
+
+module Nb_not_yet =
+ State_builder.Ref
+ (Datatype.Int)
+ (struct
+ let name = "E_ACSL.Error.Nb_not_yet"
+ let default () = 0
+ let dependencies = [ Ast.self ]
+ let kind = `Correctness
+ end)
+
+let nb_not_yet = Nb_not_yet.get
+
+let handle f x =
+ try
+ f x
+ with
+ | Typing_error s ->
+ let msg = Format.sprintf "@[invalid E-ACSL construct@ `%s'.@]" s in
+ Options.warning ~current:true "@[%s@ Ignoring annotation.@]" msg;
+ Nb_typing.set (Nb_typing.get () + 1);
+ x
+ | Not_yet s ->
+ let msg =
+ Format.sprintf "@[E-ACSL construct@ `%s'@ is not yet supported.@]" s
+ in
+ Options.warning ~current:true "@[%s@ Ignoring annotation.@]" msg;
+ Nb_not_yet.set (Nb_not_yet.get () + 1);
+ x
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)
diff --git a/src/plugins/e-acsl/error.mli b/src/plugins/e-acsl/error.mli
new file mode 100644
index 00000000000..c80ae7849a8
--- /dev/null
+++ b/src/plugins/e-acsl/error.mli
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the E-ACSL plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2011 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Handling errors. *)
+
+val untypable: string -> 'a
+(** type error built from the given argument. *)
+
+val not_yet: string -> 'a
+(** not_yet_implemented error built from the given argument. *)
+
+val handle: ('a -> 'a) -> 'a -> 'a
+(** run the closure with the given argument and handle potential errors. *)
+
+val nb_untypable: unit -> int
+(** Number of untypable annotations. *)
+
+val nb_not_yet: unit -> int
+(** Number of not-yet-supported annotations. *)
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)
diff --git a/src/plugins/e-acsl/license/CEA_LGPL b/src/plugins/e-acsl/license/CEA_LGPL
new file mode 100644
index 00000000000..7eeffb7c0c6
--- /dev/null
+++ b/src/plugins/e-acsl/license/CEA_LGPL
@@ -0,0 +1,19 @@
+
+This file is part of the E-ACSL plug-in of Frama-C.
+
+Copyright (C) 2011
+ CEA (Commissariat à l'énergie atomique et aux énergies
+ alternatives)
+
+you can redistribute it and/or modify it under the terms of the GNU
+Lesser General Public License as published by the Free Software
+Foundation, version 2.1.
+
+It is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU Lesser General Public License for more details.
+
+See the GNU Lesser General Public License version 2.1
+for more details (enclosed in the file licenses/LGPLv2.1).
+
diff --git a/src/plugins/e-acsl/license/LGPLv2.1 b/src/plugins/e-acsl/license/LGPLv2.1
new file mode 100644
index 00000000000..8c177f8bedc
--- /dev/null
+++ b/src/plugins/e-acsl/license/LGPLv2.1
@@ -0,0 +1,458 @@
+ GNU LESSER GENERAL PUBLIC LICENSE
+ Version 2.1, February 1999
+
+ Copyright (C) 1991, 1999 Free Software Foundation, Inc.
+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+[This is the first released version of the Lesser GPL. It also counts
+ as the successor of the GNU Library Public License, version 2, hence
+ the version number 2.1.]
+
+ Preamble
+
+ The licenses for most software are designed to take away your
+freedom to share and change it. By contrast, the GNU General Public
+Licenses are intended to guarantee your freedom to share and change
+free software--to make sure the software is free for all its users.
+
+ This license, the Lesser General Public License, applies to some
+specially designated software packages--typically libraries--of the
+Free Software Foundation and other authors who decide to use it. You
+can use it too, but we suggest you first think carefully about whether
+this license or the ordinary General Public License is the better
+strategy to use in any particular case, based on the explanations below.
+
+ When we speak of free software, we are referring to freedom of use,
+not price. Our General Public Licenses are designed to make sure that
+you have the freedom to distribute copies of free software (and charge
+for this service if you wish); that you receive source code or can get
+it if you want it; that you can change the software and use pieces of
+it in new free programs; and that you are informed that you can do
+these things.
+
+ To protect your rights, we need to make restrictions that forbid
+distributors to deny you these rights or to ask you to surrender these
+rights. These restrictions translate to certain responsibilities for
+you if you distribute copies of the library or if you modify it.
+
+ For example, if you distribute copies of the library, whether gratis
+or for a fee, you must give the recipients all the rights that we gave
+you. You must make sure that they, too, receive or can get the source
+code. If you link other code with the library, you must provide
+complete object files to the recipients, so that they can relink them
+with the library after making changes to the library and recompiling
+it. And you must show them these terms so they know their rights.
+
+ We protect your rights with a two-step method: (1) we copyright the
+library, and (2) we offer you this license, which gives you legal
+permission to copy, distribute and/or modify the library.
+
+ To protect each distributor, we want to make it very clear that
+there is no warranty for the free library. Also, if the library is
+modified by someone else and passed on, the recipients should know
+that what they have is not the original version, so that the original
+author's reputation will not be affected by problems that might be
+introduced by others.
+
+ Finally, software patents pose a constant threat to the existence of
+any free program. We wish to make sure that a company cannot
+effectively restrict the users of a free program by obtaining a
+restrictive license from a patent holder. Therefore, we insist that
+any patent license obtained for a version of the library must be
+consistent with the full freedom of use specified in this license.
+
+ Most GNU software, including some libraries, is covered by the
+ordinary GNU General Public License. This license, the GNU Lesser
+General Public License, applies to certain designated libraries, and
+is quite different from the ordinary General Public License. We use
+this license for certain libraries in order to permit linking those
+libraries into non-free programs.
+
+ When a program is linked with a library, whether statically or using
+a shared library, the combination of the two is legally speaking a
+combined work, a derivative of the original library. The ordinary
+General Public License therefore permits such linking only if the
+entire combination fits its criteria of freedom. The Lesser General
+Public License permits more lax criteria for linking other code with
+the library.
+
+ We call this license the "Lesser" General Public License because it
+does Less to protect the user's freedom than the ordinary General
+Public License. It also provides other free software developers Less
+of an advantage over competing non-free programs. These disadvantages
+are the reason we use the ordinary General Public License for many
+libraries. However, the Lesser license provides advantages in certain
+special circumstances.
+
+ For example, on rare occasions, there may be a special need to
+encourage the widest possible use of a certain library, so that it becomes
+a de-facto standard. To achieve this, non-free programs must be
+allowed to use the library. A more frequent case is that a free
+library does the same job as widely used non-free libraries. In this
+case, there is little to gain by limiting the free library to free
+software only, so we use the Lesser General Public License.
+
+ In other cases, permission to use a particular library in non-free
+programs enables a greater number of people to use a large body of
+free software. For example, permission to use the GNU C Library in
+non-free programs enables many more people to use the whole GNU
+operating system, as well as its variant, the GNU/Linux operating
+system.
+
+ Although the Lesser General Public License is Less protective of the
+users' freedom, it does ensure that the user of a program that is
+linked with the Library has the freedom and the wherewithal to run
+that program using a modified version of the Library.
+
+ The precise terms and conditions for copying, distribution and
+modification follow. Pay close attention to the difference between a
+"work based on the library" and a "work that uses the library". The
+former contains code derived from the library, whereas the latter must
+be combined with the library in order to run.
+
+ GNU LESSER GENERAL PUBLIC LICENSE
+ TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+ 0. This License Agreement applies to any software library or other
+program which contains a notice placed by the copyright holder or
+other authorized party saying it may be distributed under the terms of
+this Lesser General Public License (also called "this License").
+Each licensee is addressed as "you".
+
+ A "library" means a collection of software functions and/or data
+prepared so as to be conveniently linked with application programs
+(which use some of those functions and data) to form executables.
+
+ The "Library", below, refers to any such software library or work
+which has been distributed under these terms. A "work based on the
+Library" means either the Library or any derivative work under
+copyright law: that is to say, a work containing the Library or a
+portion of it, either verbatim or with modifications and/or translated
+straightforwardly into another language. (Hereinafter, translation is
+included without limitation in the term "modification".)
+
+ "Source code" for a work means the preferred form of the work for
+making modifications to it. For a library, complete source code means
+all the source code for all modules it contains, plus any associated
+interface definition files, plus the scripts used to control compilation
+and installation of the library.
+
+ Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope. The act of
+running a program using the Library is not restricted, and output from
+such a program is covered only if its contents constitute a work based
+on the Library (independent of the use of the Library in a tool for
+writing it). Whether that is true depends on what the Library does
+and what the program that uses the Library does.
+
+ 1. You may copy and distribute verbatim copies of the Library's
+complete source code as you receive it, in any medium, provided that
+you conspicuously and appropriately publish on each copy an
+appropriate copyright notice and disclaimer of warranty; keep intact
+all the notices that refer to this License and to the absence of any
+warranty; and distribute a copy of this License along with the
+Library.
+
+ You may charge a fee for the physical act of transferring a copy,
+and you may at your option offer warranty protection in exchange for a
+fee.
+
+ 2. You may modify your copy or copies of the Library or any portion
+of it, thus forming a work based on the Library, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+ a) The modified work must itself be a software library.
+
+ b) You must cause the files modified to carry prominent notices
+ stating that you changed the files and the date of any change.
+
+ c) You must cause the whole of the work to be licensed at no
+ charge to all third parties under the terms of this License.
+
+ d) If a facility in the modified Library refers to a function or a
+ table of data to be supplied by an application program that uses
+ the facility, other than as an argument passed when the facility
+ is invoked, then you must make a good faith effort to ensure that,
+ in the event an application does not supply such function or
+ table, the facility still operates, and performs whatever part of
+ its purpose remains meaningful.
+
+ (For example, a function in a library to compute square roots has
+ a purpose that is entirely well-defined independent of the
+ application. Therefore, Subsection 2d requires that any
+ application-supplied function or table used by this function must
+ be optional: if the application does not supply it, the square
+ root function must still compute square roots.)
+
+These requirements apply to the modified work as a whole. If
+identifiable sections of that work are not derived from the Library,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works. But when you
+distribute the same sections as part of a whole which is a work based
+on the Library, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote
+it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Library.
+
+In addition, mere aggregation of another work not based on the Library
+with the Library (or with a work based on the Library) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+ 3. You may opt to apply the terms of the ordinary GNU General Public
+License instead of this License to a given copy of the Library. To do
+this, you must alter all the notices that refer to this License, so
+that they refer to the ordinary GNU General Public License, version 2,
+instead of to this License. (If a newer version than version 2 of the
+ordinary GNU General Public License has appeared, then you can specify
+that version instead if you wish.) Do not make any other change in
+these notices.
+
+ Once this change is made in a given copy, it is irreversible for
+that copy, so the ordinary GNU General Public License applies to all
+subsequent copies and derivative works made from that copy.
+
+ This option is useful when you wish to copy part of the code of
+the Library into a program that is not a library.
+
+ 4. You may copy and distribute the Library (or a portion or
+derivative of it, under Section 2) in object code or executable form
+under the terms of Sections 1 and 2 above provided that you accompany
+it with the complete corresponding machine-readable source code, which
+must be distributed under the terms of Sections 1 and 2 above on a
+medium customarily used for software interchange.
+
+ If distribution of object code is made by offering access to copy
+from a designated place, then offering equivalent access to copy the
+source code from the same place satisfies the requirement to
+distribute the source code, even though third parties are not
+compelled to copy the source along with the object code.
+
+ 5. A program that contains no derivative of any portion of the
+Library, but is designed to work with the Library by being compiled or
+linked with it, is called a "work that uses the Library". Such a
+work, in isolation, is not a derivative work of the Library, and
+therefore falls outside the scope of this License.
+
+ However, linking a "work that uses the Library" with the Library
+creates an executable that is a derivative of the Library (because it
+contains portions of the Library), rather than a "work that uses the
+library". The executable is therefore covered by this License.
+Section 6 states terms for distribution of such executables.
+
+ When a "work that uses the Library" uses material from a header file
+that is part of the Library, the object code for the work may be a
+derivative work of the Library even though the source code is not.
+Whether this is true is especially significant if the work can be
+linked without the Library, or if the work is itself a library. The
+threshold for this to be true is not precisely defined by law.
+
+ If such an object file uses only numerical parameters, data
+structure layouts and accessors, and small macros and small inline
+functions (ten lines or less in length), then the use of the object
+file is unrestricted, regardless of whether it is legally a derivative
+work. (Executables containing this object code plus portions of the
+Library will still fall under Section 6.)
+
+ Otherwise, if the work is a derivative of the Library, you may
+distribute the object code for the work under the terms of Section 6.
+Any executables containing that work also fall under Section 6,
+whether or not they are linked directly with the Library itself.
+
+ 6. As an exception to the Sections above, you may also combine or
+link a "work that uses the Library" with the Library to produce a
+work containing portions of the Library, and distribute that work
+under terms of your choice, provided that the terms permit
+modification of the work for the customer's own use and reverse
+engineering for debugging such modifications.
+
+ You must give prominent notice with each copy of the work that the
+Library is used in it and that the Library and its use are covered by
+this License. You must supply a copy of this License. If the work
+during execution displays copyright notices, you must include the
+copyright notice for the Library among them, as well as a reference
+directing the user to the copy of this License. Also, you must do one
+of these things:
+
+ a) Accompany the work with the complete corresponding
+ machine-readable source code for the Library including whatever
+ changes were used in the work (which must be distributed under
+ Sections 1 and 2 above); and, if the work is an executable linked
+ with the Library, with the complete machine-readable "work that
+ uses the Library", as object code and/or source code, so that the
+ user can modify the Library and then relink to produce a modified
+ executable containing the modified Library. (It is understood
+ that the user who changes the contents of definitions files in the
+ Library will not necessarily be able to recompile the application
+ to use the modified definitions.)
+
+ b) Use a suitable shared library mechanism for linking with the
+ Library. A suitable mechanism is one that (1) uses at run time a
+ copy of the library already present on the user's computer system,
+ rather than copying library functions into the executable, and (2)
+ will operate properly with a modified version of the library, if
+ the user installs one, as long as the modified version is
+ interface-compatible with the version that the work was made with.
+
+ c) Accompany the work with a written offer, valid for at
+ least three years, to give the same user the materials
+ specified in Subsection 6a, above, for a charge no more
+ than the cost of performing this distribution.
+
+ d) If distribution of the work is made by offering access to copy
+ from a designated place, offer equivalent access to copy the above
+ specified materials from the same place.
+
+ e) Verify that the user has already received a copy of these
+ materials or that you have already sent this user a copy.
+
+ For an executable, the required form of the "work that uses the
+Library" must include any data and utility programs needed for
+reproducing the executable from it. However, as a special exception,
+the materials to be distributed need not include anything that is
+normally distributed (in either source or binary form) with the major
+components (compiler, kernel, and so on) of the operating system on
+which the executable runs, unless that component itself accompanies
+the executable.
+
+ It may happen that this requirement contradicts the license
+restrictions of other proprietary libraries that do not normally
+accompany the operating system. Such a contradiction means you cannot
+use both them and the Library together in an executable that you
+distribute.
+
+ 7. You may place library facilities that are a work based on the
+Library side-by-side in a single library together with other library
+facilities not covered by this License, and distribute such a combined
+library, provided that the separate distribution of the work based on
+the Library and of the other library facilities is otherwise
+permitted, and provided that you do these two things:
+
+ a) Accompany the combined library with a copy of the same work
+ based on the Library, uncombined with any other library
+ facilities. This must be distributed under the terms of the
+ Sections above.
+
+ b) Give prominent notice with the combined library of the fact
+ that part of it is a work based on the Library, and explaining
+ where to find the accompanying uncombined form of the same work.
+
+ 8. You may not copy, modify, sublicense, link with, or distribute
+the Library except as expressly provided under this License. Any
+attempt otherwise to copy, modify, sublicense, link with, or
+distribute the Library is void, and will automatically terminate your
+rights under this License. However, parties who have received copies,
+or rights, from you under this License will not have their licenses
+terminated so long as such parties remain in full compliance.
+
+ 9. You are not required to accept this License, since you have not
+signed it. However, nothing else grants you permission to modify or
+distribute the Library or its derivative works. These actions are
+prohibited by law if you do not accept this License. Therefore, by
+modifying or distributing the Library (or any work based on the
+Library), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Library or works based on it.
+
+ 10. Each time you redistribute the Library (or any work based on the
+Library), the recipient automatically receives a license from the
+original licensor to copy, distribute, link with or modify the Library
+subject to these terms and conditions. You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties with
+this License.
+
+ 11. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues),
+conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License. If you cannot
+distribute so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you
+may not distribute the Library at all. For example, if a patent
+license would not permit royalty-free redistribution of the Library by
+all those who receive copies directly or indirectly through you, then
+the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Library.
+
+If any portion of this section is held invalid or unenforceable under any
+particular circumstance, the balance of the section is intended to apply,
+and the section as a whole is intended to apply in other circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system which is
+implemented by public license practices. Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+
+ 12. If the distribution and/or use of the Library is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Library under this License may add
+an explicit geographical distribution limitation excluding those countries,
+so that distribution is permitted only in or among countries not thus
+excluded. In such case, this License incorporates the limitation as if
+written in the body of this License.
+
+ 13. The Free Software Foundation may publish revised and/or new
+versions of the Lesser General Public License from time to time.
+Such new versions will be similar in spirit to the present version,
+but may differ in detail to address new problems or concerns.
+
+Each version is given a distinguishing version number. If the Library
+specifies a version number of this License which applies to it and
+"any later version", you have the option of following the terms and
+conditions either of that version or of any later version published by
+the Free Software Foundation. If the Library does not specify a
+license version number, you may choose any version ever published by
+the Free Software Foundation.
+
+ 14. If you wish to incorporate parts of the Library into other free
+programs whose distribution conditions are incompatible with these,
+write to the author to ask for permission. For software which is
+copyrighted by the Free Software Foundation, write to the Free
+Software Foundation; we sometimes make exceptions for this. Our
+decision will be guided by the two goals of preserving the free status
+of all derivatives of our free software and of promoting the sharing
+and reuse of software generally.
+
+ NO WARRANTY
+
+ 15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO
+WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW.
+EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR
+OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY
+KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
+LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME
+THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+ 16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN
+WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY
+AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU
+FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR
+CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE
+LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING
+RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A
+FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF
+SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH
+DAMAGES.
+
+ END OF TERMS AND CONDITIONS
diff --git a/src/plugins/e-acsl/license/headache_config.txt b/src/plugins/e-acsl/license/headache_config.txt
new file mode 100644
index 00000000000..f95c9f51b85
--- /dev/null
+++ b/src/plugins/e-acsl/license/headache_config.txt
@@ -0,0 +1,79 @@
+##################
+# Objective Caml #
+##################
+| ".*\.mly" -> frame open:"/*" line:"*" close:"*/"
+| ".*\.ml[il4]?.*" -> frame open:"(*" line:"*" close:"*)"
+
+############
+# C source #
+############
+| ".*\.h" -> frame open:"/*" line:"*" close:"*/"
+| ".*\.c" -> frame open:"/*" line:"*" close:"*/"
+| ".*\.ast" -> frame open:"//" line:" " close:" "
+| ".*\.cc" -> frame open:"/*" line:"*" close:"*/"
+| "perfcount.c.in" -> frame open: "/*" line: "*" close: "*/"
+
+#######
+# Asm #
+#######
+| ".*\.S" -> frame open:"/*" line:"*" close:"*/"
+
+#############
+# Configure #
+#############
+| ".*config\.h\.in" -> frame open:"/*" line:"*" close:"*/"
+| ".*configure\..*" -> frame open:"#" line:"#" close:"#"
+
+############
+# Makefile #
+############
+| ".*Makefile\..*" -> frame open:"#" line:"#" close:"#"
+
+#################
+# Shell scripts #
+#################
+| ".*\.sh" -> frame open:"#" line:"#" close:"#"
+
+#########################
+# MS-Windows Ressources #
+#########################
+| ".*\.rc" -> frame open:"#" line:"#" close:"#"
+
+#############
+# man pages #
+#############
+| ".*\.[1-9]" -> frame open:".\\\"" line: " " close:""
+
+#############
+# Why files #
+#############
+| ".*\.why" -> frame open: "(*" line: "*" close: "*)"
+| ".*\.why\.src" -> frame open: "(*" line: "*" close: "*)"
+
+#############
+# Coq files #
+#############
+| ".*\.v" -> frame open: "(*" line: "*" close: "*)"
+
+########
+# HTML #
+########
+| ".*\.htm.*" -> frame open: "<!--" line: " " close: "-->"
+
+#######
+# CSS #
+#######
+| ".*\.css" -> frame open: "/*" line: "*" close: "*/"
+# plug-in's ocamldoc introductions
+| "intro_.*\.txt" -> frame open: "@ignore" line: " " close: ""
+
+##############
+# Emacs Lisp #
+##############
+| ".*\.el" -> frame open: ";" line: ";" close:";"
+
+##############
+# Misc files #
+##############
+| "make_release" -> frame open:"#" line:"#" close:"#"
+| "FAQ" -> frame open:"#" line:"#" close:"#"
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index b8a50f3edfb..5a5e829aabb 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -21,12 +21,19 @@
(**************************************************************************)
let check () =
- try
- Visitor.visitFramacFileSameGlobals (Visit.do_visit false) (Ast.get ());
- true
- with Misc.Typing_error s ->
- Options.error ~current:true "%s" s;
- false
+ Visitor.visitFramacFileSameGlobals (Visit.do_visit false) (Ast.get ());
+ let t = Error.nb_untypable () in
+ let n = Error.nb_not_yet () in
+ let print msg n =
+ Options.result "@[%d annotation%s %s ignored,@ being %s.@]"
+ n
+ (if n > 1 then "s" else "")
+ (if n > 1 then "were" else "was")
+ msg
+ in
+ print "untypable" t;
+ print "unsupported" n;
+ n + t = 0
let check =
Dynamic.register
@@ -36,18 +43,6 @@ let check =
(Datatype.func Datatype.unit Datatype.bool)
check
-let fail_check () =
- try Visitor.visitFramacFileSameGlobals (Visit.do_visit false) (Ast.get ());
- with Misc.Typing_error s -> Options.abort ~current:true "%s" s
-
-let fail_check =
- Dynamic.register
- ~plugin:"e-acsl"
- ~journalize:true
- "fail_check"
- (Datatype.func Datatype.unit Datatype.unit)
- fail_check
-
module Resulting_projects =
State_builder.Hashtbl
(Datatype.String.Hashtbl)
@@ -64,11 +59,8 @@ let () = Env.global_state := Resulting_projects.self
let generate_code =
Resulting_projects.memo
(fun name ->
- try
- let visit prj = Visit.do_visit ~prj true in
- File.create_rebuilt_project_from_visitor ~preprocess:false name visit
- with Misc.Typing_error s ->
- Options.abort ~current:true "%s" s)
+ let visit prj = Visit.do_visit ~prj true in
+ File.create_rebuilt_project_from_visitor ~preprocess:false name visit)
let generate_code =
Dynamic.register
@@ -82,7 +74,7 @@ let main () =
if Options.Run.get () then
ignore (generate_code (Options.Project_name.get ()))
else
- if Options.Check.get () then fail_check ()
+ if Options.Check.get () then ignore (check ())
let () = Db.Main.extend main
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 04141e994d6..d0a067d8a20 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -24,16 +24,6 @@ open Cil_types
open Cil_datatype
open Cil
-(* ************************************************************************** *)
-(** {2 Handling errors} *)
-(* ************************************************************************** *)
-
-exception Typing_error of string
-let type_error s = raise (Typing_error s)
-
-let not_yet s =
- Options.not_yet_implemented "construct `%s' is not yet supported." s
-
(* ************************************************************************** *)
(** {2 Builders} *)
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 41459349e6b..cc77f4e29a9 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -25,17 +25,6 @@
open Cil_types
open Cil_datatype
-(* ************************************************************************** *)
-(** {2 Handling errors} *)
-(* ************************************************************************** *)
-
-exception Typing_error of string
-val type_error: string -> 'a
-(** @raise Typing_error with with a message built from the given one. *)
-
-val not_yet: string -> 'a
-(** @raise Log.FeatureRequest with a message built from the given one. *)
-
(* ************************************************************************** *)
(** {2 Builders} *)
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.err.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle
new file mode 100644
index 00000000000..bd9b453acb5
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle
@@ -0,0 +1,29 @@
+tests/e-acsl-reject/quantif.i:6:[e-acsl] warning: E-ACSL construct `unguarded \forall quantification' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-reject/quantif.i:7:[e-acsl] warning: invalid E-ACSL construct
+ `invalid guard (x ≡ 1) in quantification (∀ ℤ x; x ≡ 1 ⇒ x ≥ 0)'.
+ Ignoring annotation.
+tests/e-acsl-reject/quantif.i:8:[e-acsl] warning: invalid E-ACSL construct
+ `invalid guard (0 ≤ x) in quantification (∀ int x; 0 ≤ x ⇒ x ≥ 0)'.
+ Ignoring annotation.
+tests/e-acsl-reject/quantif.i:9:[e-acsl] warning: invalid E-ACSL construct
+ `non integer variable x in quantification (∀ float x; 0 ≤ x ∧ x ≤ 3 ⇒ x ≥ 0)'.
+ Ignoring annotation.
+tests/e-acsl-reject/quantif.i:10:[e-acsl] warning: invalid E-ACSL construct
+ `unguarded variable y in quantification
+ (∀ ℤ x, ℤ y; 0 ≤ x ∧ x ≤ 3 ⇒ x ≥ 0)'.
+ Ignoring annotation.
+tests/e-acsl-reject/quantif.i:11:[e-acsl] warning: invalid E-ACSL construct
+ `unquantified variable z in quantification
+ (∀ ℤ x; (0 ≤ x ∧ x ≤ 3) ∧ (0 ≤ z ∧ z ≤ 3) ⇒ x ≥ 0)'.
+ Ignoring annotation.
+tests/e-acsl-reject/quantif.i:12:[e-acsl] warning: invalid E-ACSL construct
+ `invalid guard ((0 ≤ x ∧ x ≤ 3) ∨ (0 ≤ y ∧ y ≤ 3)) in quantification
+ (∀ ℤ x, ℤ y; (0 ≤ x ∧ x ≤ 3) ∨ (0 ≤ y ∧ y ≤ 3) ⇒
+ x ≥ 0)'.
+ Ignoring annotation.
+tests/e-acsl-reject/quantif.i:13:[e-acsl] warning: invalid E-ACSL construct
+ `invalid binder x+1 in quantification (∀ int x; 0 ≤ x+1 ∧ x+1 ≤ 3 ⇒ x ≥ 0)'.
+ Ignoring annotation.
+[e-acsl] 7 annotations were ignored, being untypable.
+[e-acsl] 1 annotation was ignored, being unsupported.
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid.res.oracle
index b391ab242f1..ed5525515ce 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid.res.oracle
@@ -1,3 +1,3 @@
-[kernel] Plug-in e-acsl aborted because of unimplemented feature.
- Please send a feature request at http://bts.frama-c.com with:
- '[Plug-in e-acsl] construct `\valid' is not yet supported.'.
+tests/e-acsl-reject/valid.i:5:[e-acsl] warning: E-ACSL construct `\valid' is not yet supported. Ignoring annotation.
+[e-acsl] 0 annotation was ignored, being untypable.
+[e-acsl] 1 annotation was ignored, being unsupported.
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle
index c2f59365f05..ef4250bb9ab 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle
@@ -1,3 +1,3 @@
-[kernel] Plug-in e-acsl aborted because of unimplemented feature.
- Please send a feature request at http://bts.frama-c.com with:
- '[Plug-in e-acsl] construct `\valid_index' is not yet supported.'.
+tests/e-acsl-reject/valid_index.i:5:[e-acsl] warning: E-ACSL construct `\valid_index' is not yet supported. Ignoring annotation.
+[e-acsl] 0 annotation was ignored, being untypable.
+[e-acsl] 1 annotation was ignored, being unsupported.
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle
index 211e09903d7..b8208d3c1a5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle
@@ -1,3 +1,3 @@
-[kernel] Plug-in e-acsl aborted because of unimplemented feature.
- Please send a feature request at http://bts.frama-c.com with:
- '[Plug-in e-acsl] construct `\valid_range' is not yet supported.'.
+tests/e-acsl-reject/valid_range.i:5:[e-acsl] warning: E-ACSL construct `\valid_range' is not yet supported. Ignoring annotation.
+[e-acsl] 0 annotation was ignored, being untypable.
+[e-acsl] 1 annotation was ignored, being unsupported.
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/quantif.i b/src/plugins/e-acsl/tests/e-acsl-reject/quantif.i
new file mode 100644
index 00000000000..3e460b7e88f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/quantif.i
@@ -0,0 +1,15 @@
+/* run.config
+ COMMENT: invalid quantifications */
+
+int main(void) {
+ int z;
+ /*@ assert \forall integer x; x >= 0; */
+ /*@ assert \forall integer x; x == 1 ==> x >= 0; */
+ /*@ assert \forall int x; 0 <= x ==> x >= 0; */
+ /*@ assert \forall float x; 0 <= x <= 3 ==> x >= 0; */
+ /*@ assert \forall integer x,y; 0 <= x <= 3 ==> x >= 0; */
+ /*@ assert \forall integer x; 0 <= x <= 3 && 0 <= z <= 3 ==> x >= 0; */
+ /*@ assert \forall integer x,y; 0 <= x <= 3 || 0 <= y <= 3 ==> x >= 0; */
+ /*@ assert \forall int x; 0 <= x+1 <= 3 ==> x >= 0; */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/test_config b/src/plugins/e-acsl/tests/e-acsl-reject/test_config
index 475ef57bff2..61e3a7b0e53 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/test_config
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/test_config
@@ -1,2 +1 @@
-COMMENT: -e-acsl-check set by default
-STDOPT:
+OPT: -e-acsl-check
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index ac8c48cf39b..a630f5884f7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -2,7 +2,8 @@ tests/e-acsl-runtime/ptr.i:12:[e-acsl] warning: missing guard for ensuring that
:0:[e-acsl] warning: missing guard for ensuring that 0 is a valid array index
tests/e-acsl-runtime/ptr.i:14:[e-acsl] warning: missing guard for ensuring that 2 is a valid array index
tests/e-acsl-runtime/ptr.i:15:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
-:0:[e-acsl] warning: missing guard for ensuring that (2*sizeof(int))/sizeof((int)0x0) is a valid array index
+:0:[e-acsl] warning: missing guard for ensuring that
+ (2*sizeof(int))/sizeof((int)0x0) is a valid array index
tests/e-acsl-runtime/ptr.i:18:[e-acsl] warning: missing guard for ensuring that i is a valid array index
tests/e-acsl-runtime/ptr.i:19:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
:0:[e-acsl] warning: missing guard for ensuring that 2-i is a valid array index
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
index d49b6f0ad28..adc00e63922 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
@@ -1 +1 @@
-STDOPT: +"-e-acsl" +"-then-on e-acsl" +"-check" +"-print" +"-val"
+OPT: -e-acsl -then-on e-acsl -check -print -val
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index d80583ce8e4..0e4355f4d0d 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -49,7 +49,8 @@ let context_sensitive ?loc env ctx is_mpz_string t_opt e =
Options.warning
?source:(Extlib.opt_map fst loc)
~once:true
- "missing guard for ensuring that the given integer is C-representable";
+ "@[missing guard for ensuring that the given integer is \
+C-representable@]";
Env.new_var
env
None
@@ -143,10 +144,10 @@ let compute_quantif_guards quantif bounded_vars hyps =
let error msg pp x =
let msg1 = Pretty_utils.sfprintf msg pp x in
let msg2 =
- Pretty_utils.sfprintf " in guarded quantification %a"
+ Pretty_utils.sfprintf "@[ in quantification@ %a@]"
d_predicate_named quantif
in
- Misc.type_error (msg1 ^ msg2)
+ Error.untypable (msg1 ^ msg2)
in
let vars =
let h = Logic_var.Hashtbl.create 7 in
@@ -157,7 +158,7 @@ let compute_quantif_guards quantif bounded_vars hyps =
| Ctype ty when isIntegralType ty -> ()
| Linteger -> ()
| Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
- error "non integer variable %a" d_logic_var v);
+ error "@[non integer variable %a@]" d_logic_var v);
Logic_var.Hashtbl.add h v ())
bounded_vars;
h
@@ -174,13 +175,13 @@ let compute_quantif_guards quantif bounded_vars hyps =
Logic_var.Hashtbl.replace used_vars x1 ();
(t11, r1, x1, r2, t22) :: acc
end else
- error "unbound variable %a" d_logic_var x1
+ error "@[unquantified variable %a@]" d_logic_var x1
else
- error "invalid guard %a" d_term t21
- | TLval _, _ -> error "invalid guard %a" d_term t21
- | _, _ -> error "invalid guard %a" d_term t12)
+ error "@[invalid binder %a@]" d_term t21
+ | TLval _, _ -> error "@[invalid binder %a@]" d_term t21
+ | _, _ -> error "@[invalid binder %a@]" d_term t12)
| Pand(p1, p2) -> aux (aux acc p2) p1
- | _ -> error "invalid guard %a" d_predicate_named p
+ | _ -> error "@[invalid guard %a@]" d_predicate_named p
in
aux [] p
in
@@ -193,15 +194,15 @@ let compute_quantif_guards quantif bounded_vars hyps =
if len > 0 then begin
let msg =
Pretty_utils.sfprintf
- "unguarded variable%s %tin quantification %a"
+ "@[unguarded variable%s %tin quantification@ %a@]"
(if len = 1 then "" else "s")
(fun fmt ->
Logic_var.Hashtbl.iter
- (fun v () -> Format.fprintf fmt "%a " d_logic_var v)
+ (fun v () -> Format.fprintf fmt "@[%a @]" d_logic_var v)
vars)
d_predicate_named quantif
in
- Misc.type_error msg
+ Error.untypable msg
end;
guards
@@ -229,7 +230,7 @@ let rec thost_to_host env = function
| TMem t ->
let e, env = term_to_exp env (Ctype intType) t in
Options.warning ~source:(fst e.eloc) ~once:true
- "missing guard for ensuring that %a is a valid memory access"
+ "@[missing guard for ensuring that@ %a is a valid memory access@]"
d_term t;
Mem e, env
@@ -242,7 +243,7 @@ and toffset_to_offset ?loc env = function
| TIndex(t, offset) ->
let e, env = term_to_exp env (Ctype intType) t in
Options.warning ~source:(fst e.eloc) ~once:true
- "missing guard for ensuring that %a is a valid array index"
+ "@[missing guard for ensuring that@ %a is a valid array index@]"
d_term t;
let offset, env = toffset_to_offset env offset in
Index(e, offset), env
@@ -343,10 +344,10 @@ and context_insensitive_term_to_exp env t =
e, env, false
| TBinOp((Shiftlt | Shiftrt), _, _) ->
(* left/right shift *)
- Misc.not_yet "left/right shift"
+ Error.not_yet "left/right shift"
| TBinOp((LOr | LAnd | BOr | BXor | BAnd), _, _) ->
(* other logic/arith operators *)
- Misc.not_yet "missing binary operator"
+ Error.not_yet "missing binary operator"
| TBinOp(PlusPI | IndexPI | MinusPI | MinusPP as bop, t1, t2) ->
(* binary operation over pointers *)
(* [TODO] untested *)
@@ -359,7 +360,7 @@ and context_insensitive_term_to_exp env t =
let e1, env = term_to_exp env (ctx_type t1) t1 in
let e2, env = term_to_exp env (ctx_type t2) t2 in
Options.warning ~source:(fst loc) ~once:true
- "missing guard for ensuring that %a is a valid pointer"
+ "@[missing guard for ensuring that@ %a is a valid pointer@]"
d_term t;
(* the type of the result is the same than type of the pointer [e1],
whatever is [e2] *)
@@ -373,10 +374,10 @@ and context_insensitive_term_to_exp env t =
| TStartOf lv ->
let lv, env = tlval_to_lval env lv in
mkAddrOrStartOf ~loc lv, env, false
- | Tapp _ -> Misc.not_yet "applying logic function"
- | Tlambda _ -> Misc.not_yet "functional"
- | TDataCons _ -> Misc.not_yet "constructor"
- | Tif _ -> Misc.not_yet "conditional"
+ | Tapp _ -> Error.not_yet "applying logic function"
+ | Tlambda _ -> Error.not_yet "functional"
+ | TDataCons _ -> Error.not_yet "constructor"
+ | Tif _ -> Error.not_yet "conditional"
| Tat(t', label) ->
let stmt = Env.stmt_of_label env label in
let ty = t'.term_type in
@@ -431,20 +432,20 @@ and context_insensitive_term_to_exp env t =
let new_stmt = Visitor.visitFramacStmt o (get_stmt bhv stmt) in
set_stmt bhv stmt new_stmt;
res, !env_ref, false
- | Tbase_addr _ -> Misc.not_yet "\\base_addr"
- | Tblock_length _ -> Misc.not_yet "\\block_length"
+ | Tbase_addr _ -> Error.not_yet "\\base_addr"
+ | Tblock_length _ -> Error.not_yet "\\block_length"
| Tnull -> mkCast (zero ~loc) (TPtr(TVoid [], [])), env, false
- | TCoerce _ -> Misc.not_yet "coercion" (* Jessie specific *)
- | TCoerceE _ -> Misc.not_yet "expression coercion" (* Jessie specific *)
- | TUpdate _ -> Misc.not_yet "functional update"
- | Ttypeof _ -> Misc.not_yet "typeof"
- | Ttype _ -> Misc.not_yet "C type"
- | Tempty_set -> Misc.not_yet "empty tset"
- | Tunion _ -> Misc.not_yet "union of tsets"
- | Tinter _ -> Misc.not_yet "intersection of tsets"
- | Tcomprehension _ -> Misc.not_yet "tset comprehension"
- | Trange _ -> Misc.not_yet "range"
- | Tlet _ -> Misc.not_yet "let binding"
+ | TCoerce _ -> Error.not_yet "coercion" (* Jessie specific *)
+ | TCoerceE _ -> Error.not_yet "expression coercion" (* Jessie specific *)
+ | TUpdate _ -> Error.not_yet "functional update"
+ | Ttypeof _ -> Error.not_yet "typeof"
+ | Ttype _ -> Error.not_yet "C type"
+ | Tempty_set -> Error.not_yet "empty tset"
+ | Tunion _ -> Error.not_yet "union of tsets"
+ | Tinter _ -> Error.not_yet "intersection of tsets"
+ | Tcomprehension _ -> Error.not_yet "tset comprehension"
+ | Trange _ -> Error.not_yet "range"
+ | Tlet _ -> Error.not_yet "let binding"
(* Convert an ACSL term into a corresponding C expression (if any) in the given
environment. Also extend this environment in order to include the generating
@@ -490,8 +491,8 @@ let rec named_predicate_to_exp env p =
match p.content with
| Pfalse -> zero ~loc, env
| Ptrue -> one ~loc, env
- | Papp _ -> Misc.not_yet "logic function application"
- | Pseparated _ -> Misc.not_yet "separated"
+ | Papp _ -> Error.not_yet "logic function application"
+ | Pseparated _ -> Error.not_yet "separated"
| Prel(rel, t1, t2) ->
let e, env =
comparison_to_exp ~loc env (relation_to_binop rel) t1 t2 None
@@ -535,15 +536,15 @@ let rec named_predicate_to_exp env p =
Env.pop_and_get env2 s ~global_clear:false Env.Middle
in
[ mkStmt ~valid_sid:true (If(e1, then_block, else_block, loc)) ])
- | Pxor _ -> Misc.not_yet "xor"
+ | Pxor _ -> Error.not_yet "xor"
| Pimplies(p1, p2) ->
named_predicate_to_exp env (Logic_const.por ((Logic_const.pnot p1), p2))
- | Piff _ -> Misc.not_yet "<==>"
+ | Piff _ -> Error.not_yet "<==>"
| Pnot p ->
let e, env = named_predicate_to_exp env p in
new_exp ~loc (UnOp(LNot, e, TInt(IInt, []))), env
- | Pif _ -> Misc.not_yet "_ ? _ : _"
- | Plet _ -> Misc.not_yet "let _ = _ in _"
+ | Pif _ -> Error.not_yet "_ ? _ : _"
+ | Plet _ -> Error.not_yet "let _ = _ in _"
| Pforall(bounded_vars, { content = Pimplies(hyps, goal) }) ->
(* universal quantification over integers (or a subtype of integer) *)
let guards = compute_quantif_guards p bounded_vars hyps in
@@ -652,8 +653,8 @@ let rec named_predicate_to_exp env p =
let env = Env.add_stmt env end_loop in
let env = List.fold_left Env.Logic_binding.remove env bounded_vars in
res, env
- | Pforall _ -> Misc.not_yet "unguarded \\forall quantification"
- | Pexists(bounded_vars, { content = Pand(hyps, _goal) }) ->
+ | Pforall _ -> Error.not_yet "unguarded \\forall quantification"
+(* | Pexists(bounded_vars, { content = Pand(hyps, _goal) }) ->
let guards = compute_quantif_guards p bounded_vars hyps in
List.iter
(fun (t1, _, x, _, t2) ->
@@ -661,15 +662,15 @@ let rec named_predicate_to_exp env p =
"getting %a OP %a OP %a"
d_term t1 d_logic_var x d_term t2)
guards;
- assert false
- | Pexists _ -> Misc.not_yet "unguarded \\exists quantification"
- | Pat _ -> Misc.not_yet "\\at"
- | Pvalid _ -> Misc.not_yet "\\valid"
- | Pvalid_index _ -> Misc.not_yet "\\valid_index"
- | Pvalid_range _ -> Misc.not_yet "\\valid_range"
- | Pfresh _ -> Misc.not_yet "\\fresh"
- | Psubtype _ -> Misc.not_yet "subtyping relation" (* Jessie specific? *)
- | Pinitialized _ -> Misc.not_yet "\\initialized"
+ assert false*)
+ | Pexists _ -> Error.not_yet "unguarded \\exists quantification"
+ | Pat _ -> Error.not_yet "\\at"
+ | Pvalid _ -> Error.not_yet "\\valid"
+ | Pvalid_index _ -> Error.not_yet "\\valid_index"
+ | Pvalid_range _ -> Error.not_yet "\\valid_range"
+ | Pfresh _ -> Error.not_yet "\\fresh"
+ | Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
+ | Pinitialized _ -> Error.not_yet "\\initialized"
(* ************************************************************************** *)
(* [convert_*] converts a given ACSL annotation into the corresponding C
@@ -702,32 +703,38 @@ let convert_postconditions env behaviors =
List.fold_left
(fun env (t, p) ->
if b.b_assigns <> WritesAny then
- Misc.not_yet "assigns clause in behavior";
+ Error.not_yet "assigns clause in behavior";
if b.b_extended <> [] then
- Misc.not_yet "grammar extensions in behavior";
+ Error.not_yet "grammar extensions in behavior";
match t with
| Normal ->
let p = p.ip_content in
if p <> Ptrue && b.b_assumes <> [] then
- Misc.not_yet "assumes in conjunction with ensures in behaviors";
+ Error.not_yet "assumes in conjunction with ensures in behaviors";
let p = Logic_const.unamed p in
let e, env = named_predicate_to_exp env p in
Env.add_stmt env (Misc.mk_e_acsl_guard ~reverse:true e p)
| Exits | Breaks | Continues | Returns ->
- Misc.not_yet "abnormal termination case in behavior")
+ Error.not_yet "@[abnormal termination case in behavior@]")
env
b.b_post_cond
in
List.fold_left do_behavior env behaviors
let convert_pre_spec env spec =
- if spec.spec_variant <> None then Misc.not_yet "variant clause";
- if spec.spec_terminates <> None then Misc.not_yet "terminates clause";
- if spec.spec_complete_behaviors <> [] then Misc.not_yet "complete behaviors";
- if spec.spec_disjoint_behaviors <> [] then Misc.not_yet "disjoint behaviors";
- convert_preconditions env spec.spec_behavior
+ let convert env =
+ if spec.spec_variant <> None then Error.not_yet "variant clause";
+ if spec.spec_terminates <> None then Error.not_yet "terminates clause";
+ if spec.spec_complete_behaviors <> [] then
+ Error.not_yet "complete behaviors";
+ if spec.spec_disjoint_behaviors <> [] then
+ Error.not_yet "disjoint behaviors";
+ convert_preconditions env spec.spec_behavior
+ in
+ Error.handle convert env
-let convert_post_spec env spec = convert_postconditions env spec.spec_behavior
+let convert_post_spec env spec =
+ Error.handle (fun env -> convert_postconditions env spec.spec_behavior) env
let convert_named_predicate env p =
let e, env = named_predicate_to_exp env p in
@@ -735,36 +742,32 @@ let convert_named_predicate env p =
Env.add_stmt env (Misc.mk_e_acsl_guard ~reverse:true e p)
let convert_pre_code_annotation env annot =
- try
- match annot.annot_content with
+ let convert env = match annot.annot_content with
| AAssert(l, p) ->
- if l <> [] then Misc.not_yet "assertions applied only on some behaviors";
+ if l <> [] then
+ Error.not_yet "@[assertions applied only on some behaviors@]";
convert_named_predicate env p
| AStmtSpec(l, spec) ->
if l <> [] then
- Misc.not_yet "statement contract applied only on some behaviors";
+ Error.not_yet "@[statement contract applied only on some behaviors@]";
convert_pre_spec env spec ;
- | AInvariant _ -> Misc.not_yet "invariant"
- | AVariant _ -> Misc.not_yet "variant"
- | AAssigns _ -> Misc.not_yet "assigns"
- | APragma _ -> Misc.not_yet "pragma"
- with Misc.Typing_error s ->
- let msg = Format.sprintf "invalid E-ACSL construct %s." s in
- if Options.Check.get () then Misc.type_error msg
- else Options.warning ~current:true "%s@\nignoring annotation." msg;
- env
+ | AInvariant _ -> Error.not_yet "invariant"
+ | AVariant _ -> Error.not_yet "variant"
+ | AAssigns _ -> Error.not_yet "assigns"
+ | APragma _ -> Error.not_yet "pragma"
+ in
+ Error.handle convert env
let convert_post_code_annotation env annot =
- try
- match annot.annot_content with
+ let convert env = match annot.annot_content with
| AStmtSpec(_, spec) -> convert_post_spec env spec
| AAssert _
| AInvariant _
| AVariant _
| AAssigns _
| APragma _ -> env
- with Misc.Typing_error _ ->
- env
+ in
+ Error.handle convert env
(* ************************************************************************** *)
(* Visitor *)
@@ -788,7 +791,8 @@ class e_acsl_visitor prj generate = object (self)
method vglob_aux g =
if !first_global then begin
first_global := false;
- ChangeDoChildrenPost([ g ], fun l -> Misc.e_acsl_header () :: l)
+ if Options.Check.get () then DoChildren
+ else ChangeDoChildrenPost([ g ], fun l -> Misc.e_acsl_header () :: l)
end else
DoChildren
@@ -856,7 +860,7 @@ class e_acsl_visitor prj generate = object (self)
(fun (User old_a | AI(_, old_a)) (env, new_annots) ->
let a =
(* [VP] Don't use Visitor here, as it will fill the
- queue in the middle of the computation... *)
+ queue in the middle of the computation... *)
Cil.visitCilCodeAnnotation (self :> Cil.cilVisitor) old_a
in
let env = Project.on prj (convert_pre_code_annotation env) a in
@@ -906,7 +910,7 @@ class e_acsl_visitor prj generate = object (self)
in
function_env := env;
Options.debug ~level:3
- "new stmt (from sid %d): %a" stmt.sid d_stmt new_stmt;
+ "@[new stmt (from sid %d):@ %a@]" stmt.sid d_stmt new_stmt;
new_stmt
in
ChangeDoChildrenPost(stmt, mk_block)
--
GitLab