From c03c5ba246565fcb3b16630051c6235f06c4bef8 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 1 Dec 2015 17:01:22 +0000 Subject: Teach TravisCI to use Z3 4.4.1 from repositories that I'm currently maintaining on the OpenSUSE build service. See https://build.opensuse.org/package/show/home:delcypher:z3/z3 --- .travis.yml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/.travis.yml b/.travis.yml index 11ed4d64..41ee569f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -6,14 +6,15 @@ env: - BOOGIE_CONFIG=Debug - BOOGIE_CONFIG=Release install: - - sudo apt-key adv --recv-keys --keyserver keyserver.ubuntu.com C504E590 - # FIXME: We should not be using GPUVerify's repo for Z3 - - sudo sh -c 'echo "deb http://ppa.launchpad.net/delcypher/gpuverify-smt/ubuntu precise main" > /etc/apt/sources.list.d/smt.list' + - wget http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_12.04/Release.key + - sudo apt-key add - < Release.key + # Use Z3 package built by the OpenSUSE build service https://build.opensuse.org/package/show/home:delcypher:z3/z3 + - sudo sh -c "echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_12.04/ /' >> /etc/apt/sources.list.d/z3.list" - sudo apt-get update # NuGet is a little flakey in legacy TravisCI, use travis_retry command to retry the command if it fails - travis_retry nuget restore ${TRAVIS_SOLUTION} - # Install Z3 - - sudo apt-get -y install z3=4.3.2-0~precise2 + # Install Z3 executable + - sudo apt-get -y install 'z3=4.4.1-*' # Install needed python tools - sudo pip install lit OutputCheck pyyaml - mkdir -p Source/packages && cd Source/packages && travis_retry nuget install NUnit.Runners -Version 2.6.3 -- cgit v1.2.3 From 75b5befa9f82f6fd54817d9cec20522af1a797a6 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 19 Nov 2015 18:23:03 -0600 Subject: Update test output for Z3 4.4.1. --- README.md | 2 +- Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect | 3 ++- Test/test15/CaptureState.bpl.expect | 18 +++++++++--------- 3 files changed, 12 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index a976b249..224d7196 100644 --- a/README.md +++ b/README.md @@ -48,7 +48,7 @@ You can also report issues on our [issue tracker](https://github.com/boogie-org/ ### Requirements - [NuGet](https://www.nuget.org/) -- [Z3](https://github.com/Z3Prover/z3) 4.3.2 or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note +- [Z3](https://github.com/Z3Prover/z3) 4.4.1 or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note CVC4 support is experimental) #### Windows specific diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect index 9f960f26..3c0d0b20 100644 --- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect +++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect @@ -127,7 +127,8 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(3832,3): inline$storm_IoCancelIrp$0$anon10#2 daytona_bug2_ioctl_example_2.bpl(3892,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2 daytona_bug2_ioctl_example_2.bpl(3902,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2 - daytona_bug2_ioctl_example_2.bpl(3928,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Then#2 + daytona_bug2_ioctl_example_2.bpl(3915,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2 + daytona_bug2_ioctl_example_2.bpl(3923,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2 daytona_bug2_ioctl_example_2.bpl(3933,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2 daytona_bug2_ioctl_example_2.bpl(3944,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2 daytona_bug2_ioctl_example_2.bpl(3949,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2 diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect index 5d9d41c5..6939fee4 100644 --- a/Test/test15/CaptureState.bpl.expect +++ b/Test/test15/CaptureState.bpl.expect @@ -14,17 +14,17 @@ $mv_state_const -> 3 F -> T@FieldName!val!0 Heap -> |T@[Ref,FieldName]Int!val!0| m -> **m -m@0 -> (- 276) -m@1 -> (- 275) -m@3 -> (- 275) +m@0 -> (- 2) +m@1 -> (- 1) +m@3 -> (- 1) r -> **r -r@0 -> (- 550) +r@0 -> (- 2) this -> T@Ref!val!0 x -> 719 y -> **y Select_[Ref,FieldName]$int -> { - |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 276) - else -> (- 276) + |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 2) + else -> (- 2) } $mv_state -> { 3 0 -> true @@ -49,13 +49,13 @@ tickleBool -> { *** STATE top *** END_STATE *** STATE then - m -> (- 276) + m -> (- 2) *** END_STATE *** STATE postUpdate0 - m -> (- 275) + m -> (- 1) *** END_STATE *** STATE end - r -> (- 550) + r -> (- 2) m -> 7 *** END_STATE *** END_MODEL -- cgit v1.2.3 From f97656456a74564cdf96633c3f46223d39e2c6f2 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 16 Nov 2015 11:03:28 -0800 Subject: Use the EndCurly token when creating the ReturnCmd for unifiedExit When there are more than one exit blocks, an unified exit block is created which includes a ReturnCmd. However, the ReturnCmd is created with NoToken. This causes the line/column number reported for a failed postcondition to be (0,0). The right token should be the EndCurly since the ReturnCmd is in the exit block. --- Source/VCGeneration/ConditionGeneration.cs | 3 ++- Test/test2/BadLineNumber.bpl | 15 +++++++++++++++ Test/test2/BadLineNumber.bpl.expect | 7 +++++++ 3 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 Test/test2/BadLineNumber.bpl create mode 100644 Test/test2/BadLineNumber.bpl.expect diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 6a2eec29..19438924 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1133,7 +1133,8 @@ namespace VC { } if (returnBlocks > 1) { string unifiedExitLabel = "GeneratedUnifiedExit"; - Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), new ReturnCmd(Token.NoToken)); + Block unifiedExit; + unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken)); Contract.Assert(unifiedExit != null); foreach (Block b in impl.Blocks) { if (b.TransferCmd is ReturnCmd) { diff --git a/Test/test2/BadLineNumber.bpl b/Test/test2/BadLineNumber.bpl new file mode 100644 index 00000000..b8776a4e --- /dev/null +++ b/Test/test2/BadLineNumber.bpl @@ -0,0 +1,15 @@ +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure p(); + ensures false; + +implementation p() +{ + if (*) + { + } + else + { + } +} \ No newline at end of file diff --git a/Test/test2/BadLineNumber.bpl.expect b/Test/test2/BadLineNumber.bpl.expect new file mode 100644 index 00000000..bc5d1984 --- /dev/null +++ b/Test/test2/BadLineNumber.bpl.expect @@ -0,0 +1,7 @@ +BadLineNumber.bpl(15,1): Error BP5003: A postcondition might not hold on this return path. +BadLineNumber.bpl(5,3): Related location: This is the postcondition that might not hold. +Execution trace: + BadLineNumber.bpl(9,5): anon0 + BadLineNumber.bpl(14,5): anon3_Else + +Boogie program verifier finished with 0 verified, 1 error -- cgit v1.2.3 From 3e4a58021e7f9b2bd31dd195f9a7b2f02d5b4c02 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 2 Dec 2015 09:27:06 +0000 Subject: TravisCI build icon should only show build status for master branch, not all branches. --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 224d7196..1dd0ba5a 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ |-------------------------------|---------------------------------| | [![linux build status][1]][2] | [![windows_build_status][3]][4] | -[1]: https://travis-ci.org/boogie-org/boogie.svg +[1]: https://travis-ci.org/boogie-org/boogie.svg?branch=master [2]: https://travis-ci.org/boogie-org/boogie [3]: https://pmbuilds.inf.ethz.ch/buildStatus/icon?job=boogie [4]: #FIXME -- cgit v1.2.3 From 9b355c4e494bc6427e3d165288c09e113a86000a Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 2 Dec 2015 12:02:43 -0600 Subject: Remove workaround for older versions of Z3. --- Source/VCGeneration/Check.cs | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index da445a00..8c1ae407 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -356,16 +356,8 @@ namespace Microsoft.Boogie { hasOutput = false; outputExn = null; this.handler = handler; - - if (namedAssumeVars != null && namedAssumeVars.Any()) - { - // TODO(wuestholz): Avoid doing a full reset. This is currently necessary for old versions of Z3 due to a bug. - thmProver.FullReset(gen); - } - else - { - thmProver.Reset(gen); - } + + thmProver.Reset(gen); SetTimeout(); proverStart = DateTime.UtcNow; thmProver.NamedAssumeVars = namedAssumeVars; -- cgit v1.2.3 From 9f50f449bef2aeed660a8e3c0b5eb73ad7fe1e78 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 3 Dec 2015 09:37:45 -0600 Subject: Remove unused directory. --- Build/CodePlex.Tools.MsBuild.dll | Bin 131072 -> 0 bytes Build/CodePlex.Tools.Wiki.dll | Bin 45056 -> 0 bytes Build/updateVersionFile.xml | 19 ------------------- 3 files changed, 19 deletions(-) delete mode 100644 Build/CodePlex.Tools.MsBuild.dll delete mode 100644 Build/CodePlex.Tools.Wiki.dll delete mode 100644 Build/updateVersionFile.xml diff --git a/Build/CodePlex.Tools.MsBuild.dll b/Build/CodePlex.Tools.MsBuild.dll deleted file mode 100644 index 2e400e8e..00000000 Binary files a/Build/CodePlex.Tools.MsBuild.dll and /dev/null differ diff --git a/Build/CodePlex.Tools.Wiki.dll b/Build/CodePlex.Tools.Wiki.dll deleted file mode 100644 index 9ea2bea8..00000000 Binary files a/Build/CodePlex.Tools.Wiki.dll and /dev/null differ diff --git a/Build/updateVersionFile.xml b/Build/updateVersionFile.xml deleted file mode 100644 index cb083c7a..00000000 --- a/Build/updateVersionFile.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - - - - - - -- cgit v1.2.3 From 8938d00be93e780d54917c1448bc534702766fdf Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 3 Dec 2015 09:39:44 -0600 Subject: Remove unused file. --- Source/version.ssc | 12 ------------ 1 file changed, 12 deletions(-) delete mode 100644 Source/version.ssc diff --git a/Source/version.ssc b/Source/version.ssc deleted file mode 100644 index 5bdcf170..00000000 --- a/Source/version.ssc +++ /dev/null @@ -1,12 +0,0 @@ -// ==++== -// -// -// -// ==--== -// Warning: Automatically generated file. DO NOT EDIT -// Generated at Dienstag, 5. Juli 2011 11:26:45 - -using System.Reflection; -[assembly: AssemblyVersion("2.2.30705.1126")] -[assembly: AssemblyFileVersion("2.2.30705.1126")] - -- cgit v1.2.3