Skip to content

C
c
Commit 509df330 authored by Dan Frumin's avatar Dan Frumin
Browse files
Options

remove an unnecessary sequence point

parent 6f90c357
Show whitespace changes
Inline Side-by-side
Showing with 1 addition and 2 deletions
theories/tests/store_strong.v
View file @ 509df330
...@@ -36,8 +36,7 @@ if `γl ≔ b1 ∗ γr ≔ b2`, then we have four possible situations by case-an ...@@ -36,8 +36,7 @@ if `γl ≔ b1 ∗ γr ≔ b2`, then we have four possible situations by case-an
*) *)
Definition storeme : val := λᶜ "l", Definition storeme : val := λᶜ "l", c_ret "l" =ᶜ ♯ 10.
c_ret "l" =ᶜ ♯ 10 ;ᶜ ♯ 10. (* want to have a sequence point at the end of the function *)
Definition test : val := λᶜ "l", Definition test : val := λᶜ "l",
callᶜ (c_ret storeme) (c_ret "l") +ᶜ (c_ret "l" =ᶜ ♯11). callᶜ (c_ret storeme) (c_ret "l") +ᶜ (c_ret "l" =ᶜ ♯11).
......
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