ELINA

ELINA copied to clipboard

How to tune the clam options to reproduce ELINA paper results

14

Hi, I want to reproduce the results in the paper [Fast Polyhdra Abstract Domain](http://elina.ethz.ch/papers/POPL17-Polyhedra.pdf). However clam(crab-llvm) has many options that can be tuned and I don't know how to tune...

dengyuhui14

error when executing make in ELINA

2

i get the following error when executing make in ELINA. `compute_bounds.c:5:10: fatal error: gurobi_c.h: No such file or directory #include "gurobi_c.h" ^~~~~~~~~~~~ compilation terminated. Makefile:67: recipe for target 'compute_bounds.o' failed...

metalkick

Joining operation throws overflow exception for small coefficients/dimensions

8

Hi, The code [here](https://gist.github.com/yiyunliu/587fb2c77e9e58f9b41ae285476a365f) joins two 6-dimension boxes. For each dimension, the width is no more than 100. Despite the coefficients, constants, dimensions being relatively small, ELINA throws overflow exception...

yiyunliu

zonotope_is_leq function not implemented

1

Hi Gagandeep! I noticed that zonotope_is_leq is not implemented. I wanted to know if this is something you can add quickly or plan to add? My current work around has...

shankarapailoor

Combination of substitution and dimension removal can crash polyhedra domain

1

Hi Gagandeep, I have encountered a case where the polyhedra domain crashes with an internal null pointer exception when doing the following: * Create a top value with 3 dimensions....

Cu3PO42

Hi, I am encountering issues freeing some abstract values in the polyhedra domain. I have gotten the `EXC_BAD_ACCESS` exception in ~~two~~ ~~three~~ ~~four~~ ~~five~~ six different places so far: *...

Cu3PO42

Hi Gagandeep, I have run into another issue with the polyhedra domain. Consider the following two abstract values (with two dimensions each): * `x0 - x1 >= 0 ∧ x1...

Cu3PO42

Infer results on Elina

5

Hello Gagan, I tried running our analyzer Infer on Elina and got some signals. I report this because I thought you may be interested in addressing the signals and making...

skcho

failed compilation of ocaml target

6

Make in ocaml_interface fails due to path to libraries not being correctly set. ocamlopt.opt -g -I /home/monniaux/.opam/4.04.0/lib/gmp -I /home/monniaux/.opam/4.04.0/lib/apron -o mlexample.opt bigarray.cmxa gmp.cmxa apron.cmxa elina_poly.cmxa mlexample.ml /usr/bin/ld: cannot find -lelina_poly_caml...

monniaux

Any plans for `int_64` coefficients or, ideally, `mpz_t` coefficients?

5

Hello, Unless I'm misunderstanding ELINA currently supports 32-bit integers for its coefficients but no larger (i.e. there is no `elina_coeff_set_interval_int` that works with `long long int`). It seems that ELINA...

jmct