Skip to content
Snippets Groups Projects
Commit fb7ababa authored by Cécile Ruet-Cros's avatar Cécile Ruet-Cros Committed by Loïc Correnson
Browse files

[wp] remove memRegion testing

parent 87d3a559
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 574 deletions
src/plugins/wp/tests/wp_region/README.md deleted 100644 → 0
+ 0
− 13
View file @ 87d3a559
# Testing WP/Region
Use `./fc.sh -h|--help` to visualize the output before commiting changes.
# Recommanded workflow
With default configuration, put a single 'job' function in each test file.
Then:
1. Run `./fc.sh test.i -r` to visualize the region graph and check the proofs
2. Run `./fc.sh test.i -u` to update the region-graph oracle (creates also the oracle directories)
3. Run `./fc.sh test.i -t` to check test is OK (eventually use `-t -show` or `-t -update`)
4. Run `./fc.sh test.i -q` to check qualif test is OK
src/plugins/wp/tests/wp_region/annot.i deleted 100644 → 0
+ 0
− 66
View file @ 87d3a559
/* run.config
PLUGIN: wp
OPT: -region-annot -print -generated-spec-mode skip
EXECNOW: BIN ocode_@PTEST_NAME@_1.i @frama-c@ %{dep:@PTEST_DIR@/@PTEST_NAME@.i} -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i > @DEV_NULL@ 2> @DEV_NULL@
EXECNOW: BIN ocode_@PTEST_NAME@_2.i @frama-c@ %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_1.i} -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_2.i > @DEV_NULL@ 2> @DEV_NULL@
EXECNOW: LOG diff_@PTEST_NAME@.txt diff %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_1.i} %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_2.i} &> @PTEST_RESULT@/diff_@PTEST_NAME@.txt
COMMENT: The file diff_@PTEST_NAME@.txt must be empty.
COMMENT: So, that file has not to be present into the oracle directory since absent files are considered such as empty files.
*/
/* run.config_qualif
DONTRUN:
*/
// This test only checks that annotation are correctly parsed & printed
typedef struct N { double v ; int s ; } *SN ;
typedef struct L { int v ; int s ; } *SL ;
typedef struct Block {
SN prm ;
SN inp1 ;
SN inp2 ;
SN inp3 ;
SN out1 ;
SN out2 ;
SN out3 ;
SL idx1 ;
SL idx2 ;
SL idx3 ;
SN sum ;
} FB ;
//@ \wp::wpregion *fb ;
void fb_ADD(FB *fb)
{
fb->out1->v = fb->out1->v + fb->out2->v ;
fb->out1->s = fb->out1->s | fb->out2->s ;
}
/*@
\wp::wpregion IN: (fb->inp1 .. fb->inp3), \pattern{PMEM} ;
\wp::wpregion OUT: (fb->out1 .. fb->out3), \pattern{PVECTOR} ;
\wp::wpregion IDX: (fb->idx1 .. fb->idx3), \pattern{PVECTOR} ;
*/
void fb_SORT(FB *fb)
{
SN *inp = &(fb->inp1) ;
SN *out = &(fb->out1) ;
SL *idx = &(fb->idx1) ;
for (int i = 0; i < 3; i++) {
out[i]->v = inp[i]->v + fb->prm->v ;
out[i]->s = 0 ;
idx[i]->v = inp[i]->s ;
idx[i]->s = 0 ;
}
fb->sum->v =
fb->out1->v +
fb->out2->v +
fb->out3->v ;
fb->sum->s = 0 ;
}
src/plugins/wp/tests/wp_region/annot/a.i deleted 100644 → 0
+ 0
− 58
View file @ 87d3a559
/* Generated by Frama-C */
struct N {
double v ;
int s ;
};
typedef struct N *SN;
struct L {
int v ;
int s ;
};
typedef struct L *SL;
struct Block {
SN prm ;
SN inp1 ;
SN inp2 ;
SN inp3 ;
SN out1 ;
SN out2 ;
SN out3 ;
SL idx1 ;
SL idx2 ;
SL idx3 ;
SN sum ;
};
typedef struct Block FB;
/*@ terminates \true;
\wp::wpregion *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
(fb->out1)->s |= (fb->out2)->s;
return;
}
/*@ terminates \true;
\wp::wpregion IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
\wp::wpregion OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
\wp::wpregion IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
*/
void fb_SORT(FB *fb)
{
SN *inp = & fb->inp1;
SN *out = & fb->out1;
SL *idx = & fb->idx1;
{
int i = 0;
while (i < 3) {
(*(out + i))->v = (*(inp + i))->v + (fb->prm)->v;
(*(out + i))->s = 0;
(*(idx + i))->v = (*(inp + i))->s;
(*(idx + i))->s = 0;
i ++;
}
}
(fb->sum)->v = ((fb->out1)->v + (fb->out2)->v) + (fb->out3)->v;
(fb->sum)->s = 0;
return;
}
src/plugins/wp/tests/wp_region/annot/b.i deleted 100644 → 0
+ 0
− 58
View file @ 87d3a559
/* Generated by Frama-C */
struct N {
double v ;
int s ;
};
typedef struct N *SN;
struct L {
int v ;
int s ;
};
typedef struct L *SL;
struct Block {
SN prm ;
SN inp1 ;
SN inp2 ;
SN inp3 ;
SN out1 ;
SN out2 ;
SN out3 ;
SL idx1 ;
SL idx2 ;
SL idx3 ;
SN sum ;
};
typedef struct Block FB;
/*@ terminates \true;
\wp::wpregion *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
(fb->out1)->s |= (fb->out2)->s;
return;
}
/*@ terminates \true;
\wp::wpregion IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
\wp::wpregion OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
\wp::wpregion IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
*/
void fb_SORT(FB *fb)
{
SN *inp = & fb->inp1;
SN *out = & fb->out1;
SL *idx = & fb->idx1;
{
int i = 0;
while (i < 3) {
(*(out + i))->v = (*(inp + i))->v + (fb->prm)->v;
(*(out + i))->s = 0;
(*(idx + i))->v = (*(inp + i))->s;
(*(idx + i))->s = 0;
i ++;
}
}
(fb->sum)->v = ((fb->out1)->v + (fb->out2)->v) + (fb->out3)->v;
(fb->sum)->s = 0;
return;
}
src/plugins/wp/tests/wp_region/array1.i deleted 100644 → 0
+ 0
− 8
View file @ 87d3a559
//@ \wp::wpregion *p, *q ;
int job( int n, int * p , int * q )
{
int s = 0 ;
for (int k = 0; k < n; k++)
s += p[k] * q[k] ;
return s ;
}
src/plugins/wp/tests/wp_region/array2.i deleted 100644 → 0
+ 0
− 8
View file @ 87d3a559
//@ \wp::wpregion *p; \wp::wpregion *q ;
int job( int n, int * p , int * q )
{
int s = 0 ;
for (int k = 0; k < n; k++)
s += p[k] * q[k] ;
return s ;
}
src/plugins/wp/tests/wp_region/array3.i deleted 100644 → 0
+ 0
− 6
View file @ 87d3a559
int job( int * p )
{
int s = 0 ;
while (!*p) { s+=*p ; p++; }
return s;
}
src/plugins/wp/tests/wp_region/array4.i deleted 100644 → 0
+ 0
− 7
View file @ 87d3a559
int job( int * p )
{
int s = 0 ;
int *q = p ;
while (!*q) { s+=*q ; q++; }
return s;
}
src/plugins/wp/tests/wp_region/array5.i deleted 100644 → 0
+ 0
− 7
View file @ 87d3a559
int job( int * p , int * q )
{
int s = 0 ;
q = p ;
while (!*q) { s+=*p ; p[s]; q++; }
return s;
}
src/plugins/wp/tests/wp_region/array6.i deleted 100644 → 0
+ 0
− 9
View file @ 87d3a559
int A[10] ;
int B[20] ;
int job(int k)
{
int s = 0 ;
while (!A[k]) { s += A[k]; k++; }
return s ;
}
src/plugins/wp/tests/wp_region/array7.i deleted 100644 → 0
+ 0
− 10
View file @ 87d3a559
int A[10] ;
int B[20] ;
int job(int k)
{
int s = 0 ;
int * p = A+k ;
while (!*p) { s += *p; p++; }
return s ;
}
src/plugins/wp/tests/wp_region/array8.i deleted 100644 → 0
+ 0
− 10
View file @ 87d3a559
int A[10] ;
int B[20] ;
int job(int c,int k)
{
int s = 0 ;
int * p = (c?A:B)+k ;
while (!*p) { s += *p; p++; }
return s ;
}
src/plugins/wp/tests/wp_region/fb_ADD.i deleted 100644 → 0
+ 0
− 25
View file @ 87d3a559
typedef struct N { double v ; int s ; } *SN ;
typedef struct L { int v ; int s ; } *SL ;
typedef struct Block {
SN prm ;
SN inp1 ;
SN inp2 ;
SN inp3 ;
SN out1 ;
SN out2 ;
SN out3 ;
SL idx1 ;
SL idx2 ;
SL idx3 ;
SN sum ;
} FB ;
/*@
\wp::wpregion A: fb ;
*/
void job(FB *fb)
{
fb->out1->v = fb->out1->v + fb->out2->v ;
fb->out1->s = fb->out1->s | fb->out2->s ;
}
src/plugins/wp/tests/wp_region/fb_SORT.i deleted 100644 → 0
+ 0
− 44
View file @ 87d3a559
typedef struct N { double v ; int s ; } *SN ;
typedef struct L { int v ; int s ; } *SL ;
typedef struct Block {
SN prm ;
SN inp1 ;
SN inp2 ;
SN inp3 ;
SN out1 ;
SN out2 ;
SN out3 ;
SL idx1 ;
SL idx2 ;
SL idx3 ;
SN sum ;
} FB ;
/*@
\wp::wpregion Shared: *(fb->inp1 .. fb->inp3);
\wp::wpregion IN: (fb->inp1 .. fb->inp3);
\wp::wpregion OUT: (fb->out1 .. fb->out3);
\wp::wpregion IDX: (fb->idx1 .. fb->idx3);
*/
void job(FB *fb)
{
SN *inp = &(fb->inp1) ;
SN *out = &(fb->out1) ;
SL *idx = &(fb->idx1) ;
for (int i = 0; i < 3; i++) {
out[i]->v = inp[i]->v + fb->prm->v ;
out[i]->s = 0 ;
idx[i]->v = inp[i]->s ;
idx[i]->s = 0 ;
}
fb->sum->v =
fb->out1->v +
fb->out2->v +
fb->out3->v ;
fb->sum->s = 0 ;
}
src/plugins/wp/tests/wp_region/fc.sh deleted 100755 → 0
+ 0
− 109
View file @ 87d3a559
# Visualize output of WP/Region tests
OPT=
CMD=fc
TEST="<none>"
NAME="none"
OPEN="none"
DEFAULT="-wp-msg-key dot,chunk,roots,garbled"
if type open &> /dev/null ; then
OPEN=open
elif type xpdf &> /dev/null ; then
OPEN=xpdf
elif type evince &> /dev/null ; then
OPEN=evince
fi
while [ "$1" != "" ];
do
case $1 in
"-h"|"--help")
echo "fc.sh [options...] <test.[ic]>" ;
echo " -h,--help help and exit" ;
echo " -D,--delete clean output directory and exit" ;
echo " -g,--gui run in Frama-C Gui" ;
echo " -r,--region visualize region graph" ;
echo " -u,--update commit region graph in oracle" ;
echo " -t,--test run ptests.opt on test file (or all files)" ;
echo " -q,--qualif run ptests.opt with test-config qualif" ;
echo " --open <cmd> opens pdf with '<cmd>'" ;
echo " -k <keys> set message keys" ;
echo " * any other Frama-C options" ;
exit 0 ;
;;
*.i) TEST=${1}; NAME=${TEST/.i/} ;;
*.c) TEST=${1}; NAME=${TEST/.c/} ;;
"-D"|"--delete") CMD=delete ;;
"-u"|"--update") CMD=update ;;
"-t"|"--test") CMD=test ;;
"-q"|"--qualif") CMD=qualif ;;
"-g"|"--gui") CMD=gui ;;
"-r"|"--region") CMD=region ; OPT="${OPT} -wp-msg-key pdf" ;;
"--open") shift ; CMD=region ; OPEN=${1} ;;
"-k") shift ; CMD=region ; DEFAULT="" ; OPT="${OPT} -wp-msg-key $1" ;;
*)
OPT="${OPT} $1"
;;
esac
shift
done
BIN=../../../../../bin
WP="-wp-region -wp-model Region -wp-fct job -wp-out result/${NAME}"
case $CMD in
"fc"|"region")
echo "Running frama-c $TEST"
$BIN/frama-c $WP $TEST $DEFAULT $OPT
PDF="./result/${NAME}/region/job.pdf"
if [ $CMD = region ] && [ -f $PDF ]
then
if [ $OPEN != none ] ; then
echo "Source File:"
cat $TEST
$OPEN $PDF
else
echo "No command found for opening $PDF"
echo "Use --open <cmd> option"
fi
fi
;;
"gui")
echo "Running frama-c $TEST (Gui)"
$BIN/frama-c-gui $WP $TEST $OPT
;;
"test")
if [ $TEST == "<none>" ]
then
echo "Testing directory..."
( cd ../.. ; ../../../bin/ptests.opt tests/wp_region > /dev/null )
for test in *.i
do
name=${test/.i/}
oracle=oracle/$name/region/job.dot
result=result/$name/region/job.dot
if [ -f $oracle ] && !( diff -q $oracle $result > /dev/null )
then
echo "Diff: ./fc.sh $test -r"
fi
done
else
echo "Testing $TEST$OPT"
( cd ../.. ; ../../../bin/ptests.opt tests/wp_region/$TEST $OPT )
fi
;;
"qualif")
echo "Testing $TEST -config qualif$OPT"
( cd ../.. ; ../../../bin/ptests.opt tests/wp_region/$TEST -config qualif $OPT )
;;
"update")
echo "Update './oracle/$NAME/region/job.dot"
mkdir -p ./oracle/$NAME/region
cp -f ./result/$NAME/region/job.dot ./oracle/$NAME/region/
;;
"delete")
echo "Cleaning './result/$NAME'"
rm -fr result/$NAME/*
;;
esac
src/plugins/wp/tests/wp_region/garbled.i deleted 100644 → 0
+ 0
− 6
View file @ 87d3a559
float job(int *p,int *q)
{
return *q + *(float*)p + *p ;
}
src/plugins/wp/tests/wp_region/index.i deleted 100644 → 0
+ 0
− 6
View file @ 87d3a559
int A[3][4][5] ;
int job(int i,int j,int k)
{
return A[i][j][k];
}
src/plugins/wp/tests/wp_region/matrix.i deleted 100644 → 0
+ 0
− 8
View file @ 87d3a559
void job( int cols , int rows , int ** m , int * v , int * r )
{
for (int i = 0; i < rows; i++) {
r[i] = 0 ;
for (int j = 0; j < cols; j++)
r[i] += m[i][j] * v[j] ;
}
}
src/plugins/wp/tests/wp_region/oracle/annot.res.oracle deleted 100644 → 0
+ 0
− 59
View file @ 87d3a559
[kernel] Parsing annot.i (no preprocessing)
/* Generated by Frama-C */
struct N {
double v ;
int s ;
};
typedef struct N *SN;
struct L {
int v ;
int s ;
};
typedef struct L *SL;
struct Block {
SN prm ;
SN inp1 ;
SN inp2 ;
SN inp3 ;
SN out1 ;
SN out2 ;
SN out3 ;
SL idx1 ;
SL idx2 ;
SL idx3 ;
SN sum ;
};
typedef struct Block FB;
/*@ \wp::wpregion *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
(fb->out1)->s |= (fb->out2)->s;
return;
}
/*@ \wp::wpregion IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
\wp::wpregion OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
\wp::wpregion IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
*/
void fb_SORT(FB *fb)
{
SN *inp = & fb->inp1;
SN *out = & fb->out1;
SL *idx = & fb->idx1;
{
int i = 0;
while (i < 3) {
(*(out + i))->v = (*(inp + i))->v + (fb->prm)->v;
(*(out + i))->s = 0;
(*(idx + i))->v = (*(inp + i))->s;
(*(idx + i))->s = 0;
i ++;
}
}
(fb->sum)->v = ((fb->out1)->v + (fb->out2)->v) + (fb->out3)->v;
(fb->sum)->s = 0;
return;
}
src/plugins/wp/tests/wp_region/oracle/array1.0.dot deleted 100644 → 0
+ 0
− 57
View file @ 87d3a559
digraph "job" {
rankdir="LR" ;
node [ fontname="monospace" ];
edge [ fontname="monospace" ];
V000 [ label="n", shape="cds", style="filled", fillcolor="yellow" ];
V000:e -> A000 ;
V001 [ label="p", shape="cds", style="filled", fillcolor="yellow" ];
V001:e -> A001 ;
V002 [ label="q", shape="cds", style="filled", fillcolor="yellow" ];
V002:e -> A002 ;
V003 [ label="s", shape="cds", style="filled", fillcolor="yellow" ];
V003:e -> A003 ;
V004 [ label="k", shape="cds", style="filled", fillcolor="yellow" ];
V004:e -> A004 ;
A000 [ label="R", shape="oval", fillcolor="green", style="filled" ];
_005 [ label="roots:&n", style="filled", color="lightblue", shape="box" ];
{ rank=same; A000; _005; }
_005 -> A000 [ arrowhead="tee" ];
_006 [ shape="record", label="Var sint32" ];
A000 -> _006:w [ arrowhead="tee" ];
A001 [ label="D", shape="oval" ];
_007 [ label="roots:&p", style="filled", color="lightblue", shape="box" ];
{ rank=same; A001; _007; }
_007 -> A001 [ arrowhead="tee" ];
_008 [ shape="record", label="<_p1> Ref" ];
_008:_p1 -> A005:w [ taillabel="[..]", labeldistance="1.7",
labelangle="+40", color="red"
];
A001 -> _008:w [ arrowhead="tee" ];
A002 [ label="D", shape="oval" ];
_009 [ label="roots:&q", style="filled", color="lightblue", shape="box" ];
{ rank=same; A002; _009; }
_009 -> A002 [ arrowhead="tee" ];
_010 [ shape="record", label="<_p1> Ref" ];
_010:_p1 -> A005:w [ taillabel="[..]", labeldistance="1.7",
labelangle="+40", color="red"
];
A002 -> _010:w [ arrowhead="tee" ];
A003 [ label="RW", shape="oval", fillcolor="green", style="filled" ];
_011 [ shape="record", label="Var sint32" ];
A003 -> _011:w [ arrowhead="tee" ];
A004 [ label="RW", shape="oval", fillcolor="green", style="filled" ];
_012 [ shape="record", label="Var sint32" ];
A004 -> _012:w [ arrowhead="tee" ];
A005 [ label="R[]&", shape="oval", fillcolor="orange", style="filled" ];
_013 [ label="roots:*", style="filled", color="lightblue", shape="box" ];
{ rank=same; A005; _013; }
_013 -> A005 [ arrowhead="tee" ];
_014 [ shape="record", label="Mem sint32" ];
A005 -> _014:w [ arrowhead="tee" ];
R015 [ label="\\result", shape="tab", style="filled", fillcolor="yellow" ];
{ rank=same; R015; A006; }
R015 -> A006 ;
A006 [ label="W", shape="oval", fillcolor="green", style="filled" ];
_016 [ shape="record", label="Var sint32" ];
A006 -> _016:w [ arrowhead="tee" ];
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment