mpelleau / absolute Goto Github PK

AbSolute does not seem to have a test library/framework yet, and I would need one to make simple tests on the octagon abstract domain I'm developing.
Since I won't (shouldn't ? ;-)) be the only one to use it, I prefer to ask what is your preference.
After a quick look on the ones available in OPAM, my preference goes to ppx_inline_test for the following reasons:

• Very easy to write tests (maybe the most important reason, otherwise we don't write them...).
• Use OCaml syntax.
• Tests can be written inside the source file, which has various advantages such as:
  • Serving as valuable documentation.
  • Easy access to private information of modules (for example to check invariants of internal data structures).
• Developed and used by Jane Street. It is one of the most downloaded test framework and seem to be regularly updated.

What do you think?

Hello,

I cannot install AbSolute via opam. As I can build AbSolute from the sources, I have compared both sources from master branch and the opam package sources :

• the dune file in the opam package contains the line

(c_names src/ml_float)

instead of

(c_names ml_float)

which leads to a dune error

• changing the line removes the dune error, but Pervasives is still used in the source files which leads to deprecation error.

My environment :

• OCaml 4.09
• dune 2.1.3
• apron 0.9.12

Best,

Christophe

Segfault with rational boxes on an octagon problem (octagon.abs added in pull request #12).
Replicate with:

absolute -domain boxQ problems/octagon.abs
absolute -domain boxQS problems/octagon.abs

Problem: AbSolute is compiled with a Makefile, and script to support compilation with and without the VPL library.
Also if we want to ppx_inline_test as a test framework (issue #6), the compilation script will get heavier.

Proposed solution: I suggest to use Dune which is a modern OCaml build system. The advantages include:

• It has a very complete documentation.
• It provides in its documentation an explanation on how to set ppx_inline_test and Menhir.
• A lot of cool features to generate documentation, dealing with workspaces, ...
• Conditional compilation supported with something like that:

(library
 ((name absolute)
  (libraries (vpl (select vpl_domain.ml from
                   (vpl  -> vpl_domain.ok.ml)
                   (!vpl -> vpl_domain.ko.ml))))))

self explanatory

Travis CI is a tool for continuous integration of projects, which is very useful to know when the project is does not compile anymore (which frequently happens :-)).
I set the .travis.yml file on my fork, and it works well.

If you are interested, and in order to make it work on this repository, here the steps (it should take 5 minutes):

• @mpelleau should activate travis CI on this repository.
• Copy the .travis.yml in this repository.
• Remove the three first lines (about secure stuff), or set the encryption key on your account.

And it should work.

Hello,
I'm trying this set of constraints :

init{
int x = [-20;20];
int y = [-1;2];
}

constraints{
x - y > 1;
x - y < 0;
}

When solving this (with the command $ ./solver.opt problems/test.txt ),
I get
solving ends
Unique solution - #created nodes: 2

I don't think it should be possible.
I've looked at the other problems and I think that the syntax is correct.

What I've tried :
-using real instead of int : same problem
-using different domains : same problem sometimes. But with y in [0;2] for instance the problem disappear (the solver say that there are no solutions).
-using another precision that the default one (with the option -p). Even with precision 0 or precision 120, I still get one solution
-with not strict inequalities (typing >= and <=) : same problem

I've also tried to locate the said solution. The visualization option does not help.
Thus I've tried to add constraints.
If I add the constraint y>1, no solution. So in the solution, y should be <= 1.
But if I add the constraint y<=1, no solutions either.
Is there a way to print the found solutions (other than the visualization option)?

Maybe I just did something wrong in the syntax or maybe I missed something, but I don't know what.

Step by step does not work when pruning is enabled.

Self explanatory

F.to_rat F.inf throws a signal FPE (floating point exception).
Can Mpqf represent infinite numbers? Nothing is written in its documentation.

This is problematic in the function var_bounds if the bounds are not constrained yet.

• change for rational constants
• add step by step visualization
• add visualization for reduced product
• add vpl
• add reduced product between box and vpl
• add test
• fix bug with non box abstract domain
• fix bug with reduced product (seg fault, floating point exception)
• build opam package
• add integers