Description
After #15026 there remain two sources of random tabs in the sources we store in the repo:
- SMTChecker includes indentation in its source locations so it's also included in code snippets.
- Jump labels in
--asmoutput are prepended with a tab.
I think either of those is unnecessary and removing them would make automatic style checks simpler (less files to exclude). Not only for us but for anyone storing this output in their repository.
Still, this is more of an annoyance than a real issue so I don't expect that we'll work on it any time soon. I'm submitting an issue more to document what I discovered while addressing #15026 than to get someone to actually work on it.
Tabs in SMTChecker output
This happens only if the input file is indented
test.sol
// SPDX-License-Identifier: GPL-3.0
pragma solidity *;
contract C {
function f() public {
assert ( false ) ;
}
}Note that the assert line has leading and trailing tabs.
solc test.sol --model-checker-engine allWarning: Function state mutability can be restricted to pure
--> test.sol:5:5:
|
5 | function f() public {
| ^ (Relevant source part starts here and spans across multiple lines).
Warning: CHC: Assertion violation happens here.
Counterexample:
Transaction trace:
C.constructor()
C.f()
--> test.sol:6:3:
|
6 | assert ( false ) ;
| ^^^^^^^^^^^^^^^^^^^
Note that the assert line is included as is, including the leading and trailing indentation. The ^^^^^ marker repeats that indentation too.
Tab as separator in jump labels
solc test.sol --asm tag_3:
tag_4
tag_5
jump // in
tag_4:
stop
tag_5:
/* "test.sol":109:114 false */
0x00
/* "test.sol":97:116 assert ( false ) */
tag_7
jumpi
tag_8
tag_9
jump // in
Note that jump // in includes a tab character as a separator. It seems to be a deliberate decision made in #1330:
solidity/libevmasm/AssemblyItem.cpp
Lines 331 to 338 in b61c2a9
The PR does not have any justification for that decision though and it seems to me that using a space there would work just as well.