Default precondition of external functions

[fpoli]

trafficstars

We discussed that external functions should have false as precondition, instead of true. The latter only makes sense if Prusti verifies all the dependencies, but this is not what cargo-prusti does.

[Aurel300]

At the very least this depends on having a solid library of stdlib specifications. Otherwise this kind of thing would quickly make any code unusable without a huge chunk of boilerplate specs.

[vakaras]

At the very least this depends on having a solid library of stdlib specifications. Otherwise this kind of thing would quickly make any code unusable without a huge chunk of boilerplate specs.

I think this is true in any case.

[fpoli]

#1187 is done. When PRUSTI_OPT_IN_VERIFICATION is enabled, we can now use false as the default precondition.