- 21 Feb, 2016 3 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
Lsymbols in programs are probably more trouble than they are worth. It took me ten minutes to find out why the whole program was ghost.
-
Andrei Paskevich authored
-
- 20 Feb, 2016 9 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
Instead, we use more cautious simplification in Vc.
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 17 Feb, 2016 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 16 Feb, 2016 3 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 12 Feb, 2016 1 commit
-
-
Andrei Paskevich authored
-
- 11 Feb, 2016 1 commit
-
-
Andrei Paskevich authored
-
- 10 Feb, 2016 3 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
Dexpr checks for this earlier and adds "_ -> absurd" when needed.
-
Andrei Paskevich authored
-
- 09 Feb, 2016 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 02 Feb, 2016 1 commit
-
-
Andrei Paskevich authored
-
- 31 Jan, 2016 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 26 Jan, 2016 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 24 Jan, 2016 1 commit
-
-
Andrei Paskevich authored
also, rename asym_label to asym_split and keep_on_simp_label to keep_on_simp.
-
- 17 Jan, 2016 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 11 Jan, 2016 3 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
This makes "let f ... : unit = <effect> ; <ghost effect>" acceptable without ghostness annotation in the result. However, "let f ... : unit = <ghost effect>" is still required to be marked ghost (unless f is a local non-recursive function).
-
Andrei Paskevich authored
Refutable ghost subpatterns that are not followed by a non-absurd branch are actually irrefutable and do not make the whole match-with expression ghost.
-
- 10 Jan, 2016 1 commit
-
-
Andrei Paskevich authored
this is still work in progress and no testing was done so far. Highlights of this commit: - "(ghost 42, 15)" is now a non-ghost expression that can be returned from a function and/or matched against a "(ghost x, y)" pattern. Only the tuple constructor and direct pattern matching are magical: "let z = (ghost 42, 15) in ..." still makes z ghost, and therefore "snd (ghost 42, 15)" is ghost, too. - "if c then e1 else ghost e2" and "let z = e1 in ghost e2" are now non-ghost expressions with a ghost result. This means that e1 may have visible effects. Of course, if e2 raises exceptions, the whole expression is ghostified. Contamination is still done when possible, that is, when the contaminated expression has no visible effects. - "let ghost x = e1 in e2" no longer ghostifies e1. - "let f (ghost x) = ... in f e1" no longer ghostifies e1. - new syntax: variables in program patterns may be marked ghost. In particular: "let x, ghost y = ...". - new syntax: the function result type may be written as a partially ghost tuple: "val f ... : ghost int" or "any (int, ghost bool)". The ghostness annotation is required for top-level and recursive functions. - exceptions can carry partially ghost tuples (API only, WIP)
-
- 11 Dec, 2015 1 commit
-
-
MARCHE Claude authored
make bench should not - build why3extract (not ready yet) - test the API of programs (is changed, tests has to be updated first) - test extraction (not ready yet)
-
- 07 Dec, 2015 3 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
Andrei Paskevich authored
This reverts commit e368d43a.
-