Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.

4 files changed, 4 insertions, 63 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 630f6f14..9a0fe64e 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -494,8 +494,6 @@ namespace Microsoft.Boogie {
 

     public override void Typecheck(TypecheckingContext tc) {

       //Contract.Requires(tc != null);

-      if (Val is BvConst && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None)

-        tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag");

       this.Type = ShallowType;

     }

 

@@ -2241,9 +2239,6 @@ namespace Microsoft.Boogie {
                TypeParameters == null) {

         TypeParamInstantiation tpInsts;

         Type = Fun.Typecheck(ref Args, out tpInsts, tc);

-        if (Type != null && Type.IsBv && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None) {

-          tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag");

-        }

         TypeParameters = tpInsts;

       }

       IOverloadedAppliable oa = Fun as IOverloadedAppliable;

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4ebad5cc..8647e79e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -241,7 +241,6 @@ namespace Microsoft.Boogie {
       Z3Native,

       ToInt

     }

-    public BvHandling Bitvectors = BvHandling.Z3Native;

     public bool UseArrayTheory = false;

     public bool MonomorphicArrays {

       get {

@@ -945,31 +944,6 @@ namespace Microsoft.Boogie {
             ForceBplErrors = true;

             break;

 

-          case "-bv":

-          case "/bv":

-            if (ps.ConfirmArgumentCount(1)) {

-              if (TheProverFactory == null) {

-                TheProverFactory = ProverFactory.Load("Z3");

-                ProverName = "Z3".ToUpper();

-              }

-

-              switch (args[ps.i]) {

-                case "n":

-                  Bitvectors = BvHandling.None;

-                  break;

-                case "z":

-                  Bitvectors = BvHandling.Z3Native;

-                  break;

-                case "i":

-                  Bitvectors = BvHandling.ToInt;

-                  break;

-                default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

-              }

-            }

-            break;

-

           case "-contractInfer":

           case "/contractInfer":

             ContractInfer = true;

@@ -1918,15 +1892,6 @@ namespace Microsoft.Boogie {
      {:verify false}

        Skip verification of an implementation.

 

-     {:forceBvZ3Native true}

-       Verify the given implementation with the native Z3 bitvector

-       handling. Only works if /bv:i (or /bv:z, but then it does not do

-       anything) is given on the command line.

-

-     {:forceBvInt true}

-       Use int translation for the given implementation. Only work with

-       /bv:z (or /bv:i).

-

      {:vcs_max_cost N}

      {:vcs_max_splits N}

      {:vcs_max_keep_going_splits N}

@@ -1942,12 +1907,9 @@ namespace Microsoft.Boogie {
 

   ---- On functions ----------------------------------------------------------

 

+     {:builtin ""spec""}

      {:bvbuiltin ""spec""}

-       Z3 specific, used only with /bv:z.

-

-     {:bvint ""fn""}

-       With /bv:i rewrite the function to function symbol 'fn', except if

-       the 'fn' is 'id', in which case just strip the function altogether.

+       Rewrite the function to built-in prover function symbol 'fn'.

 

      {:never_pattern true}

        Terms starting with this function symbol will never be

@@ -2177,10 +2139,6 @@ namespace Microsoft.Boogie {
                    statement in that position) is ignored in checking contexts

                    (like other free things); this option includes these free

                    loop invariants as assumes in both contexts

-  /bv:<bv>       : bitvector handling

-                   n = none

-                   z = native Z3 bitvectors (default)

-                   i = unsoundly translate bitvectors to integers

   /inline:<i>    : use inlining strategy <i> for procedures with the :inline

                    attribute, see /attrHelp for details:

                    none

diff --git a/Source/Provers/Isabelle/Prover.cs b/Source/Provers/Isabelle/Prover.cs
index 60a8de22..8bf6bbf0 100644
--- a/Source/Provers/Isabelle/Prover.cs
+++ b/Source/Provers/Isabelle/Prover.cs
@@ -192,7 +192,7 @@ namespace Microsoft.Boogie.Isabelle {
     public readonly bool AllTypes;

 

     public IsabelleContext(string outputFilename, bool allTypes)

-      : base(new VCExpressionGenerator(), new VCGenerationOptions(new List<string/*!*/>(new string/*!*/[] { "bvInt", "bvDefSem", "bvint", "bvz", "external" }))) {

+      : base(new VCExpressionGenerator(), new VCGenerationOptions(new List<string/*!*/> { "bvInt", "bvDefSem", "bvint", "bvz", "external" })) {

       Contract.Requires(outputFilename != null);

 

       this.OutputFilename = outputFilename;

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 134cff4c..24e083d0 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -49,19 +49,7 @@ namespace Microsoft.Boogie {
     public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);

 

     private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) {

-      if (impl == null)

-        return CommandLineOptions.Clo.Bitvectors;

-      bool force_int = false;

-      bool force_native = false;

-      cce.NonNull(impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int);

-      impl.Proc.CheckBooleanAttribute("forceBvZ3Native", ref force_native);

-      impl.CheckBooleanAttribute("forceBvInt", ref force_int);

-      impl.CheckBooleanAttribute("forceBvZ3Native", ref force_native);

-      if (force_native)

-        return CommandLineOptions.BvHandling.Z3Native;

-      if (force_int)

-        return CommandLineOptions.BvHandling.ToInt;

-      return CommandLineOptions.Clo.Bitvectors;

+      return CommandLineOptions.BvHandling.Z3Native;

     }

 

     public bool WillingToHandle(Implementation impl, int timeout) {