Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
32943e89
Commit
32943e89
authored
Jan 08, 2014
by
MARCHE Claude
Browse files
interp: eval also ghost expressions
parent
f35196cc
Changes
2
Hide whitespace changes
Inline
Side-by-side
examples/fibonacci.mlw
View file @
32943e89
...
...
@@ -149,5 +149,6 @@ module FibonacciLogarithmic
let test1 () = fibo 1
let test7 () = fibo 7
let test42 () = fibo 42
let test2014 () = fibo 2014
end
src/whyml/mlw_interp.ml
View file @
32943e89
...
...
@@ -833,10 +833,10 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
end
|
Eassign
(
_pl
,_
e1
,
reg
,
pvs
)
->
let
t
=
get_pvs
env
s
pvs
in
(*
(*
*)
eprintf
"updating region <%a> with value %a@."
Mlw_pretty
.
print_reg
reg
Pretty
.
print_term
t
;
*)
(*
*)
let
r
=
try
Mreg
.
find
reg
env
.
regenv
with
Not_found
->
reg
...
...
@@ -845,7 +845,9 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
|
Eassert
_
->
(* TODO check the validity ! *)
Normal
t_void
,
s
|
Eghost
_
(* -> (* eval_expr env s e *) Normal t_void, s *)
|
Eghost
e1
->
(* TODO: do not eval ghost if no assertion check *)
eval_expr
env
s
e1
|
Erec
_
|
Eany
_
|
Eabstr
_
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment