Language: Frama-c

The -wp-rte option of the plugin Wp generates ACSL annotations asserting that the program does not contain runtime errors. In the case of filter it generates 3 such assertions. Two are related to accesses in the arrays t and mask, one is related to arithmetic overflow. Complete the file filter.c so that when issuing the command: frama-c-gui -wp -wp-rte filter.c all the RTE assertions are proved correct. Using the command-line version of Frama-C with the following command:frama-c-gui -wp -wp-rte filter.c

#include "limits.h" /*@ assigns othing; */ int condition(int v); /* @ requires TO COMPLETE ; @ requires TO COMPLETE ; @ requires TO COMPLETE ;*/ void filter(int * t, char * mask, int size) { /*@ loop invariant 0 <= i <= size; @ loop assigns i, *(mask+(0..i)); */ for(int i=0; i