feat: full support for adding constraint to the issuing transactions

[yxliang01]

Description

Nowadays, we already have options like --attacker-address to add constraint to the transactions can be issued by laser. However, such support is not complete, e.g. can't specify constraint on the value of transactions. This feature would be very useful if we have some knowledge to direct the search to be more efficient.

[norhh]

At this moment you can use require to handle such cases, like require(msg.value<limit).

[yxliang01]

Thanks @norhh To reconfirm, require acts like adding preconditions to the symbolic exploration? What will mythril do if the require condition is provably false?

[norhh]

If any path violates the requirement, the path is terminated.