Updated README.md, LICENSE.txt, and headers in all files of ViperProj…

…ect.

LICENSE.txt

@@ -1,4 +1,4 @@
-Silicon and all files of its source code are licensed under the Mozilla Public
+ViperServer and all files of its source code are licensed under the Mozilla Public
 License Version 2.0 (see below or http://www.mozilla.org/MPL/2.0/), with the
 following *exceptions*:
 
@@ -11,11 +11,11 @@ following *exceptions*:
     src/test/resources
     utils
 
-- Files found in src/main/resources/dafny_axioms (and its sub-directories),
-  which are licensed under Microsoft Public License (Ms-PL)
-
-
+- Files found in src/main/scala/viper/server/utility/apache (and its sub-directories),
+  which are licensed under Apache License, Version 2.0
 
+- Files found in src/main/scala/viper/server/utility/ibm (and its sub-directories),
+  which are licensed under Eclipse Public License 2.0
 
 
 Mozilla Public License Version 2.0

README.md

@@ -1,34 +1,27 @@
 # README #
 
-Viper Server
+This is ViperServer, an HTTP server that manages verification requests to different tools from the Viper tool stack.
 
-### What is this repository for? ###
+The main two tools currently are:
 
-* Quick summary
-* Version
-* [Learn Markdown](https://bitbucket.org/tutorials/markdowndemo)
+- [Carbon](https://bitbucket.org/viperproject/carbon), a verification condition generation (VCG) backend for the Viper language.
+- [Silicon](https://bitbucket.org/viperproject/silicon), a symbolic execution verification backend.
 
-### How do I get set up? ###
 
-* Summary of set up
-* Configuration
-* Dependencies
-* Database configuration
-* How to run tests
-* Deployment instructions
+### The Purpose of ViperServer ###
 
-### Contribution guidelines ###
+1. Viper IDE: integration of Viper into Visual Studio Code (VS Code). Viper IDE provides the best user experience for Viper.
+   More details here: http://viper.ethz.ch/downloads/
+2. Avoid 1-3 second delays caused by JVM startup time. ViperServer offers a robust alternative to, e.g.,
+   [Nailgun](https://github.com/facebook/nailgun).
+3. Develop Viper encodings more efficiently with caching.
+4. Interact with Viper tools programmatically using the HTTP API. A reference client implementation (in Python) is
+   available via [viper_client](https://bitbucket.org/viperproject/viper_client).
 
-* Writing tests
-* Code review
-* Other guidelines
+For more details, please visit: http://viper.ethz.ch/downloads/
 
-### Who do I talk to? ###
-
-* Repo owner or admin
-* Other community or team contact
 
-### Installation Instructions:
+### Installation Instructions ###
 
 * Clone [silver](https://bitbucket.org/viperproject/silver/), [silicon](https://bitbucket.org/viperproject/silicon/) and [carbon](https://bitbucket.org/viperproject/carbon/) repositories in your computer, in separate directories.
 * Clone **viperserver** (this repository) in your computer, in another directory.
@@ -45,4 +38,17 @@ mklink /D silver <relative path to diretory where you installed silver>
 mklink /D silicon <relative path to diretory where you installed silicon>  
 mklink /D carbon <relative path to diretory where you installed carbon>  
 ```
-* Compile by typing: ```sbt compile```
+* Compile by typing: ```sbt compile```
+
+* Other supported SBT commands are: ```sbt stage``` (produces fine-grained jar files), ```sbt assembly``` (produces a single fat jar file).
+
+### Running Tests ###
+
+* Set the environment variable ```Z3_EXE``` to an executable of a recent version of [Z3](https://github.com/Z3Prover/z3).
+
+* Run the following command: ```sbt test```.
+
+
+### Who do I talk to? ###
+
+* This repository is maintained by [Arshavir Ter-Gabrielyan](mailto:ter-gabrielyan@inf.ethz.ch).

src/main/resources/application.conf

@@ -1,3 +1,9 @@
+# This Source Code Form is subject to the terms of the Mozilla Public
+# License, v. 2.0. If a copy of the MPL was not distributed with this
+# file, You can obtain one at http://mozilla.org/MPL/2.0/.
+#
+# Copyright (c) 2011-2019 ETH Zurich.
+
 akka {
 
   http {

src/main/scala/viper/server/VerificationWorker.scala

@@ -1,7 +1,9 @@
-/*
+/**
  * This Source Code Form is subject to the terms of the Mozilla Public
  * License, v. 2.0. If a copy of the MPL was not distributed with this
  * file, You can obtain one at http://mozilla.org/MPL/2.0/.
+ *
+ * Copyright (c) 2011-2019 ETH Zurich.
  */
 
 package viper.server

src/main/scala/viper/server/ViperCache.scala

@@ -1,8 +1,10 @@
-/*
- * This Source Code Form is subject to the terms of the Mozilla Public
- * License, v. 2.0. If a copy of the MPL was not distributed with this
- * file, You can obtain one at http://mozilla.org/MPL/2.0/.
- */
+/**
+  * This Source Code Form is subject to the terms of the Mozilla Public
+  * License, v. 2.0. If a copy of the MPL was not distributed with this
+  * file, You can obtain one at http://mozilla.org/MPL/2.0/.
+  *
+  * Copyright (c) 2011-2019 ETH Zurich.
+  */
 
 package viper.server
 

src/main/scala/viper/server/ViperConfig.scala

@@ -1,8 +1,18 @@
+/**
+  * This Source Code Form is subject to the terms of the Mozilla Public
+  * License, v. 2.0. If a copy of the MPL was not distributed with this
+  * file, You can obtain one at http://mozilla.org/MPL/2.0/.
+  *
+  * Copyright (c) 2011-2019 ETH Zurich.
+  */
+
 package  viper.server
 
 import java.io.File
 
 import org.rogach.scallop.{ScallopConf, ScallopOption, singleArgConverter}
+import viper.server.utility.ibm
+import viper.server.utility.ibm.Socket
 
 class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
 
@@ -79,11 +89,11 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
 
   val port: ScallopOption[Int] = opt[Int]("port", 'p',
     descr = ("Specifies the port on which ViperServer will be started."
-      + s"The port must be an integer in range [${viper.server.utility.Sockets.MIN_PORT_NUMBER}-${viper.server.utility.Sockets.MAX_PORT_NUMBER}]"
+      + s"The port must be an integer in range [${Socket.MIN_PORT_NUMBER}-${ibm.Socket.MAX_PORT_NUMBER}]"
       + "If the option is omitted, an available port will be selected automatically."),
-    default = Some(viper.server.utility.Sockets.findFreePort),
+    default = Some(ibm.Socket.findFreePort),
     validate = p => try {
-      viper.server.utility.Sockets.available(p)
+      ibm.Socket.available(p)
     } catch {
       case e: Exception =>
         println(s"Invalid port $p: $e")

src/main/scala/viper/server/ViperIDEProtocol.scala

@@ -1,8 +1,10 @@
-/*
- * This Source Code Form is subject to the terms of the Mozilla Public
- * License, v. 2.0. If a copy of the MPL was not distributed with this
- * file, You can obtain one at http://mozilla.org/MPL/2.0/.
- */
+/**
+  * This Source Code Form is subject to the terms of the Mozilla Public
+  * License, v. 2.0. If a copy of the MPL was not distributed with this
+  * file, You can obtain one at http://mozilla.org/MPL/2.0/.
+  *
+  * Copyright (c) 2011-2019 ETH Zurich.
+  */
 
 package viper.server
 

src/main/scala/viper/server/ViperRequests.scala

@@ -1,3 +1,11 @@
+/**
+  * This Source Code Form is subject to the terms of the Mozilla Public
+  * License, v. 2.0. If a copy of the MPL was not distributed with this
+  * file, You can obtain one at http://mozilla.org/MPL/2.0/.
+  *
+  * Copyright (c) 2011-2019 ETH Zurich.
+  */
+
 package viper.server
 
 import spray.json._

src/main/scala/viper/server/ViperServer.scala

@@ -1,8 +1,10 @@
-/*
- * This Source Code Form is subject to the terms of the Mozilla Public
- * License, v. 2.0. If a copy of the MPL was not distributed with this
- * file, You can obtain one at http://mozilla.org/MPL/2.0/.
- */
+/**
+  * This Source Code Form is subject to the terms of the Mozilla Public
+  * License, v. 2.0. If a copy of the MPL was not distributed with this
+  * file, You can obtain one at http://mozilla.org/MPL/2.0/.
+  *
+  * Copyright (c) 2011-2019 ETH Zurich.
+  */
 
 package viper.server
 

src/main/scala/viper/server/ViperServerProtocol.scala

@@ -1,8 +1,10 @@
-/*
- * This Source Code Form is subject to the terms of the Mozilla Public
- * License, v. 2.0. If a copy of the MPL was not distributed with this
- * file, You can obtain one at http://mozilla.org/MPL/2.0/.
- */
+/**
+  * This Source Code Form is subject to the terms of the Mozilla Public
+  * License, v. 2.0. If a copy of the MPL was not distributed with this
+  * file, You can obtain one at http://mozilla.org/MPL/2.0/.
+  *
+  * Copyright (c) 2011-2019 ETH Zurich.
+  */
 
 package viper.server