Adding test case that fails if contracts can initiate transactions.

INSTALL.md

@@ -6,17 +6,11 @@ The following are dynamically installed at VeriSol runtime (the first time only)
 
 - Follow either **Nuget** package installation directly, or after building the **sources**.
 
-### Install from nuget.org
-Install to the **global** dotnet CLI tools cache so that you can run command  `VeriSol` from anywhere:
-```
-dotnet tool install VeriSol --version 0.1.1-alpha --global
-```
-
 ### Install from sources
 
 Perform the following set of commands:
 ```
-git clone https://github.com/microsoft/verisol.git
+git clone https://github.com/utopia-group/verisol.git
 ```
 
 From %VERISOL_PATH%  (the root folder of the repository), perform

Sources/BoogieAST/BoogieAST.cs

@@ -317,19 +317,29 @@ public class BoogieImplementation : BoogieDeclWithFormals
 
         public BoogieStmtList StructuredStmts { get; set; }
 
-        public BoogieImplementation(string name, List<BoogieVariable> inParams, List<BoogieVariable> outParams, List<BoogieVariable> localVars, BoogieStmtList stmts)
+        public BoogieImplementation(string name, List<BoogieVariable> inParams, List<BoogieVariable> outParams, List<BoogieVariable> localVars, BoogieStmtList stmts, List<BoogieAttribute> attributes = null)
         {
             this.Name = name;
             this.InParams = inParams;
             this.OutParams = outParams;
             this.LocalVars = localVars;
             this.StructuredStmts = stmts;
+            this.Attributes = attributes;
         }
 
         public override string ToString()
         {
             StringBuilder builder = new StringBuilder();
-            builder.Append("implementation ").Append(Name).Append("(");
+            builder.Append("implementation ");
+            if (Attributes != null)
+            {
+                foreach (BoogieAttribute attribute in Attributes)
+                {
+                    builder.Append(attribute).Append(" ");
+                }
+            }
+
+            builder.Append(Name).Append("(");
             if (InParams.Count > 0)
             {
                 foreach (BoogieVariable inParam in InParams)
@@ -925,6 +935,14 @@ public override string ToString()
     public abstract class BoogieStructuredCmd : BoogieCmd
     {
     }
+
+    public class BoogieWildcardExpr : BoogieExpr
+    {
+        public override string ToString()
+        {
+            return "*";
+        }
+    }
 
     public class BoogieIfCmd : BoogieStructuredCmd
     {
@@ -1212,6 +1230,8 @@ public enum Opcode
             UNKNOWN,
         }
 
+        public static bool USE_ARITH_OPS { get; set; }
+
         public Opcode Op { get; set; }
 
         public BoogieExpr Lhs { get; set; }
@@ -1245,9 +1265,9 @@ public static string OpcodeToString(Opcode op)
                 case Opcode.MUL:
                     return "*";
                 case Opcode.DIV:
-                    return "div";
+                    return USE_ARITH_OPS ? "/" : "div";
                 case Opcode.MOD:
-                    return "mod";
+                    return USE_ARITH_OPS ? "%" : "mod";
                 case Opcode.EQ:
                     return "==";
                 case Opcode.NEQ:

Sources/SolToBoogie/BoogieTranslator.cs

@@ -1,5 +1,8 @@
 // Copyright (c) Microsoft Corporation. All rights reserved.
 // Licensed under the MIT license.
+
+using SolidityAnalysis;
+
 namespace SolToBoogie
 {
     using System;
@@ -19,11 +22,10 @@ public BoogieAST Translate(AST solidityAST, HashSet<Tuple<string, string>> ignor
             bool generateInlineAttributesInBpl = _translatorFlags.GenerateInlineAttributes;
 
             SourceUnitList sourceUnits = solidityAST.GetSourceUnits();
-
-            TranslatorContext context = new TranslatorContext(ignoredMethods, generateInlineAttributesInBpl, _translatorFlags, entryPointContract);
+            
+            TranslatorContext context = new TranslatorContext(solidityAST, ignoredMethods, generateInlineAttributesInBpl, _translatorFlags, entryPointContract);
             context.IdToNodeMap = solidityAST.GetIdToNodeMap();
             context.SourceDirectory = solidityAST.SourceDirectory;
-
             // collect the absolute source path and line number for each AST node
             SourceInfoCollector sourceInfoCollector = new SourceInfoCollector(context);
             sourceUnits.Accept(sourceInfoCollector);
@@ -65,8 +67,11 @@ public BoogieAST Translate(AST solidityAST, HashSet<Tuple<string, string>> ignor
             FunctionEventResolver functionEventResolver = new FunctionEventResolver(context);
             functionEventResolver.Resolve();
 
+            // Generate map helper
+            MapArrayHelper mapHelper = new MapArrayHelper(context, solidityAST);
+
             // add types, gobal ghost variables, and axioms
-            GhostVarAndAxiomGenerator generator = new GhostVarAndAxiomGenerator(context);
+            GhostVarAndAxiomGenerator generator = new GhostVarAndAxiomGenerator(context, mapHelper);
             generator.Generate();
 
             // collect modifiers information
@@ -77,8 +82,15 @@ public BoogieAST Translate(AST solidityAST, HashSet<Tuple<string, string>> ignor
             UsingCollector usingCollector = new UsingCollector(context);
             sourceUnits.Accept(usingCollector);
 
+            if (context.TranslateFlags.PerformFunctionSlice)
+            {
+                FunctionDependencyCollector depCollector = new FunctionDependencyCollector(context, entryPointContract, context.TranslateFlags.SliceFunctionNames);
+                context.TranslateFlags.SliceFunctions = depCollector.GetFunctionDeps();
+                context.TranslateFlags.SliceModifiers = depCollector.getModifierDeps();
+            }
+
             // translate procedures
-            ProcedureTranslator procTranslator = new ProcedureTranslator(context, generateInlineAttributesInBpl);
+            ProcedureTranslator procTranslator = new ProcedureTranslator(context, mapHelper, generateInlineAttributesInBpl);
             sourceUnits.Accept(procTranslator);
 
             // generate fallbacks
@@ -104,6 +116,12 @@ public BoogieAST Translate(AST solidityAST, HashSet<Tuple<string, string>> ignor
                 modSetAnalysis.PerformModSetAnalysis();
             }
 
+            if (context.TranslateFlags.GenerateERC20Spec)
+            {
+                ERC20SpecGenerator specGen = new ERC20SpecGenerator(context, solidityAST, entryPointContract);
+                specGen.GenerateSpec();
+            }
+
             return new BoogieAST(context.Program);
         }
     }