Commit 9491b639 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid

eval_expr

parent 7c91d500
......@@ -300,23 +300,23 @@ predicate eval_fmla (sigma:env) (pi:stack) (f:fmla) =
end
function eval_expr (sigma:env) (pi:stack) (e:expr) : value =
match e with
| Evalue v -> v
| Evar id -> get_stack id pi
| Ederef id -> get_env id sigma
| Ebin e1 op e2 ->
eval_bin (eval_expr sigma pi e1) op (eval_expr sigma pi e2)
| Eassign id e1
| Eseq e1 e2
| Elet id e1 e2 -> void
| Eif e1 e2 e3 ->
if ((eval_expr sigma pi e1) = (Vbool True))
then eval_expr sigma pi e2
else eval_expr sigma pi e3
| Eassert f -> eval_fmla f
| Ewhile expr fmla expr ->
end
(* function eval_expr (sigma:env) (pi:stack) (e:expr) : value = *)
(* match e with *)
(* | Evalue v -> v *)
(* | Evar id -> get_stack id pi *)
(* | Ederef id -> get_env id sigma *)
(* | Ebin e1 op e2 -> *)
(* eval_bin (eval_expr sigma pi e1) op (eval_expr sigma pi e2) *)
(* | Eassign id e1 *)
(* | Eseq e1 e2 *)
(* | Elet id e1 e2 -> void *)
(* | Eif e1 e2 e3 -> *)
(* if ((eval_expr sigma pi e1) = (Vbool True)) *)
(* then eval_expr sigma pi e2 *)
(* else eval_expr sigma pi e3 *)
(* | Eassert f -> eval_fmla f *)
(* | Ewhile expr fmla expr -> *)
(* end *)
(** substitution of a reference [r] by a logic variable [v]
warning: proper behavior only guaranted if [v] is "fresh",
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment