MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 5f65268e authored by Asma Tafat's avatar Asma Tafat
Browse files

blocking semantics

parent f1943861
......@@ -624,47 +624,39 @@ simpl.
assert (h: 2%Z = ((1%Z) + (1%Z))%Z).
omega.
rewrite h.
pose (pi := (Cons (x, Vint 42) Nil)).
fold pi.
pose (s1 := (Ebin (Evar x) Oplus (Evalue (Vint 13)))).
fold s1.
pose (s3 := (Evalue (Vint 55))).
fold s3.
pose (s2 := (Ebin (Evalue (get_stack x pi)) Oplus (Evalue (Vint 13)))).
fold s2.
assert ((one_step (const (Vint 0)) pi s1
(const (Vint 0)) pi s2)).
assert ((one_step (const (Vint 0)) pi s1 (const (Vint 0)) pi s2)).
apply one_step_bin_ctxt1.
apply one_step_var.
assert ((many_steps (const (Vint 0)) pi s2
(const (Vint 0)) pi s3 1)).
pose (s4 := Evalue (eval_bin (get_stack x pi) Oplus (Vint 13))).
assert ((one_step (const (Vint 0)) pi s2
(const (Vint 0)) pi s4)).
pose (s3 := Evalue (eval_bin (get_stack x pi) Oplus (Vint 13))).
assert ((one_step (const (Vint 0)) pi s2 (const (Vint 0)) pi s3)).
apply one_step_bin_value.
assert ((many_steps (const (Vint 0)) pi s4
(const (Vint 0)) pi s3 0)).
assert (s3 = s4).
unfold s4.
assert (Evalue (eval_bin (get_stack x pi) Oplus (Vint 13)) = Evalue (Vint 55)).
admit.
rewrite H1.
apply many_steps_refl.
apply many_steps_trans with
(sigma2 := (const (Vint 0))) (pi2 := pi) (s2 := s2); auto.
apply many_steps_trans; auto.
clear h.
assert (h: 1%Z = ((0%Z) + (1%Z))%Z).
omega.
rewrite h.
apply many_steps_trans with
(sigma2 := (const (Vint 0))) (pi2 := pi) (s2 := s2); auto.
(sigma2 := (const (Vint 0))) (pi2 := pi) (s2 := s3); auto.
rewrite <- H1.
apply many_steps_refl.
Qed.
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