From 30347b268fbc1e386066842cbc8b08a1d0d8ed2e Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 25 Jan 2013 17:53:29 -0800 Subject: updated answer files og and linear creates some rearrangement of blocks --- Test/aitest0/Answer | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'Test/aitest0/Answer') diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer index fe848aab..18359b2e 100644 --- a/Test/aitest0/Answer +++ b/Test/aitest0/Answer @@ -24,14 +24,7 @@ implementation Join(b: bool) y := 4; z := x + y; assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7; - goto Then, Else; - - Then: - assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7; - assume b <==> true; - x := x + 1; - assume {:inferred} GlobalFlag && x == 4 && y == 4 && z == 7 && b; - goto join; + goto Then, Else; Else: assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7; @@ -47,6 +40,13 @@ implementation Join(b: bool) assert GlobalFlag <==> true; assume {:inferred} GlobalFlag && 3 <= x && x < 5 && y == 4 && z == 7; return; + + Then: + assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7; + assume b <==> true; + x := x + 1; + assume {:inferred} GlobalFlag && x == 4 && y == 4 && z == 7 && b; + goto join; } @@ -72,17 +72,17 @@ implementation Loop() assume {:inferred} c == 0 && 0 <= i && i < 11; goto Then, Else; + Else: + assume {:inferred} c == 0 && 0 <= i && i < 11; + assume {:inferred} c == 0 && 0 <= i && i < 11; + return; + Then: assume {:inferred} c == 0 && 0 <= i && i < 11; assume i < 10; i := i + 1; assume {:inferred} c == 0 && 1 <= i && i < 11; goto test; - - Else: - assume {:inferred} c == 0 && 0 <= i && i < 11; - assume {:inferred} c == 0 && 0 <= i && i < 11; - return; } -- cgit v1.2.3