summaryrefslogtreecommitdiff
path: root/main.ml
Commit message (Collapse)AuthorAgeFilesLines
* 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
| | | | | | - Use correect clock scope in typing - De-activate multi-valuated domain for enumerate vars + var couples. - Add comment explaining why it doesn't work
* Many things, sorry for the mess.Alex Auvolat2014-06-261-4/+6
| | | | | | | | | | - Implement two new enumeration domains (they don't bring us much) : multi valuation for variables ; multi valuation for variables and pairs of variables (not really sure it works) - Make it so that the number of init/time variables is reduced (do not create new init/time variables on node instanciation, only inside activate blocks and automaton states) - Some work on EDD (it is currently broken and does not compile)
* 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