Brian Johannesmeyer

Dynamic array lengths

3

Is it possible to verify a function with a variable length array input? All of the examples use constant lengths for `__SMACK_values`. For example, in the following code there is...

Is there a way to specify when a value should be declassified?

3

As an example, suppose we want to verify `xor` in `xor.c`: ``` #include #include "../ct-verif.h" void xor(int *key, int *out) { // key is secret, out is public *out =...