Adding test case that fails if contracts can initiate transactions.#255

Open

stephensj2 wants to merge 52 commits intomicrosoft:masterfrom

utopia-group:master

Commits on Apr 15, 2020

Adding regression for case where harness can call otherwise unreachable code. Also guarding code that only allows non-contracts to initiate transactions with a flag that is on by default

stephensj2
authored and
stephensj2
committed

Commits on Apr 17, 2020

Merge branch 'master' of https://github.com/microsoft/verisol

stephensj2
authored and
stephensj2
committed

Commits on Apr 22, 2020

Adding in simple syntactic alias check

stephensj2
authored and
stephensj2
committed
Adding tip for translating from solidity to boogie in global declarations

stephensj2
authored and
stephensj2
committed

Commits on Apr 24, 2020

Adding map splitting for the alias analysis. Also fixed a bug in the analysis

stephensj2
authored and
stephensj2
committed
Adding sum splitting

stephensj2
authored and
stephensj2
committed

Commits on Apr 27, 2020

A transaction is rejected if a value is provided to a non-payable function. Adding an assumption that msgvalue is 0 for all non-payable functions.

stephensj2
authored and
stephensj2
committed
Essentially adding a deployer mode. It will call all of the public functions of contract variables in addition to the contract's public functions

stephensj2
authored and
stephensj2
committed

Commits on May 4, 2020

Adding a fix to a small bug in lazyAlloc scheme

stephensj2
authored and
stephensj2
committed

Commits on May 14, 2020

Adding a smtDefined to ConstantToRef so that it acts as the identity function. Adding a flag to model non-linear arithmetic as an uninterpreted function. Adding preliminary support for super. Funct…

stephensj2
authored and
stephensj2
committed
Forgot to add attribute to ConstantToRef

stephensj2
authored and
stephensj2
committed
Adding fix to ConstToRef

stephensj2
authored and
stephensj2
committed
Adding power function to non-linear modeling

stephensj2
authored and
stephensj2
committed
Fixing a bug with super arguments

stephensj2
authored and
stephensj2
committed

Commits on May 22, 2020

Updating gas instrumentation for fallback. It was possible to enter an infinite loop where you had run out of gas but it was never checked. We not guard against that. Also adding an explicit revert…

stephensj2
authored and
stephensj2
committed
Adding ability to support modular arithmetic with modulus. Only supporting uints right now.

stephensj2
authored and
stephensj2
committed

Commits on May 25, 2020

Adding the adversarial model

stephensj2
authored and
stephensj2
committed
Adding non-linear mod

stephensj2
authored and
stephensj2
committed
Treat block.number as now (temporarily).
kferles
committed
Merge branch 'master' of github.com:utopia-group/verisol
kferles
committed

Commits on May 27, 2020

Adding constraints to variables so they are within the range of their type if modularArithmetic flag is on. Fixed bug with casting down in Modular arithmetic and found bug in VeriSol where it will …

stephensj2
authored and
stephensj2
committed
Merge branch 'master' of https://github.com/utopia-group/verisol

stephensj2
authored and
stephensj2
committed
Fixing callback and multipleCallbacks fallback function. For callback, we should check the type of the contract we are making the call to, otherwise we we have a lot of repetition and can make ille…

stephensj2
authored and
stephensj2
committed

Commits on Aug 31, 2020

Adding a lazy allocation scheme that doesn't modify the memory structures on an access. It passes all regressions as long as ERC20 recursionDepth=4. I also think it may need a bit more work on nest…

stephensj2
authored and
stephensj2
committed

Commits on Sep 7, 2020

Adding a mode to model arrays/mappings as multi-dimension boogie maps rather than a split map if not aliased. All regressions pass in this mode, but there is still some work that needs to be done f…

stephensj2
authored and
stephensj2
committed

Commits on Sep 15, 2020

Adding a Pre/Post mode for SmartPulse

stephensj2
authored and
stephensj2
committed
Adding the script I use to reset the installation

stephensj2
authored and
stephensj2
committed

Commits on Sep 18, 2020

Adding an argument to generate getters for public variables

stephensj2
authored and
stephensj2
committed

Commits on Sep 24, 2020

Adding mode to generate ERC20 specifications

stephensj2
authored and
stephensj2
committed

Commits on Sep 25, 2020

Making minor modifications to the spec generation

stephensj2
authored and
stephensj2
committed

Commits on Sep 28, 2020

Fixing bugs

stephensj2
authored and
stephensj2
committed

Commits on Oct 2, 2020

Fixing bugs. Adding new method to model inline assembly that havoc's all written variables

stephensj2
authored and
stephensj2
committed

Commits on Oct 7, 2020

Changing VeriSol so it will not fail if multiple functions named same thing

stephensj2
authored and
stephensj2
committed

Commits on Oct 8, 2020

Adding ability to have variable declarations inside tuples

stephensj2
authored and
stephensj2
committed
Adding the ability to leave entries out of tuple in an assignment. i.e. (bool success, ) = call()

stephensj2
authored and
stephensj2
committed

Commits on Oct 9, 2020

Added ability to define using for with contracts

stephensj2
authored and
stephensj2
committed

Commits on Oct 13, 2020

Fixing a bug caused by now.div()

stephensj2
authored and
stephensj2
committed

Commits on Oct 23, 2020

Adding variable positions to config file and adding support for gasleft call

stephensj2
authored and
stephensj2
committed
Changing evmVersion

stephensj2
authored and
stephensj2
committed
Adding this. from generated specifications

stephensj2
authored and
stephensj2
committed

Commits on Oct 29, 2020

Fixing something in spec generator
Jon Stephens
committed

Commits on Nov 6, 2020

Fixing a bug in the spec generator

stephensj2
authored and
stephensj2
committed

Commits on Nov 10, 2020

Fixing a few issues with the specification generation. Constants should not be included in vars and vars should be in inheritance order.

stephensj2
authored and
stephensj2
committed

Commits on Nov 11, 2020

Fixing a bug where constructor msg.value can be negative

stephensj2
authored and
stephensj2
committed

Commits on Nov 12, 2020

Adding error for unsupported abi functions

stephensj2
authored and
stephensj2
committed
Fixing bug where zero function isn't declared

stephensj2
authored and
stephensj2
committed
Fixing a bug when determining if a public getter

stephensj2
authored and
stephensj2
committed
Fixing a bug with public getters. Essentially verisol didn't support public getters for mappings/arrays as it didn't take arguments into account. Have a workaround but only if generating the getters

stephensj2
authored and
stephensj2
committed

Commits on Dec 11, 2020

Fixing an issue with payable functions

stephensj2
authored and
stephensj2
committed

Commits on Jun 1, 2021

Commits on Jun 8, 2021

Create resetInstallwsl.sh
stephensj2
authored