diff -Naur apron-0.9.9-orig/apron/lgpl.texi apron-0.9.9-patch/apron/lgpl.texi --- ./apron/lgpl.texi 1970-01-01 00:00:00.000000000 +0000 +++ ./apron/lgpl.texi 2009-03-22 02:26:16.000000000 +0000 @@ -0,0 +1,556 @@ +@center Version 2.1, February 1999 + +@display +Copyright @copyright{} 1991, 1999 Free Software Foundation, Inc. +51 Franklin St -- 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.] +@end display + +@subheading 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---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 @dfn{Lesser} General Public License because it +does @emph{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. + +@subheading TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + +@enumerate 0 +@item +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. + +@item +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. + +@item +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: + +@enumerate a +@item +The modified work must itself be a software library. + +@item +You must cause the files modified to carry prominent notices +stating that you changed the files and the date of any change. + +@item +You must cause the whole of the work to be licensed at no +charge to all third parties under the terms of this License. + +@item +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.) +@end enumerate + +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. + +@item +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. + +@item +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. + +@item +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. + +@item +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: + +@enumerate a +@item +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.) + +@item +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. + +@item +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. + +@item +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. + +@item +Verify that the user has already received a copy of these +materials or that you have already sent this user a copy. +@end enumerate + + 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. + +@item +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: + +@enumerate a +@item +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. + +@item +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. +@end enumerate + +@item +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. + +@item +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. + +@item +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. + +@item +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. + +@item +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. + +@item +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. + +@item +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. + +@iftex +@heading NO WARRANTY +@end iftex +@ifinfo +@center NO WARRANTY +@end ifinfo + +@item +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. + +@item +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 enumerate + +@iftex +@heading END OF TERMS AND CONDITIONS +@end iftex +@ifinfo +@center END OF TERMS AND CONDITIONS +@end ifinfo + +@page +@subheading How to Apply These Terms to Your New Libraries + + If you develop a new library, and you want it to be of the greatest +possible use to the public, we recommend making it free software that +everyone can redistribute and change. You can do so by permitting +redistribution under these terms (or, alternatively, under the terms of the +ordinary General Public License). + + To apply these terms, attach the following notices to the library. It is +safest to attach them to the start of each source file to most effectively +convey the exclusion of warranty; and each file should have at least the +``copyright'' line and a pointer to where the full notice is found. + +@smallexample +@var{one line to give the library's name and an idea of what it does.} +Copyright (C) @var{year} @var{name of author} + +This library is free software; 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; either version 2.1 of the License, or (at +your option) any later version. + +This library 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. + +You should have received a copy of the GNU Lesser General Public +License along with this library; if not, write to the Free Software +Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, +USA. +@end smallexample + +Also add information on how to contact you by electronic and paper mail. + +You should also get your employer (if you work as a programmer) or your +school, if any, to sign a ``copyright disclaimer'' for the library, if +necessary. Here is a sample; alter the names: + +@smallexample +Yoyodyne, Inc., hereby disclaims all copyright interest in the library +`Frob' (a library for tweaking knobs) written by James Random Hacker. + +@var{signature of Ty Coon}, 1 April 1990 +Ty Coon, President of Vice +@end smallexample + +That's all there is to it! + diff -Naur apron-0.9.9-orig/apron/rationale.texi apron-0.9.9-patch/apron/rationale.texi --- ./apron/rationale.texi 1970-01-01 00:00:00.000000000 +0000 +++ ./apron/rationale.texi 2009-03-22 02:26:16.000000000 +0000 @@ -0,0 +1,647 @@ + +@menu +* General choices:: +* Functionalities of the interface at level 0:: +* Functionalities of the interface at level 1:: +@end menu + +@c =================================================================== +@node General choices, Functionalities of the interface at level 0, APRON Rationale and Functionalities, APRON Rationale and Functionalities +@section General choices +@c =================================================================== + +@menu +* Interface levels:: +* Programming language:: +* Compatibility with threads:: +* Interruptions:: +* Memory management:: +* Programming style:: +* Number representation:: +@end menu + +@c ------------------------------------------------------------------- +@node Interface levels, Programming language, General choices, General choices +@subsubheading Interface levels + +There are two main goals for the APRON interface: efficiency of the +implementations, and ease of use for the user. In addition, code +duplication between libraries should be avoided. As a consequence, two +levels were identified: +@table @emph +@item Level 0 +Choices are guided by the efficiency and the precision of the operations; +@item Level 1 +Choices are guided by ease of use, and code factorization. +@end table + +The level 0 is directly connected to the underlying (existing) +library. It includes all the operations that are specific to an +abstract domain and whose code cannot be shared. The interface should +be minimal, @emph{unless} there is a strong algorithmical advantage to +include a combination of more basic operations. + +The higher levels offers additional functionalities that are shared by +all the library connected to the level 0. For instance: + +@itemize +@item +managing correspondance between numerical dimensions and names +(characters strings or more generally references); +@item +abstraction of non linear expressions in interval linear expressions; +@item +automatic call to redimensioning and permutation operations for +computing +@iftex +@tex +$P(x,y)\sqcap Q(y,z)$ +@end tex +@end iftex +@ifnottex +P(x,y)/\Q(y,z). +@end ifnottex +@end itemize + +Combination of abstract domain is possible at the level 0. One can +implement for instance the cartesian or reduced product of two +different abstract domains, the decomposition of abstract values into +a product of values of smaller dimensionality, ... + +@c ------------------------------------------------------------------- +@node Programming language, Compatibility with threads, Interface levels, General choices +@subsubheading Programming language + +The reference version of the interface is the C version of the interface: + +@itemize +@item +C can be easily interfaced with most programming languages; +@item +Most of the existing libraries implementing abstract domains for +numerical variables are programmed in C or C++. +@end itemize + +An @sc{OCaml} version is already available. The interface between +OCaml and C is even generic and any libraries can benefit from it by +providing the glue for just one function (see XX). + +@c ------------------------------------------------------------------- +@node Compatibility with threads, Interruptions, Programming language, General choices +@subsubheading Compatibility with threads + +In order to ensure compatibility with multithreading programming, a +context is explicitly passed to functions in order to ensure the +following points: + +@itemize +@item +the transmission of data specific to each library (non-standard +options, workspace, ...); +@item +the transmission of standard options (selection of algorithms and their +precision inside a library); +@item +the management of exceptions (implemented as error codes in the C +interface) (@code{not_implemented}, @code{invalid_argument}, +@code{overflow}, @code{timeout}, @code{out_of_space}). +@end itemize + +@c ------------------------------------------------------------------- +@node Interruptions, Memory management, Compatibility with threads, General choices +@subsubheading Interruptions + +Interruptions mechanism is have possible for different cases: +@table @code +@item timeout +if the execution time for an operation exceeds some bound; +@item out_of_space +if the space consumption for an operation exceeds some bound; +@item overflow +if the magnitude or the space usage of manipulated numbers exceeds some bound; +@item not_implemented +if the operation is actually not implemented by the underlying library; +@item invalid_argument +if the arguments do not follow the requirements of an operation. +@end table + +@quotation +For instance, in a convex polyhedra library, the @code{out_of_space} +exception allows to abort an operation is the result appears to have +too many constraints and/or generators. If this happens, one can redo +the operation with another (less precise) algorithm. The +@code{overflow} may be useful when effective overflows are encountered +with machine integers or when multiprecision rational numbers have too +large numerators and denominators. The @code{not_implemented} +exception allows for a library to be linked to the interface even if +it does not provide some operation of the interface. +@end quotation + +When an interruption occurs, the function should still return a +correct result, in the abstract interpretation sense: it should be a +correct approximation, usable for next operations in the program. The +top value is always a correct approximation. + +@c ------------------------------------------------------------------- +@node Memory management, Programming style, Interruptions, General choices +@subsubheading Memory management + +Memory is managed differently depending on the programming language. Currently: + +@itemize +@item +No automatic garbage collection in the C interface +@item +Use of the @sc{OCaml} runtime garbage collector in the @sc{OCaml} interface +@end itemize + +@c ------------------------------------------------------------------- +@node Programming style, Number representation, Memory management, General choices +@subsubheading Programming style + +Both functional and imperative (i.e., side-effect) signatures are +supported for operations. This allows to optimize the memory +allocation and to use whichever version is more convenient for an user +and the used programming language. + +@c ------------------------------------------------------------------- +@node Number representation, , Programming style, General choices +@subsubheading Number representation + +Inside a specific library, any number representation may be used +(floating-point numbers, machine integers, multiprecision +integers/rationals, ...). Existing libraries often offers the +possibility to select different representations. + +However, in the interface, this representation should be normalized +and independent of underlying libraries, without being restrictive +either. As a consequence, the interface offers the choiced between + +@itemize +@item GMP multiprecision rationals (which implements exact arithmetic); +@item and machine floating-point numbers (@code{double}). +@end itemize + +@c =================================================================== +@node Functionalities of the interface at level 0, Functionalities of the interface at level 1, General choices, APRON Rationale and Functionalities +@section Functionalities of the interface at level 0 +@c =================================================================== + +@menu +* Representation of an abstract value:: +* Semantics of an abstract value:: +* Dimensions:: +* Other datatypes:: +* Control of internal representation:: +* Printing:: +* Serializaton/Deserialization:: +* Constructors:: +* Tests:: +* Property extraction:: +* Lattice operations:: +* Assignement and Substitutions:: +* Operations on dimensions:: +* Other operations:: +@end menu + + +@c ------------------------------------------------------------------- +@node Representation of an abstract value, Semantics of an abstract value, Functionalities of the interface at level 0, Functionalities of the interface at level 0 +@subsubheading Representation of an abstract value + +At the level 0 of the interface, an abstract value is a structure +@verbatim +struct ap_abstract0_t { + ap_manager_t *manager; /* Explicit context */ + void *value; /* Abstract value representation + (only known by the underlying library) */ +} +@end verbatim +The context is allocated by the underlying library, and contains an +array of function pointers pointing to the function of the underlying +library. Hence, it indicates the effective type of an abstract value. + +The validity of the arguments of the functions called through the +interface is checked before the call to effective functions. In case +of problem, an @code{invalid_argument} exception is raised. + +@c ------------------------------------------------------------------- +@node Semantics of an abstract value, Dimensions, Representation of an abstract value, Functionalities of the interface at level 0 +@subsubheading Semantics of an abstract value + +The semantics of an abstract value is a subset +@iftex +@tex +$$X\subseteq {\cal N}^p\times{\cal R}^q$$ +@end tex +@end iftex +@ifnottex +@quotation +X of N^p x R^q +@end quotation +@end ifnottex + +@noindent Abstract values are typed according to their dimensionality +(p,q). + +@c ------------------------------------------------------------------- +@node Dimensions, Other datatypes, Semantics of an abstract value, Functionalities of the interface at level 0 +@subsubheading Dimensions +Dimensions are numbered from 0 to p+q-1 and are typed either as +integer or real, depending on their rank w.r.t. the dimensionality of +the abstract value. + +@quotation Note +Taking into account or not the fact that some dimensions are integers +is left to underlying libraries. Treating them as real is still a +correct approximation. The behaviour of the libraries in this regard +may also depend on some options. +@end quotation + +@c ------------------------------------------------------------------- +@node Other datatypes, Control of internal representation, Dimensions, Functionalities of the interface at level 0 +@subsubheading Other datatypes + +In addition to abstract values, the interface also manipulates the +following main datatypes: +@table @emph +@item scalar (number) +Either GMP multiprecision rationals or C @code{double}. +@item interval +composed of 2 scalar numbers. With rationals, plus (resp minus) infinity is represented by 1/0 (resp -1/0). With @code{double}, the IEEE754 is assumed and the corresponding standard representation is used. +@item coefficient +which is either a scalar or an interval. +@item (interval) linear expression +The term linear is used even if the proper term should rather be +affine. A linear expression is a linear expression in the common +sense, using only scalar numbers. A quasi-linear expression is a +linear expression where the constant coefficient is an interval. An +interval linear expression is a linear expression where any +coefficient may be an interval. In order to have a unique datatype for +these variations, we introduced the notion of coefficient described +above. +@item ``linear'' constraints +``Linear'' constraints includes proper linear constraints, linear +constraints in which the expression can be possibly an interval linear +expression, linear equalities modulo a number, and linear disequalities. +@item generators +A generator system for a subset of @math{X\subseteq R^n} is a finite +set of vectors, among which one distinguishes @emph{points} +@math{p_0,\ldots,p_m} and @emph{rays} @math{r_0,\ldots,r_n}, that +generates @math{X}: +@iftex +@tex +$$X=\{ \lambda_0 \vec{p_0} + \ldots \lambda_m \vec{p_m} + \mu_0 \vec{r_0} +\ldots + \mu_n \vec{r_n} ~|~ \sum_i \lambda_i = 1 ~\wedge~ \forall j: \mu_j\geq 0 \}$$ +@end tex +@end iftex +@ifnottex +@quotation +X = @{ lambda0 p0 +...+ lambdaM pM + mu0 r0 +...+ muN rN | lambda0 +...+ lambdaN = 1 and forall J : muJ >= 0 @} +@end quotation +@end ifnottex +The APRON datatype for generators distinguishes points (sum of +coefficients equal to one), rays (positive coefficients), lines (or +bidirectional rays, with unconstrainted coefficients), integer rays +(integer positive coefficients) and integer lines (integer +coefficients). +@end table + +@c ------------------------------------------------------------------- +@node Control of internal representation, Printing, Other datatypes, Functionalities of the interface at level 0 +@subsubheading Control of internal representation + +We identified several notions: + +@itemize +@item +Canonical form +@item +Minimal form (in term of space) +@item +Approximation notion left to the underlying library (taking into +account integers or not, ...). +@end itemize + +@c ------------------------------------------------------------------- +@node Printing, Serializaton/Deserialization, Control of internal representation, Functionalities of the interface at level 0 +@subsubheading Printing + +There are two printing operations: + +@itemize +@item +Printing of an abstract value; +@item +Printing the difference between two abstract values. +@end itemize + +@noindent The printing format is library dependent. However, the conversion of +abstract values to constraints (see below) allows a form of +standardized printing for abstract values. + +@c ------------------------------------------------------------------- +@node Serializaton/Deserialization, Constructors, Printing, Functionalities of the interface at level 0 +@subsubheading Serializaton/Deserialization + +Serialization and deserialization of abstract values to a memory +buffer is offered. It is entirely managed by the underlying +library. In particular, it is up to it to check that a value read from +the memory buffer has the right format and has not been written by a +different library. + +Serialization is done to a memory buffer instead of to a file +descriptor because this mechanism is more general and is needed for +interfacing with languages like @sc{OCaml}. + +@c ------------------------------------------------------------------- +@node Constructors, Tests, Serializaton/Deserialization, Functionalities of the interface at level 0 +@subsubheading Constructors + +Four basic constructors are offered: + +@itemize +@item +bottom (empty) and top (universe) values (with a specified dimensionality); +@item +abstraction of a bounding box; +@item +abstraction of conjunction of linear constraints (in the broad sense). +@end itemize + +@c ------------------------------------------------------------------- +@node Tests, Property extraction, Constructors, Functionalities of the interface at level 0 +@subsubheading Tests + +Predicates are offered for testing +@itemize +@item +emptiness and universality of an abstract value: +@item +inclusion and equality of two abstract values; +@item +inclusion of a dimension into an interval given an abstract value; +@iftex +@tex +$${\it abs}(\vec{x}) \models x_i \in I ~~ ?$$ +@end tex +@end iftex +@item +satisfaction of a linear constraint by the abstract value. +@iftex +@tex +$${\it abs}(\vec{x}) \models {\it cons}(\vec{x}) ~~ {\tt or} ~~ {\it abs}(\vec{x}) \Rightarrow {\it cons}(\vec{x}) ~~ ?$$ +@end tex +@end iftex +@end itemize + +@c ------------------------------------------------------------------- +@node Property extraction, Lattice operations, Tests, Functionalities of the interface at level 0 +@subsubheading Property extraction + +Some properties may be inferred given an abstract values: + +@itemize +@item Interval of variation of a dimension in an abstract value; +@iftex +@tex +$$\bigcap\{ I ~|~ {\it abs}(\vec{x}) \models x_i\in I\}$$ +@end tex +@end iftex + +@item Interval of variation of a linear expression in an abstract value; +@iftex +@tex +$$\bigcap\{ I ~|~ {\it abs}(\vec{x}) \models {\it expr}(\vec{x})\in I\}$$ +@end tex +@end iftex +@item Conversion to a bounding box +@iftex +@tex +$$\bigcap\{ B ~|~ {\it abs}(\vec{x}) \subseteq B \}$$ +@end tex +@end iftex +@item Conversion to a set of linear constraints (in the broad sense). +@end itemize + +@noindent Notice that the second operation implements linear programming if it +is exact. The third operation is not minimal, as it can be implemented +using the first one, but it was convenient to include it. But the +fourth operation is minimal and cannot be implemented using the second +one, as the number of linear expression is infinite. + +@c ------------------------------------------------------------------- +@node Lattice operations, Assignement and Substitutions, Property extraction, Functionalities of the interface at level 0 +@subsubheading Lattice operations + +@itemize +@item +Least upper bound and greatest lower bound of two abstract values, and of arrays of abstract values; +@item +Intersection with one or several linear constraints; +@iftex +@tex +$$\alpha\left(\gamma({\it abs}(\vec{x})) \cap \bigcap_i {\it cons}_i(\vec{x})\right)$$ +@end tex +@end iftex +@item +Addition of rays (for instance for implement generalized time elapse +operator in linear hybrid systems). +@iftex +@tex +$$\alpha\left(\left\{ \vec{x} + \sum_i \lambda_i \vec{r}_i ~|~ \vec{x}\in\gamma({\it abs}), \lambda_i\geq 0\right\}\right)$$ +@end tex +@end iftex +@end itemize + +@c ------------------------------------------------------------------- +@node Assignement and Substitutions, Operations on dimensions, Lattice operations, Functionalities of the interface at level 0 +@subsubheading Assignement and Substitutions + +@itemize +@item +of a dimension by a (interval) linear expression +@iftex +@tex + +Assignement: +$$\alpha\left(\biggl( +\exists x_i: \Bigl(\gamma({\it abs}(\vec{x})) \cap x_i'={\it expr}(\vec{x})\Bigr)\biggr)[x_i\leftarrow x_i']\right)$$ +Substitution: +$$\alpha\biggl( +\exists x_i': \Bigl(\gamma({\it abs}(\vec{x}))[x_i'\leftarrow x_i] \cap x_i'={\it expr}(\vec{x})\Bigr)\biggr)$$ + +@end tex +@end iftex +@item +in parallel of several dimensions by several (interval) linear expressions +@iftex +@tex + +Assignement: +$$\alpha\left(\biggl( +\exists \vec{x}: \Bigl(\gamma({\it abs}(\vec{x})) \cap \bigcap_i x_i'={\it expr}_i(\vec{x})\Bigr)\biggr)[\vec{x}\leftarrow \vec{x'}]\right)$$ +Substitution: +$$\alpha\biggl( +\exists \vec{x'}: \Bigl(\gamma({\it abs}(\vec{x'})) \cap \bigcap_i x_i'={\it expr}(\vec{x})\Bigr)\biggr)$$ + +@end tex +@end iftex +@end itemize + +@noindent Parallel assignement and substitution ar enot minimal operations, but +for some abstract domains implementing them directly results in more +efficient or more precise operations. + +@c ------------------------------------------------------------------- +@node Operations on dimensions, Other operations, Assignement and Substitutions, Functionalities of the interface at level 0 +@subsubheading Operations on dimensions + +@itemize +@item +Projection/Elimination of one or several dimensions with constant +dimensionality; +@iftex +@tex + +Elimination: $$\exists x_i:{\it abs}(\vec{x})$$ + +Projection: $$(\exists x_i:{\it abs}(\vec{x}))\cap x_i=0$$ +@end tex +@end iftex +@item +Addition/Removal/Permutation of dimensions with corresponding change +of dimensionality (with the exception of permutation). These +operations allows to resize abstract values, and reorganize +dimensions. +@item +Expansion and folding of dimensions. This is useful for the +abstraction of arrays, where a dimension may represent several +variables. +@iftex +@tex + +Expansion of $i$ into $i$, $j_1$, $j_2$ assuming $x_{j_1}$, $x_{j_2}$ are new dimensions: +$${\it abs}(\vec{x}) \sqcap {\it abs}(\vec{x})[x_{j_1}\leftarrow x_i] \sqcap {\it abs}(\vec{x})[x_{j_2}\leftarrow x_i] ... +$$ +Folding of $j_0$ and $j_1$ into $j_0$: +$$(\exists x_{j_1}:{\it abs}(\vec{x})) \sqcup (\exists x_{j_0}:{\it abs}(\vec{x})[x_{j_0}\leftarrow x_{j_1}] +$$ +@end tex +@end iftex + + +@end itemize + +@c ------------------------------------------------------------------- +@node Other operations, , Operations on dimensions, Functionalities of the interface at level 0 +@subsubheading Other operations + +Widening, either simple or with threshold, is offered. A generic +widening with threshold function is offered in the interface. + +Topological closure (i.e., relaxation of strict inequalities) is +offered. + +@c =================================================================== +@node Functionalities of the interface at level 1, , Functionalities of the interface at level 0, APRON Rationale and Functionalities +@section Functionalities of the interface at level 1 +@c =================================================================== + +We focus on the changes brought by the level 1 w.r.t. the level 0. + +@menu +* Variables and Environments:: +* Semantics and Representation of an abstract value:: +* Operations on environments:: +* Dynamic typing w.r.t. environments:: +* Operations on variables in abstract values:: +@end menu + +@c ------------------------------------------------------------------- +@node Variables and Environments, Semantics and Representation of an abstract value, Functionalities of the interface at level 1, Functionalities of the interface at level 1 +@subsubheading Variables + +Dimensions are replaced by @emph{variables}. + +In the C interface, variables are defined by a generic type +(@code{char*}, structured type, ...), equipped with the operations +@code{compare}, @code{copy}, @code{free}, @code{to_string}. In the +@sc{OCaml}, for technical reasons, the type is just the @code{string} +type. + +@emph{Environments} manages the correspondance between the numerical +dimensions of level 0 and the variables of level 1. + +@c ------------------------------------------------------------------- +@node Semantics and Representation of an abstract value, Operations on environments, Variables and Environments, Functionalities of the interface at level 1 +@subsubheading Semantics and Representation of an abstract value + +The semantics of an abstract value is a subset +@iftex +@tex +$$X\subseteq V\rightarrow ({\cal N}\cup{\cal R})$$ +@end tex +@end iftex +@ifnottex +@quotation +X -> (N+R). +@end quotation +@end ifnottex +where @math{X} is a set of variables. +@noindent +Abstract values are typed according to their environment. + +It is represented by a structure +@verbatim +struct ap_abstract1_t { + ap_abstract0_t *abstract0; + ap_environment_t *env; +}; +@end verbatim +Other datatypes of level 0 are extend in the same way. For instance, +@verbatim +struct ap_linexpr1_t { + ap_linexpr0_t *linexpr0; + ap_environment_t *env; +}; +@end verbatim + +@c ------------------------------------------------------------------- +@node Operations on environments, Dynamic typing w.r.t. environments, Semantics and Representation of an abstract value, Functionalities of the interface at level 1 +@subsubheading Operations on environments + +@itemize +@item creation, merging, destruction +@item addition/removal/renaming of variables +@end itemize + +@c ------------------------------------------------------------------- +@node Dynamic typing w.r.t. environments, Operations on variables in abstract values, Operations on environments, Functionalities of the interface at level 1 +@subsubheading Dynamic typing w.r.t. environments + +For binary operations on abstract values, the environments should be +the same. + +For operations involving an abstract value and an other datatype +(expression, constraint, ...), one checks that the environment of +the expression is a subenvironment of the environment of the abstract +value, and one resize if necessary. + +@c ------------------------------------------------------------------- +@node Operations on variables in abstract values, , Dynamic typing w.r.t. environments, Functionalities of the interface at level 1 +@subsubheading Operations on variables in abstract values + +Operations on dimensions are lifted to operations on variables: + +@itemize +@item +Projection/Elimination of one or several variables with constant +environment; +@item +Addition/Removal/Renaming of variables with corresponding change +of environment; +@item +Change of environment (possibly combining removal and addition of variables); +@item +Expansion and folding of variables. +@end itemize diff -Naur apron-0.9.9-orig/mlapronidl/index.html apron-0.9.9-patch/mlapronidl/index.html --- ./mlapronidl/index.html 1970-01-01 00:00:00.000000000 +0000 +++ ./mlapronidl/index.html 2009-03-22 02:26:16.000000000 +0000 @@ -0,0 +1,215 @@ + + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +Manager |
+APRON Managers
+
+ |
Box |
+BOX: intervals abstract domain
+
+ |
Oct |
+OCT: octagon abstract domain.
+
+ |
Polka |
+POLKA: Convex Polyhedra and Linear Equalities abstract domain
+
+ |
PPL |
+PPL: Convex Polyhedra and Linear Congruences abstract domain
+
+ |
PolkaGrid |
+PolkaGrid: reduced product of (NewPolka) Convex Polyhedra and (PPL) Linear Congruences abstract domain
+
+ |
Scalar |
+APRON Scalar numbers.
+
+ |
Interval |
+APRON Intervals on scalars
+
+ |
Coeff |
+APRON Coefficients (either scalars or intervals)
+
+ |
Var |
+APRON Variables
+
+ |
Environment |
+APRON Environments binding dimensions to names
+
+ |
Linexpr1 |
+APRON Linear Expressions of level 1
+
+ |
Lincons1 |
+APRON Linear Constraints and array of constraints of level 1
+
+ |
Generator1 |
+APRON Generators and array of generators of level 1
+
+ |
Texpr1 |
+APRON Non-Linear Expressions of level 1
+
+ |
Tcons1 |
+APRON Non-Linear Constraints and array of constraints of level 1
+
+ |
Abstract1 |
+APRON Abstract values of level 1
+
+ |
Parser |
+APRON Parser for expressions, constraints and generators
+
+ |
Dim |
+APRON Dimensions and related types
+
+ |
Linexpr0 |
+APRON Linear expressions of level 0
+
+ |
Lincons0 |
+APRON Linear constraints of level 0
+
+ |
Generator0 |
+APRON Generators of level 0
+
+ |
Texpr0 |
+APRON Non-Linear Expressions of level 0
+
+ |
Tcons0 |
+APRON Non-Linear Constraints and array of constraints of level 0
+
+ |
Abstract0 |
+APRON Abstract value of level 0
+
+ |
Mpz |
+GMP multi-precision integers
+
+ |
Mpq |
+GMP multiprecision rationals
+
+ |
Mpf |
+GMP multiprecision floating-point numbers
+
+ |
Mpfr |
+MPFR Multiprecision floating-point numbers with guaranteed rounding
+
+ |
Gmp_random |
+GMP random generation functions
+
+ |
Mpzf |
+GMP multi-precision integers, functional version
+
+ |
Mpqf |
+GMP multi-precision rationals, functional version
+
+ |
Mpfrf |
+MPFR multi-precision floating-point numbers, functional version
+
+ |