diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-19 13:47:00 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-19 13:47:00 +0200 |
| commit | f4200a0aa90e2641ce1b0b1c54d00d9d4dd3b73e (patch) | |
| tree | 53b82c4d758d11936f0ee0d106ea0aaf75d48f61 /abstract/abs_interp.ml | |
| parent | 8286c7c23a47c166aa87337a3146cdf3b278b144 (diff) | |
| download | scade-analyzer-f4200a0aa90e2641ce1b0b1c54d00d9d4dd3b73e.tar.gz scade-analyzer-f4200a0aa90e2641ce1b0b1c54d00d9d4dd3b73e.zip | |
Did most of the boring stuff. Now, work on the abstract domain.
Diffstat (limited to 'abstract/abs_interp.ml')
| -rw-r--r-- | abstract/abs_interp.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 1d3e20a..7950144 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -27,14 +27,10 @@ end = struct } - - (* init state *) let init_state widen_delay rp = let f = Formula.eliminate_not (Transform.f_of_prog rp false) in - let cl = Formula.conslist_of_f f in let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in - let cl_g = Formula.conslist_of_f f_g in let env = List.fold_left (fun env (_, id, ty) -> E.addvar env id ty) @@ -58,6 +54,9 @@ end = struct let env = E.apply_f env init_f in + let cl = Formula.conslist_of_f f in + let cl_g = Formula.conslist_of_f f_g in + { rp; widen_delay; f; cl; f_g; cl_g; guarantees; env } |