This file is indexed.

/usr/include/ap_abstract1.h is in libapron-dev 0.9.10-7.

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
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
/* ************************************************************************* */
/* ap_abstract1.h: generic operations on abstract values at level 1 */
/* ************************************************************************* */

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

/* GENERATED FROM ap_abstract1.nw: DO NOT MODIFY ! */

#ifndef _AP_ABSTRACT1_H_
#define _AP_ABSTRACT1_H_

#include "ap_manager.h"
#include "ap_abstract0.h"
#include "ap_expr1.h"

#ifdef __cplusplus
extern "C" {
#endif

typedef struct ap_abstract1_t {
  ap_abstract0_t* abstract0;
  ap_environment_t* env;
} ap_abstract1_t;
  /* data structure invariant:
     ap_abstract0_integer_dimension(man,abstract0)== env->intdim &&
     ap_abstract0_real_dimension(man,abstract0)== env->realdim */

typedef struct ap_box1_t {
  ap_interval_t** p;
  ap_environment_t* env;
} ap_box1_t;
void ap_box1_fprint(FILE* stream, ap_box1_t* box);
void ap_box1_clear(ap_box1_t* box);

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

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

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

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

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


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

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

void ap_abstract1_canonicalize(ap_manager_t* man, ap_abstract1_t* a);
  /* Put the abstract value in canonical form. (not yet clear definition) */
  int ap_abstract1_hash(ap_manager_t* man, ap_abstract1_t* a);
  /* Return an hash value for the abstract value.  Two abstract values in
     canonical from (according to ap_abstract1_canonicalize) and
     considered as equal by the function ap_abstract0_is_eq are given the
     same hash value.
  */
  /* Return an hash code (assume canonical form) */ 
void ap_abstract1_approximate(ap_manager_t* man, ap_abstract1_t* a, int algorithm);
  /* Perform some transformation on the abstract value, guided by the
     field algorithm.

     The transformation may lose information.  The argument "algorithm"
     overrides the field algorithm of the structure of type foption_t
     associated to ap_abstract1_approximate (commodity feature). */

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

void ap_abstract1_fprint(FILE* stream,
			 ap_manager_t* man,
			 ap_abstract1_t* a);
  /* Print the abstract value in a pretty way */

void ap_abstract1_fprintdiff(FILE* stream,
			     ap_manager_t* man,
			     ap_abstract1_t* a1, ap_abstract1_t* a2);
  /* Print the difference between a1 (old value) and a2 (new value).
     The meaning of difference is library dependent. */

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


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

ap_membuf_t ap_abstract1_serialize_raw(ap_manager_t* man, ap_abstract1_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 responsibility to free the memory
   afterwards (with free). */

ap_abstract1_t ap_abstract1_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 */
/* ============================================================ */

ap_abstract1_t ap_abstract1_bottom(ap_manager_t* man, ap_environment_t* env);
  /* Create a bottom (empty) value defined on the environment */

ap_abstract1_t ap_abstract1_top(ap_manager_t* man, ap_environment_t* env);
  /* Create a top (universe) value defined on the environment */

ap_abstract1_t ap_abstract1_of_box(ap_manager_t* man,
				   ap_environment_t* env,
				   ap_var_t* tvar,
				   ap_interval_t** tinterval,
				   size_t size);
  /* Abstract an hypercube defined by the arrays tvar and tinterval,
     satisfying: forall i, tvar[i] in tinterval[i].

     If no inclusion is specified for a variable in the environment, its value
     is no constrained in the resulting abstract value.
  */


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

ap_environment_t* ap_abstract1_environment(ap_manager_t* man, ap_abstract1_t* a);
ap_abstract0_t* ap_abstract1_abstract0(ap_manager_t* man, ap_abstract1_t* a);

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

/* In abstract tests,

   - true means that the predicate is certainly true.

   - false means by default don't know (an exception has occurred, or the exact
     computation was considered too expensive to be performed).

     However, if the flag exact in the manager is true, then false means really
     that the predicate is false.
*/

bool ap_abstract1_is_bottom(ap_manager_t* man, ap_abstract1_t* a);
bool ap_abstract1_is_top(ap_manager_t* man, ap_abstract1_t* a);

bool ap_abstract1_is_leq(ap_manager_t* man, ap_abstract1_t* a1, ap_abstract1_t* a2);
  /* inclusion check */

bool ap_abstract1_is_eq(ap_manager_t* man, ap_abstract1_t* a1, ap_abstract1_t* a2);
  /* equality check */

bool ap_abstract1_sat_lincons(ap_manager_t* man, ap_abstract1_t* a, ap_lincons1_t* lincons);
bool ap_abstract1_sat_tcons(ap_manager_t* man, ap_abstract1_t* a, ap_tcons1_t* tcons);
  /* does the abstract value satisfy the constraint ? */

bool ap_abstract1_sat_interval(ap_manager_t* man, ap_abstract1_t* a,
			       ap_var_t var, ap_interval_t* interval);
  /* is the dimension included in the interval in the abstract value ?
     - Raises an exception if var is unknown in the environment of the abstract value
  */
bool ap_abstract1_is_variable_unconstrained(ap_manager_t* man, ap_abstract1_t* a,
					    ap_var_t var);
  /* is the variable unconstrained in the abstract value ?
     - Raises an exception if var is unknown in the environment of the abstract value
  */

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

ap_interval_t* ap_abstract1_bound_linexpr(ap_manager_t* man,
					  ap_abstract1_t* a, ap_linexpr1_t* expr);
ap_interval_t* ap_abstract1_bound_texpr(ap_manager_t* man,
					ap_abstract1_t* a, ap_texpr1_t* expr);
  /* Returns the interval taken by the expression
     over the abstract value. */

ap_interval_t* ap_abstract1_bound_variable(ap_manager_t* man,
					   ap_abstract1_t* a, ap_var_t var);
  /* Returns the interval taken by the variable
     over the abstract value
     - Raises an exception if var is unknown in the environment of the abstract value
  */

ap_lincons1_array_t ap_abstract1_to_lincons_array(ap_manager_t* man, ap_abstract1_t* a);
ap_tcons1_array_t ap_abstract1_to_tcons_array(ap_manager_t* man, ap_abstract1_t* a);
  /* Converts an abstract value to conjunction of constraints.  The environment
     of the result is a copy of the environment of the abstract value. */


ap_box1_t ap_abstract1_to_box(ap_manager_t* man, ap_abstract1_t* a);
  /* Converts an abstract value to an interval/hypercube. */

ap_generator1_array_t ap_abstract1_to_generator_array(ap_manager_t* man, ap_abstract1_t* a);
  /* Converts an abstract value to a system of generators.
     - The environment of the result is a copy of the environment of the abstract value.
 */

/* ********************************************************************** */
/* III. Operations: functional version */
/* ********************************************************************** */

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

ap_abstract1_t ap_abstract1_meet(ap_manager_t* man, bool destructive, ap_abstract1_t* a1, ap_abstract1_t* a2);
ap_abstract1_t ap_abstract1_join(ap_manager_t* man, bool destructive, ap_abstract1_t* a1, ap_abstract1_t* a2);
  /* Meet and Join of 2 abstract values
     - The environment of the result is the lce of the arguments
     - Raises an EXC_INVALID_ARGUMENT exception if the lce does not exists
  */

ap_abstract1_t ap_abstract1_meet_array(ap_manager_t* man, ap_abstract1_t* tab, size_t size);
ap_abstract1_t ap_abstract1_join_array(ap_manager_t* man, ap_abstract1_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
     - The environment of the result is the lce of the arguments
     - Raises an EXC_INVALID_ARGUMENT exception if the lce does not exists
  */

ap_abstract1_t ap_abstract1_meet_lincons_array(ap_manager_t* man,
					       bool destructive,
					       ap_abstract1_t* a,
					       ap_lincons1_array_t* array);
ap_abstract1_t
ap_abstract1_meet_tcons_array(ap_manager_t* man,
			      bool destructive, ap_abstract1_t* a, ap_tcons1_array_t* array);
  /* Meet of an abstract value with a set of constraints. */

ap_abstract1_t ap_abstract1_add_ray_array(ap_manager_t* man,
					  bool destructive,
					  ap_abstract1_t* a,
					  ap_generator1_array_t* array);
  /* Generalized time elapse operator */

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

/* Parallel Assignment and Substitution of several dimensions by
   expressions. */
ap_abstract1_t 
ap_abstract1_assign_linexpr_array(ap_manager_t* man,
				  bool destructive, ap_abstract1_t* a,
				  ap_var_t* tvar, ap_linexpr1_t* texpr, size_t size,
				  ap_abstract1_t* dest);
ap_abstract1_t 
ap_abstract1_substitute_linexpr_array(ap_manager_t* man,
				      bool destructive, ap_abstract1_t* a,
				      ap_var_t* tvar, ap_linexpr1_t* texpr, size_t size,
				      ap_abstract1_t* dest);
 ap_abstract1_t 
ap_abstract1_assign_texpr_array(ap_manager_t* man,
				bool destructive, ap_abstract1_t* a,
				ap_var_t* tvar, ap_texpr1_t* texpr, size_t size,
				ap_abstract1_t* dest);
ap_abstract1_t 
ap_abstract1_substitute_texpr_array(ap_manager_t* man,
				    bool destructive, ap_abstract1_t* a,
				    ap_var_t* tvar, ap_texpr1_t* texpr, size_t size,
				    ap_abstract1_t* dest);
  
/* ============================================================ */
/* III.3 Projections */
/* ============================================================ */

ap_abstract1_t ap_abstract1_forget_array(ap_manager_t* man,
					 bool destructive, ap_abstract1_t* a, 
					 ap_var_t* tvar, size_t size,
					 bool project);

/* ============================================================ */
/* III.4 Change of environment */
/* ============================================================ */

ap_abstract1_t 
ap_abstract1_change_environment(ap_manager_t* man,
				bool destructive, ap_abstract1_t* a,
				ap_environment_t* nenv,
				bool project);

ap_abstract1_t 
ap_abstract1_minimize_environment(ap_manager_t* man,
				  bool destructive, ap_abstract1_t* a);
  /* Remove from the environment of the abstract value
     variables that are unconstrained in it. */

ap_abstract1_t 
ap_abstract1_rename_array(ap_manager_t* man,
			  bool destructive, ap_abstract1_t* a,
			  ap_var_t* var, ap_var_t* nvar, size_t size);
  /* Parallel renaming. The new variables should not interfere with the variables that are not renamed. */

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

ap_abstract1_t ap_abstract1_expand(ap_manager_t* man,
				   bool destructive, ap_abstract1_t* a,
				   ap_var_t var,
				   ap_var_t* tvar, size_t size);
  /* Expand the variable var into itself + the size additional variables 
     of the array tvar, which are given the same type as var.

     It results in (size+1) unrelated variables having same
     relations with other variables.

     The additional variables are added to the environment
     of the argument for making the environment of the result.
  */

ap_abstract1_t ap_abstract1_fold(ap_manager_t* man,
				 bool destructive, ap_abstract1_t* a,
				 ap_var_t* tvar, size_t size);
  /* Fold the dimensions in the array tvar of size n>=1 and put the result
     in the first variable in the array.

     The other variables of the array are then forgot
     and removed from the environment. */


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

/* Widening */
ap_abstract1_t ap_abstract1_widening(ap_manager_t* man,
				     ap_abstract1_t* a1, ap_abstract1_t* a2);
/* Widening with threshold */
ap_abstract1_t ap_abstract1_widening_threshold(ap_manager_t* man,
					       ap_abstract1_t* a1, ap_abstract1_t* a2,
					       ap_lincons1_array_t* array);


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

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

ap_abstract1_t ap_abstract1_closure(ap_manager_t* man, bool destructive, ap_abstract1_t* a);

/* ============================================================ */
/* IV. Additional functions */
/* ============================================================ */

ap_abstract1_t ap_abstract1_of_lincons_array(ap_manager_t* man,
					     ap_environment_t* env,
					     ap_lincons1_array_t* array);
ap_abstract1_t ap_abstract1_of_tcons_array(ap_manager_t* man,
					   ap_environment_t* env,
					   ap_tcons1_array_t* array);
  /* Abstract a conjunction of constraints and return an abstract value 
     defined on the given environment. */

ap_abstract1_t ap_abstract1_assign_linexpr(ap_manager_t* man,
					   bool destructive, ap_abstract1_t* a,
					   ap_var_t var, ap_linexpr1_t* expr,
					   ap_abstract1_t* dest);
ap_abstract1_t ap_abstract1_substitute_linexpr(ap_manager_t* man,
					       bool destructive, ap_abstract1_t* a,
					       ap_var_t var, ap_linexpr1_t* expr,
					       ap_abstract1_t* dest);
ap_abstract1_t ap_abstract1_assign_texpr(ap_manager_t* man,
					 bool destructive, ap_abstract1_t* a,
					 ap_var_t var, ap_texpr1_t* expr,
					 ap_abstract1_t* dest);
ap_abstract1_t ap_abstract1_substitute_texpr(ap_manager_t* man,
					     bool destructive, ap_abstract1_t* a,
					     ap_var_t var, ap_texpr1_t* expr,
					     ap_abstract1_t* dest);
  /* Assignment and Substitution of a single
     dimension by an expression */

ap_abstract1_t ap_abstract1_unify(ap_manager_t* man,
				  bool destructive, 
				  ap_abstract1_t* a1,ap_abstract1_t* a2);
  /* Unify two abstract values on their common variables, that is, embed them
     on the least common environment and then compute their meet. The result is
     defined on the least common environment. 

     Ex: unify of {x=y, defined on {x,y}} and {y=z+t, defined on {y,z,t}}
     gives {x=y and y=z+t, defined on {x,y,z,t}}.
*/


ap_linexpr1_t ap_abstract1_quasilinear_of_intlinear(ap_manager_t* man, ap_abstract1_t* a, ap_linexpr1_t* expr, ap_scalar_discr_t discr);
  /* Evaluate the interval linear expression expr on the abstract value a and
     approximate it by a quasilinear expression. discr indicates which type of
     numbers should be used for computations.

     This implies calls to ap_abstract0_bound_dimension. */

ap_linexpr1_t ap_abstract1_intlinear_of_tree (ap_manager_t* man, ap_abstract1_t* a, ap_texpr1_t* expr, ap_scalar_discr_t discr, bool quasilinearize);
  /* Evaluate the tree expression expr on the abstract value a and approximate
     it by an interval linear (resp. quasilinear if quasilinearize is true)
     expression. discr indicates which type of numbers should be used for
     computations.
     
     This implies calls to ap_abstract0_bound_dimension. */

#ifdef __cplusplus
}
#endif

#endif