diff options
| -rw-r--r-- | libsolidity/formal/SymbolicVariables.cpp | 28 | ||||
| -rw-r--r-- | libsolidity/formal/SymbolicVariables.h | 29 | ||||
| -rwxr-xr-x | scripts/build.sh | 28 |
3 files changed, 69 insertions, 16 deletions
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index f7d2a119..997635af 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -99,3 +99,31 @@ SymbolicFixedBytesVariable::SymbolicFixedBytesVariable( SymbolicIntVariable(make_shared<IntegerType>(_numBytes * 8), _uniqueName, _interface) { } + +SymbolicFunctionVariable::SymbolicFunctionVariable( + TypePointer _type, + string const& _uniqueName, + smt::SolverInterface&_interface +): + SymbolicVariable(move(_type), _uniqueName, _interface), + m_declaration(m_interface.newVariable(currentName(), smtSort(*m_type))) +{ + solAssert(m_type->category() == Type::Category::Function, ""); +} + +void SymbolicFunctionVariable::resetDeclaration() +{ + m_declaration = m_interface.newVariable(currentName(), smtSort(*m_type)); +} + +smt::Expression SymbolicFunctionVariable::increaseIndex() +{ + ++(*m_ssa); + resetDeclaration(); + return currentValue(); +} + +smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _arguments) const +{ + return m_declaration(_arguments); +} diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index ef40944c..6754ee07 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -49,7 +49,11 @@ public: smt::Expression currentValue() const; std::string currentName() const; virtual smt::Expression valueAtIndex(int _index) const; - smt::Expression increaseIndex(); + virtual smt::Expression increaseIndex(); + virtual smt::Expression operator()(std::vector<smt::Expression> /*_arguments*/) const + { + solAssert(false, "Function application to non-function."); + } unsigned index() const { return m_ssa->index(); } unsigned& index() { return m_ssa->index(); } @@ -116,5 +120,28 @@ public: ); }; +/** + * Specialization of SymbolicVariable for FunctionType + */ +class SymbolicFunctionVariable: public SymbolicVariable +{ +public: + SymbolicFunctionVariable( + TypePointer _type, + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); + + smt::Expression increaseIndex(); + smt::Expression operator()(std::vector<smt::Expression> _arguments) const; + +private: + /// Creates a new function declaration. + void resetDeclaration(); + + /// Stores the current function declaration. + smt::Expression m_declaration; +}; + } } diff --git a/scripts/build.sh b/scripts/build.sh index bddbb97a..6edd60bd 100755 --- a/scripts/build.sh +++ b/scripts/build.sh @@ -1,28 +1,26 @@ #!/usr/bin/env bash +set -e -if [ -z "$1" ]; then +ROOTDIR="$(dirname "$0")/.." +BUILDDIR="${ROOTDIR}/build" + +if [[ $# -eq 0 ]]; then BUILD_TYPE=Release else BUILD_TYPE="$1" fi -cd $(dirname "$0")/.. && - if [[ "$(git tag --points-at HEAD 2>/dev/null)" == v* ]]; then - touch prerelease.txt + touch "${ROOTDIR}/prerelease.txt" fi -mkdir -p build && -cd build && -cmake .. -DCMAKE_BUILD_TYPE="$BUILD_TYPE" && -make -j2 +mkdir -p "${BUILDDIR}" +cd "${BUILDDIR}" -if [ $? -ne 0 ]; then - echo "Failed to build" - exit 1 -fi +cmake .. -DCMAKE_BUILD_TYPE="$BUILD_TYPE" "${@:2}" +make -j2 -if [ -z $CI ]; then - echo "Installing solc and soltest" - install solc/solc /usr/local/bin && install test/soltest /usr/local/bin +if [[ "${CI}" == "" ]]; then + echo "Installing ..." + sudo make install fi |