- 15 Mar, 2013 3 commits
-
-
Andrei Paskevich authored
we really, really should implement blacklists in drivers
-
Andrei Paskevich authored
- recognize versioned executables - mark old versions as old - mark all Simplify versions old and I'd like to get rid of it completely
-
Andrei Paskevich authored
-
- 14 Mar, 2013 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 13 Mar, 2013 2 commits
-
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
- 12 Mar, 2013 3 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 11 Mar, 2013 1 commit
-
-
MARCHE Claude authored
-
- 10 Mar, 2013 2 commits
-
-
MARCHE Claude authored
-
Guillaume Melquiond authored
-
- 08 Mar, 2013 8 commits
-
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
- 07 Mar, 2013 8 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Andrei Paskevich authored
-
- 06 Mar, 2013 7 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
also, fix the evaluation order to left-to-right in e_binop. Thanks to Johannes for the bug report.
-
Jean-Christophe Filliâtre authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
This fixes the bug with .dep cleaning, when we don't build the IDE. Also, can we merge the replayer into why3session already, please?
-
- 04 Mar, 2013 5 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Andrei Paskevich authored
We store in every lsymbol a new integer field ls_constr, equal to zero if the lsymbol is not a constructor, and equal to the number of constructors of the lsymbol's type otherwise. It is allowed to declare or define an lsymbol with ls_constr > 0 as an ordinary function (otherwise algebraic type elimination wouldn't work - though we might still check this in theories), but it is forbidden to use a wrong ls_constr in algebraic type definitions. The ghostness of a match expression is now determined as follows: If at least one branch expression is ghost, then the match is ghost; else if there is only one branch, then the match is not ghost; else if the matched expression is ghost, then the match is ghost; else if at least one pattern matches a ghost field against a constructor with ls_constr > 1 then the match is ghost; else the match is not ghost. We do just enough to recognize obvious non-ghost cases, and make no attempt to handle redundant matches or to detect exhaustive or-patterns in subpatterns.
-