SMTChecker: Some (uncommon) valid values for selecting contracts are rejected as invalid

Open blishko opened this issue 10 months ago • 1 comments

Model checker's CLI option to select contracts to be analyzed (--model-checker-contracts) rejects some valid values, for example if the path contains :.

Mar 15 '25 22:03 blishko

Full context: https://github.com/ethereum/solidity/pull/15880#discussion_r1994368591

BTW, note that an empty source name is actually something that can happen. You can't do this on the CLI, but in Standard JSON source names can be arbitrary strings, including empty ones. There are some quirks around their behavior (#15747) and I think we'd be better off disallowing them, but for the time being they're technically valid.

And they can contain : and , even on the CLI (as long as the file system allows this). Only contract names are guaranteed to be identifiers.

Mar 16 '25 15:03 cameel