Invariants on types

Sep 13, 2015 at 12:35 AM
Edited Sep 13, 2015 at 12:42 AM
Hello everyone,

Am I wrong to think that code should not pass ? Invariant on set.len has been defined as set.len<10 but vcc verify set.len=15 correctly. (Code from documentation)
#include <vcc.h>

#define SIZE 10

typedef struct Set {
  unsigned int len;
  int data[SIZE];
  
  _(invariant len < SIZE)
  _(invariant \forall unsigned int i, j; i < j && j < len ==> data[i] < data[j])
} Set;

int main() {
  Set set;
  set.len = 15;
}
Thanks for help !
Marked as answer by Sl0th on 9/14/2015 at 6:28 AM
Sep 14, 2015 at 1:28 PM
Hello,

I found why, I misunderstood the tool.

Thanks
Marked as answer by Sl0th on 9/14/2015 at 6:28 AM