Skip to content

Instantly share code, notes, and snippets.

@yosriady
Created Feb 9, 2022
Embed
What would you like to do?
Sample contracts you can test Echidna with
contract Ownable {
address owner;
constructor() {
owner = msg.sender;
}
modifier onlyOwner() {
require(owner == msg.sender);
_;
}
function renounceOwnership() onlyOwner public {
delete owner;
}
}
contract Pausable is Ownable {
bool isPaused;
modifier ifNotPaused(){
require(!isPaused);
_;
}
modifier ifPaused(){
require(isPaused);
_;
}
function pause() onlyOwner public {
isPaused = true;
}
function unpause() ifPaused public {
isPaused = false;
}
}
// Test the scenario of decomissioning a contract
contract EchidnaTest is Pausable {
constructor() {
pause(); // final pause
owner = address(0); // renounce ownership
}
// define invariant
function echidna_CheckPauseIsFinal() public view returns(bool){
return isPaused == true;
}
}
pragma solidity ^0.7.6;
contract Token {
mapping(address => uint) public balances;
function transfer(address to, uint value) public {
balances[msg.sender] -= value;
balances[to] += value;
}
}
contract EchidnaTest is Token {
address echidna_caller = 0x00a329C0648769a73afAC7F9381e08fb43DBEA70;
constructor() {
balances[echidna_caller] = 10000;
}
// add the property
function echidna_test_balance() view public returns(bool){
return balances[echidna_caller] <= 10000;
}
}
@yosriady
Copy link
Author

yosriady commented Feb 9, 2022

echidna-test pausable.sol --contract EchidnaTest

echidna-test token.sol --contract EchidnaTest

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment