summaryrefslogtreecommitdiff
path: root/main.ml
Commit message (Expand)AuthorAgeFilesLines
* Implement selection of disjunction variables for EDDs.Alex Auvolat2014-07-301-2/+23
* Plug into Apron Box domain for intervals.Alex Auvolat2014-07-241-7/+9
* Add support for octagons.Alex Auvolat2014-07-221-13/+22
* Clean up & comment a bit.Alex Auvolat2014-07-151-2/+18
* DP locations defined by abstract values and not by formula.Alex Auvolat2014-07-101-0/+9
* Fix a few things, this doesn't work well.Alex Auvolat2014-07-101-2/+24
* Now it's starting to work...Alex Auvolat2014-07-091-1/+8
* Begin dynamic partitionning ; CORRECT BUG IN unpass_cycle !!Alex Auvolat2014-07-091-11/+34
* Add ternaries, simplifications. BIG BUG FOUND (init/reset translation)Alex Auvolat2014-07-081-2/+2
* Revert that. We have two different domain kinds for enums, that's all.Alex Auvolat2014-07-081-2/+2
* Adapt abs_interp to use ENUM_DOMAIN2 (this is a test...)Alex Auvolat2014-07-081-2/+4
* Adapt domain with non-EDD disjunctions ; it doesn't work very well !Alex Auvolat2014-07-041-7/+10
* New example ; minor fixes.Alex Auvolat2014-07-041-1/+1
* Use LAST instead of NEXT (only EDD implementation works at the moment)Alex Auvolat2014-07-041-1/+6
* More verbosity ; adapt rfollow so that it can be provedAlex Auvolat2014-07-021-1/+4
* Implement chaotic iterations on EDDs. Global widening is missing.Alex Auvolat2014-06-301-2/+10
* More work on EDDs.Alex Auvolat2014-06-271-4/+3
* Minor corrections.Alex Auvolat2014-06-261-2/+2
* Many things, sorry for the mess.Alex Auvolat2014-06-261-4/+6
* Begin implementation of EDD ; SCA implemented.Alex Auvolat2014-06-251-1/+8
* Add command line option : verbose chaotic iterations.Alex Auvolat2014-06-251-2/+11
* Implementation of disjunction domain seems to work.Alex Auvolat2014-06-241-10/+21
* Not much. Still does not work very well.Alex Auvolat2014-06-201-7/+18
* Isolate numerical part of domain. Next: isolate numerical part of equations.Alex Auvolat2014-06-191-2/+6
* Do some typing ; support multiple pre in abstract interpretation.Alex Auvolat2014-06-191-3/+3
* Nice view of guarantees ; add half test, proved.Alex Auvolat2014-06-181-5/+5
* Add gilbreath suite ; booleans are not represented in a good way.Alex Auvolat2014-06-181-2/+12
* Abstract interpretation gives good results on the limiter example.Alex Auvolat2014-06-181-1/+1
* Add intervals domain ; some interesting analysis works.Alex Auvolat2014-06-181-1/+2
* Some abstract interpretation does something now.Alex Auvolat2014-06-171-6/+2
* Add bindings to apron. Next : work on abstract interpret.Alex Auvolat2014-06-171-0/+2
* Write transformation of program into logical formula.Alex Auvolat2014-06-171-0/+6
* Add AST for logical formula.Alex Auvolat2014-06-171-38/+33
* Begin of new interpret with more imperative concepts. Scope activation 'n stuff.Alex Auvolat2014-06-131-20/+26
* Move a lot of things.Alex Auvolat2014-06-131-11/+14
* Nothing.Alex Auvolat2014-06-121-1/+1
* Adopt same output format as test.cAlex Auvolat2014-06-121-14/+37
* Working prototype for an interpret ! But very messy.Alex Auvolat2014-06-121-1/+25
* Initial commit: parser for tiny subset of SCADE language...Alex Auvolat2014-06-111-0/+25