force disarm

[newcodepusher]

With this contract have trouble. Command scribble --arm -m files Test.sol working, but command scribble --disarm -m files Test.sol doesn't.

pragma solidity ^0.6.0;

contract Test {

    /// if_succeeds {:msg "wrong byte"} checkBytes(_bytes) == result;
    function process(bytes calldata _bytes) external returns (bool result) {
        return this.checkBytes(_bytes);
    }

    function checkBytes(bytes calldata _bytes) pure external returns (bool result) {
        return _bytes.length > 0;
    }
}

log:

$ scribble --arm -m files Test.sol
Test.sol -> Test.sol.instrumented
Copying Test.sol to Test.sol.original
Copying Test.sol.instrumented to Test.sol

$ scribble --disarm -m files Test.sol
Compile errors encountered for Test.sol:
SolcJS 0.6.12:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.11:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.10:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.9:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.8:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.7:
Test.sol:8:15: DeclarationError: Undeclared identifier. "checkBytes" is not (or not yet) visible at this point.
        if (!(checkBytes(_bytes) == result)) {
              ^--------^

SolcJS 0.6.6:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.5:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.4:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.3:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.2:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.1:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

SolcJS 0.6.0:
Test.sol:14:37: TypeError: Data location must be "storage" or "memory" for parameter in function, but "calldata" was given.
    function _original_Test_process(bytes calldata _bytes) private returns (bool result) {
                                    ^-------------------^

[newcodepusher]

If I change
/// if_succeeds {:msg "wrong byte"} checkBytes(_bytes) == result;
to
/// if_succeeds {:msg "wrong byte"} this.checkBytes(_bytes) == result;
disarm starting working, but for fix this I must manualy restore contract

[cd1m0]

Thank you for reporting this! Will investigate and root cause