This file is indexed.

/usr/include/pkeq.h 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
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
/* ********************************************************************** */
/* pkeq.h: Interface of the polka linear equalities library  */
/* ********************************************************************** */

/* This file is part of the APRON Library, released under LGPL license.  Please
   read the COPYING file packaged in the distribution */

#ifndef __PKEQ_H__
#define __PKEQ_H__


#ifdef __cplusplus
extern "C" {
#endif

#include "ap_global0.h"
#include "pk.h"

typedef pk_t pkeq_t;

/* 

  Important remark: the newpolka library is normally intended to be accessed
  through the APRON interface, i.e., through abstract0_XX and abstract1_XX
  functions. If it is accessed directly with poly_XXX functions, many checks on
  arguments will not be performed.

*/


/* ============================================================ */
/* A. Constructor for APRON manager (to be freed with ap_manager_free). */
/* ============================================================ */

ap_manager_t* pkeq_manager_alloc(void);
pk_internal_t* pkeq_manager_get_internal(ap_manager_t*);

/* ============================================================ */
/* D. Conversions */
/* ============================================================ */

pkeq_t* pkeq_of_abstract0(ap_abstract0_t* abstract);
  /* Extract from an abstract value the underlying NewPolka polyhedron.  There
     is no copy, so only one of the two objects should be freed. */

ap_abstract0_t* pkeq_to_abstract0(ap_manager_t* man, pkeq_t* poly);
  /* Create an abstract value from the manager and the underlying NewPolka
     polyhedron. There is no copy, and only the result should be freed
  */

/* ********************************************************************** */
/* I. General management */
/* ********************************************************************** */


/* ============================================================ */
/* I.1 Memory */
/* ============================================================ */

pkeq_t* pkeq_copy(ap_manager_t* man, pkeq_t* a);
  /* Return a copy of an abstract value, on
     which destructive update does not affect the initial value. */

void pkeq_free(ap_manager_t* man, pkeq_t* a);
  /* Free all the memory used by the abstract value */

size_t pkeq_size(ap_manager_t* man, pkeq_t* a);
  /* Return the abstract size of an abstract value (see ap_manager_t) */


/* ============================================================ */
/* I.2 Control of internal representation */
/* ============================================================ */

void pkeq_minimize(ap_manager_t* man, pkeq_t* a);
  /* Minimize the size of the representation of a.
     This may result in a later recomputation of internal information.
  */

void pkeq_canonicalize(ap_manager_t* man, pkeq_t* a);
  /* Put the abstract value in canonical form. (not yet clear definition) */

void pkeq_hash(ap_manager_t* man, pkeq_t* a);
  /* Return an hash code */

void pkeq_approximate(ap_manager_t* man, pkeq_t* a, int algorithm);
  /* Perform some transformation on the abstract value, guided by the
     field algorithm.

     The transformation may lose information. */

/* ============================================================ */
/* I.3 Printing */
/* ============================================================ */

void pkeq_fprint(FILE* stream,
		 ap_manager_t* man,
		 pkeq_t* a,
		 char** name_of_dim);
  /* Print the abstract value in a pretty way, using function
     name_of_dim to name dimensions */

void pkeq_fprintdiff(FILE* stream,
		     ap_manager_t* man,
		     pkeq_t* a1, pkeq_t* a2,
		     char** name_of_dim);
  /* Print the difference between a1 (old value) and a2 (new value),
     using function name_of_dim to name dimensions.
     The meaning of difference is library dependent. */

void pkeq_fdump(FILE* stream, ap_manager_t* man, pkeq_t* a);
  /* Dump the internal representation of an abstract value,
     for debugging purposes */


/* ============================================================ */
/* I.4 Serialization */
/* ============================================================ */

ap_membuf_t pkeq_serialize_raw(ap_manager_t* man, pkeq_t* a);
/* Allocate a memory buffer (with malloc), output the abstract value in raw
   binary format to it and return a pointer on the memory buffer and the size
   of bytes written.  It is the user responsability to free the memory
   afterwards (with free). */

pkeq_t* pkeq_deserialize_raw(ap_manager_t* man, void* ptr, size_t* size);
/* Return the abstract value read in raw binary format from the input stream
   and store in size the number of bytes read */

/* ********************************************************************** */
/* II. Constructor, accessors, tests and property extraction */
/* ********************************************************************** */

/* ============================================================ */
/* II.1 Basic constructors */
/* ============================================================ */

/* We assume that dimensions [0..intdim-1] correspond to integer variables, and
   dimensions [intdim..intdim+realdim-1] to real variables */

pkeq_t* pkeq_bottom(ap_manager_t* man, size_t intdim, size_t realdim);
  /* Create a bottom (empty) value */

pkeq_t* pkeq_top(ap_manager_t* man, size_t intdim, size_t realdim);
  /* Create a top (universe) value */


pkeq_t* pkeq_of_box(ap_manager_t* man,
		    size_t intdim, size_t realdim,
		    ap_interval_t** tinterval);
  /* Abstract an hypercube defined by the array of intervals
     of size intdim+realdim */

pkeq_t* pkeq_of_lincons_array(ap_manager_t* man,
			      size_t intdim, size_t realdim,
			      ap_lincons0_array_t* array);
  /* Abstract a convex polyhedra defined by the array of linear constraints
     of size size */


/* ============================================================ */
/* II.2 Accessors */
/* ============================================================ */

ap_dimension_t pkeq_dimension(ap_manager_t* man, pkeq_t* a);
/* Return the total number of dimensions of the abstract values */

/* ============================================================ */
/* II.3 Tests */
/* ============================================================ */

bool pkeq_is_bottom(ap_manager_t* man, pkeq_t* a);
bool pkeq_is_top(ap_manager_t* man, pkeq_t* a);

bool pkeq_is_leq(ap_manager_t* man, pkeq_t* a1, pkeq_t* a2);
  /* inclusion check */

bool pkeq_is_eq(ap_manager_t* man, pkeq_t* a1, pkeq_t* a2);
  /* equality check */

bool pkeq_sat_lincons(ap_manager_t* man, pkeq_t* a, ap_lincons0_t* lincons);
  /* does the abstract value satisfy the linear constraint ? */

bool pkeq_sat_interval(ap_manager_t* man, pkeq_t* a,
		       ap_dim_t dim, ap_interval_t* interval);
  /* is the dimension included in the interval in the abstract value ? */

bool pkeq_is_dimension_unconstrained(ap_manager_t* man, pkeq_t* po,
				     ap_dim_t dim);
  /* is the dimension unconstrained ? */

/* ============================================================ */
/* II.4 Extraction of properties */
/* ============================================================ */

ap_interval_t* pkeq_bound_linexpr(ap_manager_t* man,
				      pkeq_t* a, ap_linexpr0_t* expr);
  /* Returns the interval taken by a linear expression
     over the abstract value */

ap_interval_t* pkeq_bound_dimension(ap_manager_t* man,
				    pkeq_t* a, ap_dim_t dim);
  /* Returns the interval taken by the dimension
     over the abstract value */

ap_lincons0_array_t pkeq_to_lincons_array(ap_manager_t* man, pkeq_t* a);
  /* Converts an abstract value to a polyhedra
     (conjunction of linear constraints). */

ap_interval_t** pkeq_to_box(ap_manager_t* man, pkeq_t* a);
  /* Converts an abstract value to an interval/hypercube.
     The size of the resulting array is pkeq_dimension(man,a).  This
     function can be reimplemented by using pkeq_bound_linexpr */

ap_generator0_array_t pkeq_to_generator_array(ap_manager_t* man, pkeq_t* a);
  /* Converts an abstract value to a system of generators. */


/* ********************************************************************** */
/* III. Operations */
/* ********************************************************************** */

/* ============================================================ */
/* III.1 Meet and Join */
/* ============================================================ */

pkeq_t* pkeq_meet(ap_manager_t* man, bool destructive, pkeq_t* a1, pkeq_t* a2);
pkeq_t* pkeq_join(ap_manager_t* man, bool destructive, pkeq_t* a1, pkeq_t* a2);
  /* Meet and Join of 2 abstract values */

pkeq_t* pkeq_meet_array(ap_manager_t* man, pkeq_t** tab, size_t size);
pkeq_t* pkeq_join_array(ap_manager_t* man, pkeq_t** tab, size_t size);
  /* Meet and Join of an array of abstract values.
     Raises an [[exc_invalid_argument]] exception if [[size==0]]
     (no way to define the dimensionality of the result in such a case */

pkeq_t* pkeq_meet_lincons_array(ap_manager_t* man,
				bool destructive, pkeq_t* a,
				ap_lincons0_array_t* array);
  /* Meet of an abstract value with a set of constraints
     (generalize pkeq_of_lincons_array) */

pkeq_t* pkeq_add_ray_array(ap_manager_t* man,
			   bool destructive, pkeq_t* a,
			   ap_generator0_array_t* array);
  /* Generalized time elapse operator */

/* ============================================================ */
/* III.2 Assignement and Substitutions */
/* ============================================================ */

pkeq_t* pkeq_assign_linexpr(ap_manager_t* man,
			    bool destructive, pkeq_t* a,
			    ap_dim_t dim, ap_linexpr0_t* expr,
			    pkeq_t* dest);
pkeq_t* pkeq_substitute_linexpr(ap_manager_t* man,
				bool destructive, pkeq_t* a,
				ap_dim_t dim, ap_linexpr0_t* expr,
				pkeq_t* dest);
  /* Assignement and Substitution of a single dimension by resp.
     a linear expression and a interval linear expression */

pkeq_t* pkeq_assign_linexpr_array(ap_manager_t* man,
				  bool destructive, pkeq_t* a,
				  ap_dim_t* tdim,
				  ap_linexpr0_t** texpr,
				  size_t size,
				  pkeq_t* dest);
pkeq_t* pkeq_substitute_linexpr_array(ap_manager_t* man,
				      bool destructive, pkeq_t* a,
				      ap_dim_t* tdim,
				      ap_linexpr0_t** texpr,
				      size_t size,
				      pkeq_t* dest);
  /* Parallel Assignement and Substitution of several dimensions by
     linear expressons. */

/* ============================================================ */
/* III.3 Projections */
/* ============================================================ */

pkeq_t* pkeq_forget_array(ap_manager_t* man,
			  bool destructive, pkeq_t* a,
			  ap_dim_t* tdim, size_t size,
			  bool project);

/* ============================================================ */
/* III.4 Change and permutation of dimensions */
/* ============================================================ */

pkeq_t* pkeq_add_dimensions(ap_manager_t* man,
			    bool destructive, pkeq_t* a,
			    ap_dimchange_t* dimchange,
			    bool project);

pkeq_t* pkeq_remove_dimensions(ap_manager_t* man,
			       bool destructive, pkeq_t* a,
			       ap_dimchange_t* dimchange);
pkeq_t* pkeq_permute_dimensions(ap_manager_t* man,
				bool destructive,
				pkeq_t* a,
				ap_dimperm_t* permutation);

/* ============================================================ */
/* III.5 Expansion and folding of dimensions */
/* ============================================================ */

pkeq_t* pkeq_expand(ap_manager_t* man,
		    bool destructive, pkeq_t* a,
		    ap_dim_t dim,
		    size_t n);
  /* Expand the dimension dim into itself + n additional dimensions.
     It results in (n+1) unrelated dimensions having same
     relations with other dimensions. The (n+1) dimensions are put as follows:

     - original dimension dim

     - if the dimension is integer, the n additional dimensions are put at the
       end of integer dimensions; if it is real, at the end of the real
       dimensions.
  */

pkeq_t* pkeq_fold(ap_manager_t* man,
		  bool destructive, pkeq_t* a,
		  ap_dim_t* tdim,
		  size_t size);
  /* Fold the dimensions in the array tdim of size n>=1 and put the result
     in the first dimension in the array. The other dimensions of the array
     are then removed (using pkeq_permute_remove_dimensions). */

/* ============================================================ */
/* III.6 Widening */
/* ============================================================ */

/* Widening */
pkeq_t* pkeq_widening(ap_manager_t* man,
		      pkeq_t* a1, pkeq_t* a2);

/* ============================================================ */
/* III.7 Closure operation */
/* ============================================================ */

/* Returns the topological closure of a possibly opened abstract value */

pkeq_t* pkeq_closure(ap_manager_t* man, bool destructive, pkeq_t* a);

#ifdef __cplusplus
}
#endif

#endif