Getting Started
Installation Guide
Tutorial
Issue Tracker
Tools
Verifier
Alpinist
VeSUV
VeyMont
Showcases
Publications
About
VerCors Team
News
Contact
Credits
License
Backward dependencies (error 1)
Verification example with backward loop dependencies that does not verify.
General Information
Backend
: Silicon
Language
: C / OpenMP / OpenCL
Features
: Iteration contracts, Arrays, Loop parallelisations
Path to Example File
: arrays/backward-dep-e1.c
Should Verify
: No
Date
: 2017-06-15
Lines of Code
: 35 (comments not included)
Lines of Specification
: 17 (48.6% of total)
Computation Time
: 14.7 seconds
// -*- tab-width:2 ; indent-tabs-mode:nil -*- //:: cases backward-dep-err1 //:: tools silicon //:: verdict Fail /*@ context \pointer(a, len, write); context \pointer(b, len, 1\2); context \pointer(c, len, write); @*/ void example(int a[],int b[],int c[],int len){ for(int i=0;i < len;i++) /*@ requires a != NULL; requires b != NULL; requires c != NULL; requires Perm(a[i],1\2); requires i==0 ==> Perm(a[i],1\2); requires i < len-1 ==> Perm(a[i+1],1\2); requires Perm(b[i],1\2); requires Perm(c[i],write); ensures Perm(a[i],write); ensures Perm(b[i],1\2); ensures Perm(c[i],write); @*/ { a[i]=b[i]+1; /*@ ghost S1:if (i>0) { recv a!=NULL ** Perm(a[i],1\2) from S2,1; } @*/ S2:if (i < len-1) { c[i]=a[i+1]+2; //@ send a!=NULL ** Perm(a[i+1],1\2) to S1,1; } } }
Language:
PVL
Java
Cuda
C / OpenMP / OpenCL
Viper