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
db474433
Commit
db474433
authored
Jan 11, 2011
by
Jean-Christophe
Browse files
programs: a bug to be fixed
parent
b1efe700
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/programs/pgm_typing.ml
View file @
db474433
...
...
@@ -1360,6 +1360,7 @@ and letrec gl env dl = (* : env * recfun list *)
map_fold_left
type1
Mvs
.
empty
dl
in
let
rec
fixpoint
m
=
(* printf "fixpoint...@\n"; *)
let
m'
,
dl'
=
one_step
m
in
let
same_effect
(
i
,_,_,_,_
)
=
E
.
equal
(
Mvs
.
find
i
.
i_pgm
m
)
.
c_effect
(
Mvs
.
find
i
.
i_pgm
m'
)
.
c_effect
...
...
tests/test-pgm-jcf.mlw
View file @
db474433
...
...
@@ -4,12 +4,8 @@ module P
use import int.Int
use import module stdlib.Ref
let f (a : ref int) = a
(* let rec f5 (a b:ref int) variant { a } = *)
(* { a >= 0 } *)
(* if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end *)
(* { result = old a + old b } *)
let rec f5 (a b : ref int) =
if True then !b else f5 a b
end
...
...
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