Skip to content
Snippets Groups Projects
Commit 2ba796ff authored by Hai Dang's avatar Hai Dang
Browse files

Merge branch 'ci/weak_mem_mangle_names' into 'masters/weak_mem' 

Enable mangled  names

See merge request !30
parents 623d628b ed863f8b
No related branches found
No related tags found
1 merge request!30Enable mangled names
Pipeline #83632 failed
Stage: build
Hide whitespace changes
Inline Side-by-side
.gitlab-ci.yml
+ 1
− 0
View file @ 2ba796ff
...@@ -33,6 +33,7 @@ build-coq.8.17.0: ...@@ -33,6 +33,7 @@ build-coq.8.17.0:
variables: variables:
OPAM_PINS: "coq version 8.17.0" OPAM_PINS: "coq version 8.17.0"
DENY_WARNINGS: "1" DENY_WARNINGS: "1"
MANGLE_NAMES: "1"
tags: tags:
- fp-timing - fp-timing
......
theories/lang/memcpy.v
+ 0
− 1
View file @ 2ba796ff
...@@ -32,7 +32,6 @@ Proof. ...@@ -32,7 +32,6 @@ Proof.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia). - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !own_loc_na_vec_cons. subst n. revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !own_loc_na_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]". iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus.
wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|]. wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
iIntros "!> [Hl1 Hl2]"; iApply "HΦ"; by iFrame. iIntros "!> [Hl1 Hl2]"; iApply "HΦ"; by iFrame.
Qed. Qed.
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