Customizable privacy bound

[SSoelvsten]

Currently we only support epsilon-private algorithms, but many algorithms, such as SmartSum in the presentation by Zhang and Kifer [ZK17], are c · epsilon-private for some positive constant c = 1. We suggest to add a new annotation that describes the privacy guarantee, which is then used to generate the assertions before all return statements. The SmartSum of [ZK17] would then have the added annotation

privacy: 2 * epsilon

If no such annotation has been provided, then epsilon is the default used.