/usr/share/doc/libapron-dev/html/apron_6.html is in libapron-dev 0.9.10-5.2ubuntu3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html401/loose.dtd">
<html>
<!-- Created on November 19, 2011 by texi2html 1.82
texi2html was written by:
Lionel Cons <Lionel.Cons@cern.ch> (original author)
Karl Berry <karl@freefriends.org>
Olaf Bachmann <obachman@mathematik.uni-kl.de>
and many others.
Maintained by: Many creative people.
Send bugs and suggestions to <texi2html-bug@nongnu.org>
-->
<head>
<title>APRON 0.9.10: Functionalities of the interface at level 1</title>
<meta name="description" content="APRON 0.9.10: Functionalities of the interface at level 1">
<meta name="keywords" content="APRON 0.9.10: Functionalities of the interface at level 1">
<meta name="resource-type" content="document">
<meta name="distribution" content="global">
<meta name="Generator" content="texi2html 1.82">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css">
<!--
a.summary-letter {text-decoration: none}
blockquote.smallquotation {font-size: smaller}
pre.display {font-family: serif}
pre.format {font-family: serif}
pre.menu-comment {font-family: serif}
pre.menu-preformatted {font-family: serif}
pre.smalldisplay {font-family: serif; font-size: smaller}
pre.smallexample {font-size: smaller}
pre.smallformat {font-family: serif; font-size: smaller}
pre.smalllisp {font-size: smaller}
span.roman {font-family:serif; font-weight:normal;}
span.sansserif {font-family:sans-serif; font-weight:normal;}
ul.toc {list-style: none}
-->
</style>
</head>
<body lang="en" bgcolor="#FFFFFF" text="#000000" link="#0000FF" vlink="#800080" alink="#FF0000">
<a name="Functionalities-of-the-interface-at-level-1"></a>
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="apron_5.html#Functionalities-of-the-interface-at-level-0" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="apron_7.html#APRON-Guidelines" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="apron_3.html#APRON-Rationale-and-Functionalities" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="apron_3.html#APRON-Rationale-and-Functionalities" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="apron_7.html#APRON-Guidelines" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="apron.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[Contents]</td>
<td valign="middle" align="left">[<a href="apron_42.html#Appendices" title="Index">Index</a>]</td>
<td valign="middle" align="left">[<a href="apron_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<a name="Functionalities-of-the-interface-at-level-1-1"></a>
<h2 class="section">Functionalities of the interface at level 1</h2>
<p>We focus on the changes brought by the level 1 w.r.t. the level 0.
</p>
<table class="menu" border="0" cellspacing="0">
<tr><td align="left" valign="top"><a href="#Variables-and-Environments">• Variables and Environments</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Semantics-and-Representation-of-an-abstract-value">• Semantics and Representation of an abstract value</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Operations-on-environments">• Operations on environments</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Dynamic-typing-w_002er_002et_002e-environments">• Dynamic typing w.r.t. environments</a></td><td> </td><td align="left" valign="top">
</td></tr>
<tr><td align="left" valign="top"><a href="#Operations-on-variables-in-abstract-values">• Operations on variables in abstract values</a></td><td> </td><td align="left" valign="top">
</td></tr>
</table>
<a name="Variables-and-Environments"></a>
<a name="Variables"></a>
<h4 class="subsubheading">Variables</h4>
<p>Dimensions are replaced by <em>variables</em>.
</p>
<p>In the C interface, variables are defined by a generic type
(<code>char*</code>, structured type, ...), equipped with the operations
<code>compare</code>, <code>copy</code>, <code>free</code>, <code>to_string</code>. In the
<small>OCAML</small>, for technical reasons, the type is just the <code>string</code>
type.
</p>
<p><em>Environments</em> manages the correspondance between the numerical
dimensions of level 0 and the variables of level 1.
</p>
<a name="Semantics-and-Representation-of-an-abstract-value"></a>
<a name="Semantics-and-Representation-of-an-abstract-value-1"></a>
<h4 class="subsubheading">Semantics and Representation of an abstract value</h4>
<p>The semantics of an abstract value is a subset
</p><blockquote><p>X -> (N+R).
</p></blockquote>
<p>where <em>X</em> is a set of variables.
Abstract values are typed according to their environment.
</p>
<p>It is represented by a structure
</p><pre class="verbatim">struct ap_abstract1_t {
ap_abstract0_t *abstract0;
ap_environment_t *env;
};
</pre><p>Other datatypes of level 0 are extend in the same way. For instance,
</p><pre class="verbatim">struct ap_linexpr1_t {
ap_linexpr0_t *linexpr0;
ap_environment_t *env;
};
</pre>
<a name="Operations-on-environments"></a>
<a name="Operations-on-environments-1"></a>
<h4 class="subsubheading">Operations on environments</h4>
<ul>
<li> creation, merging, destruction
</li><li> addition/removal/renaming of variables
</li></ul>
<a name="Dynamic-typing-w_002er_002et_002e-environments"></a>
<a name="Dynamic-typing-w_002er_002et_002e-environments-1"></a>
<h4 class="subsubheading">Dynamic typing w.r.t. environments</h4>
<p>For binary operations on abstract values, the environments should be
the same.
</p>
<p>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.
</p>
<a name="Operations-on-variables-in-abstract-values"></a>
<a name="Operations-on-variables-in-abstract-values-1"></a>
<h4 class="subsubheading">Operations on variables in abstract values</h4>
<p>Operations on dimensions are lifted to operations on variables:
</p>
<ul>
<li>
Projection/Elimination of one or several variables with constant
environment;
</li><li>
Addition/Removal/Renaming of variables with corresponding change
of environment;
</li><li>
Change of environment (possibly combining removal and addition of variables);
</li><li>
Expansion and folding of variables.
</li></ul>
<hr size="6">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="apron_5.html#Functionalities-of-the-interface-at-level-0" title="Previous section in reading order"> < </a>]</td>
<td valign="middle" align="left">[<a href="apron_7.html#APRON-Guidelines" title="Next section in reading order"> > </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="apron_3.html#APRON-Rationale-and-Functionalities" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="apron_3.html#APRON-Rationale-and-Functionalities" title="Up section"> Up </a>]</td>
<td valign="middle" align="left">[<a href="apron_7.html#APRON-Guidelines" title="Next chapter"> >> </a>]</td>
</tr></table>
<p>
<font size="-1">
This document was generated by <em>Build Daemon user</em> on <em>November 19, 2011</em> using <a href="http://www.nongnu.org/texi2html/"><em>texi2html 1.82</em></a>.
</font>
<br>
</p>
</body>
</html>
|