TODO

In PathCondition:

- check for errors (only if type is TA and only on the latest predicate)

- simplifications:
  - types (assert (is_Vxxx some_symbol))
  - values (once we get the model, (assert (distinct some_symbol value)))
  - with a parameter to branch if there is a few number of cases
  - problems :
    - need to keep a map of simplifications for each symbol (easy)
    - traverse the env, the heap, the output, the path condition to (possibly) simplify all values
    - which expression to remove from the path condition?

- other orders of search
  - BFS (usefull for a join operator)
  - code coverage (DFS with priorities)
  - shortest paths first (Dijkstra)

- analysis of functions separately with function summaries (with guard) interprocedural

- option -smt-timeout (0 => -no-smt)

- in interactive mode, continue computation in the background

- symbolic (uninterpreted) pure functions

- function try_branching symb_val f_app f_fallback
(could call the SMT solver ?)

- bounding on:
  - time
  - nb-paths (done)
  - recursion level

- assert must branch

Fun:

- PHP bindings for Jsxweb

- old(x) evaluates x in the context at the beginning of the function
   - problem with the "arguments" stuff ?

- two runs at the same time (product of states, only the path condition is common)

XDelta:
Optimization of some trivial cases
@x + 0 --> @x, @x <= +Infinity --> true, ...

Compilation:

- static compilation of Z3 bindings to be able to use JsxWeb again

- try with other SMT solvers

- option to replace the SMT env

- optimize embedded environments (print them as OCaml values instead of parsing them each time) with a priority on the SMT env

- -version

- Z3 version

LambdaJS:

- constructors for AST
- continue to implement the standard library
- if new primitives are needed, add them in es5_delta.ml (lambdaJS), xDelta.ml (Jsx) and env.smt2 (Jsx SMT environment)