File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 1+ (* * Abstraktne väärtustaja ehk abstraktne interpretaator. *)
2+ open Ast
3+
4+ (* * Abstraktseid väärtustajaid saab luua kasutades erinevaid täisarve abstraheerivaid domeene.
5+ Vt. IntDomain. *)
6+ module Make (ID : IntDomain.S ) =
7+ struct
8+ (* * Väärtuskeskkonna domeen kasutades antud täisarvude domeeni. *)
9+ module ED = EnvDomain. Make (ID )
10+
11+ (* * Väärtustab avaldise keskkonnas.
12+ Vihje: ID.of_int.
13+ Vihje: ID.of_interval.
14+ Vihje: ID.eval_binary. *)
15+ let rec eval_expr (env : ED.t ) (expr : expr ): ID.t =
16+ failwith " TODO"
17+
18+ (* * Väärtustab valvuri (avaldis ja selle oodatav tõeväärtus) keskkonnas.
19+ Kui valvur on keskkonnaga vastuolus, siis tagastab saavutamatu programmi oleku ED.bot.
20+ Kui valvuriga saab keskkonna muutujate väärtusi täpsemaks kitsendada, siis võib keskkonda muuta.
21+ Võib jätta keskkonna muutmata, kuid siis ei kasutata valvurist saadavat lisainfot. *)
22+ let eval_guard (env : ED.t ) (expr : expr ) (branch : bool ): ED.t =
23+ failwith " TODO"
24+
25+ module EDFP = Fixpoint. MakeDomain (ED )
26+
27+ (* * Väärtustab lause keskkonnas.
28+ Vihje: Vea jaoks kasuta failwith funktsiooni.
29+ Vihje: eval_guard.
30+ Vihje: While jaoks kasuta püsipunkti moodulit EDFP. *)
31+ let rec eval_stmt (env : ED.t ) (stmt : stmt ): ED.t =
32+ failwith " TODO"
33+ end
Original file line number Diff line number Diff line change 1+ (library
2+ (name abseval)
3+ (libraries ast domain fixpoint))
You can’t perform that action at this time.
0 commit comments