Merge branch 'release-1.7.2'

smackers · Jan 8, 2017 · 01aaa6e · 01aaa6e
2 parents 435044d + 2f2d6a2
commit 01aaa6e
Show file tree

Hide file tree

Showing 17 changed files with 469 additions and 144 deletions.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -1,11 +1,16 @@
-# Contribution Guidelines
+## Contribution Guidelines
+
 
 The information provided here is a must read for anyone who would like to
 contribute to SMACK. Hence, please make sure to study thoroughly the following
 items before you start contributing:
-
-* We adhere to the [Open Code of Conduct](http://todogroup.org/opencodeofconduct/#SMACK/[email protected]). By participating, you are expected to honor this code.
-* We use this [git branching model](http://nvie.com/posts/a-successful-git-branching-model/). Please avoid working directly on the `master` branch.
-* We follow guidelines for [good git commit practice](https://wiki.openstack.org/wiki/GitCommitMessages)
-* We follow the [LLVM Coding Standards](http://llvm.org/docs/CodingStandards.html)
+* We adhere to the [Contributor Covenant Code of Conduct](docs/code-of-conduct.md).
+  By participating, you are expected to honor this code.
+* We use this [git branching
+  model](http://nvie.com/posts/a-successful-git-branching-model/). Please avoid
+  working directly on the `master` branch.
+* We follow guidelines for [good git commit
+  practice](https://wiki.openstack.org/wiki/GitCommitMessages)
+* We follow the [LLVM Coding
+  Standards](http://llvm.org/docs/CodingStandards.html)
 
diff --git a/Doxyfile b/Doxyfile
@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 1.7.1
+PROJECT_NUMBER         = 1.7.2
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs

diff --git a/LICENSE b/LICENSE
@@ -1,9 +1,10 @@
 The MIT License
 
-Copyright (c) 2008-2016 Zvonimir Rakamaric ([email protected]),
+Copyright (c) 2008-2017 Zvonimir Rakamaric ([email protected]),
                         Michael Emmi ([email protected])
-Modified work Copyright (c) 2013-2016 Pantazis Deligiannis,
-                                      Montgomery Carter,
+Modified work Copyright (c) 2013-2017 Montgomery Carter,
+                                      Pantazis Deligiannis,
+                                      Dietrich Geisler,
                                       Arvind Haran,
                                       Shaobo He,
                                       Jiten Thakkar,

diff --git a/README.md b/README.md
@@ -59,7 +59,7 @@ SMACK.
 1. [Demos](docs/demos.md)
 1. [FAQ](docs/faq.md)
 1. [Inline Boogie Code](docs/boogie-code.md)
-1. [Contribution Guidelines](docs/contributions.md)
+1. [Contribution Guidelines](CONTRIBUTING.md)
 1. [Projects](docs/projects.md)
 1. [Publications](docs/publications.md)
 1. [People](docs/people.md)

diff --git a/bin/package-smack.sh b/bin/package-smack.sh
@@ -6,7 +6,7 @@
 # Note: this script requires CDE to be downloaded from
 # http://www.pgbovine.net/cde.html
 
-VERSION=1.7.1
+VERSION=1.7.2
 PACKAGE=smack-$VERSION-64
 
 # Create folder to export

diff --git a/docs/contributions.md b/docs/contributions.md
diff --git a/docs/people.md b/docs/people.md
@@ -4,15 +4,16 @@
 ### Coordinators
 
 * [Michael Emmi](http://michael-emmi.github.io)
-* [Zvonimir Rakamaric](http://www.zvonimir.info/) ([SOAR Lab](http://soarlab.org/), University of Utah)
+* [Zvonimir Rakamaric](http://www.zvonimir.info) ([SOAR Lab](http://soarlab.org), University of Utah)
 
 
 ### Contributors
 
-* [Montgomery Carter](http://www.linkedin.com/pub/montgomery-carter/12/a89/512) ([SOAR Lab](http://soarlab.org/), University of Utah)
-* [Pantazis Deligiannis](http://pdeligia.github.io/) (Microsoft Research)
-* [Arvind Haran](http://www.cs.utah.edu/~haran) ([SOAR Lab](http://soarlab.org/), University of Utah)
-* [Shaobo He](http://www.cs.utah.edu/~shaobo) ([SOAR Lab](http://soarlab.org/), University of Utah)
-* [Jiten Thakkar](http://jiten-thakkar.com) ([SOAR Lab](http://soarlab.org/), University of Utah)
+* [Montgomery Carter](http://www.linkedin.com/pub/montgomery-carter/12/a89/512) ([SOAR Lab](http://soarlab.org), University of Utah)
+* [Pantazis Deligiannis](http://pdeligia.github.io) (Microsoft Research)
+* [Dietrich Geisler](https://github.com/Checkmate50) ([SOAR Lab](http://soarlab.org), University of Utah)
+* [Arvind Haran](http://www.cs.utah.edu/~haran) ([SOAR Lab](http://soarlab.org), University of Utah)
+* [Shaobo He](http://www.cs.utah.edu/~shaobo) ([SOAR Lab](http://soarlab.org), University of Utah)
+* [Jiten Thakkar](http://jiten-thakkar.com) ([SOAR Lab](http://soarlab.org), University of Utah)
 * [Jonathan Whitaker](https://www.linkedin.com/in/jonathan-whitaker-5a8b2484) ([SOAR Lab](http://soarlab.org/), University of Utah)
 
diff --git a/include/smack/Naming.h b/include/smack/Naming.h
@@ -28,6 +28,7 @@ class Naming {
   static const std::string UNINTERPRETED_FLOAT_TYPE;
   static const std::string FLOAT_TYPE;
   static const std::string DOUBLE_TYPE;
+  static const std::string LONG_DOUBLE_TYPE;
   static const std::string PTR_TYPE;
   static const std::string NULL_VAL;
 

diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp
@@ -15,6 +15,7 @@ const std::string Naming::BOOL_TYPE = "bool";
 const std::string Naming::UNINTERPRETED_FLOAT_TYPE = "float";
 const std::string Naming::FLOAT_TYPE = "bvfloat";
 const std::string Naming::DOUBLE_TYPE = "bvdouble";
+const std::string Naming::LONG_DOUBLE_TYPE = "bvlongdouble";
 const std::string Naming::PTR_TYPE = "ref";
 const std::string Naming::NULL_VAL = "$0.ref";
 

diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
@@ -201,6 +201,8 @@ std::string SmackRep::type(const llvm::Type* t) {
       return Naming::FLOAT_TYPE;
     else if (t->isDoubleTy())
       return Naming::DOUBLE_TYPE;
+    else if (t->isX86_FP80Ty())
+      return Naming::LONG_DOUBLE_TYPE;
     else
       llvm_unreachable("Unsupported floating-point type.");
   }
@@ -950,6 +952,7 @@ std::string SmackRep::getPrelude() {
   if (SmackOptions::FloatEnabled) {
     s << Decl::typee(Naming::FLOAT_TYPE, "float24e8") << "\n";
     s << Decl::typee(Naming::DOUBLE_TYPE, "float53e11") << "\n";
+    s << Decl::typee(Naming::LONG_DOUBLE_TYPE, "float65e15") << "\n";
   }
   s << Decl::typee(Naming::UNINTERPRETED_FLOAT_TYPE, intType(32)) << "\n";
   s << "\n";

diff --git a/share/smack/include/smack.h b/share/smack/include/smack.h
@@ -196,6 +196,20 @@ int signbit(double x);
 int __fpclassify(double x);
 int fpclassify(double x);
 int __finite(double x);
+
+//long doubles
+/*int __isnormall(long double x);
+int __isSubnormall(long double x);
+int __iszerol(long double x);
+int __isinfl(long double x);
+int __isnanl(long double x);
+int __isnegativel(long double x);
+int __ispositivel(long double x);
+int __signbitl(long double x);
+int signbitl(long double x);
+int __fpclassifyl(long double x);
+int fpclassifyl(long double x);
+int __finitel(long double x);*/
 #endif
 
 #undef S1