Project

General

Profile

Revision 3f823d04 test/test-compile.sh

View differences:

test/test-compile.sh
13 13
LUSTREC=lustrec
14 14
mkdir -p build
15 15
build=`pwd`"/build"
16
    
16

  
17 17

  
18 18
base_compile() {
19 19
    while IFS=, read -r file main opts
20 20
    do
21 21
	name=`basename "$file" .lus`
22
	dir=${SRC_PREFIX}/`dirname "$file"`
22
        ext=".lus"
23
	if [ `dirname "$file"`/"$name" = "$file" ]; then
24
	    name=`basename "$file" .lusi`
25
	    ext=".lusi"
26
	fi
27
        dir=${SRC_PREFIX}/`dirname "$file"`
23 28
	pushd $dir > /dev/null
24 29
    if [ "$main" != "" ]; then
25
	$LUSTREC -d $build -verbose 0 $opts -node $main "$name".lus;
30
	$LUSTREC -d $build -verbose 0 $opts -node $main "$name""$ext";
26 31
        if [ $? -ne 0 ]; then
27 32
            rlustrec1="INVALID";
28 33
        else
29 34
            rlustrec1="VALID"
30 35
	fi
31 36
	pushd $build > /dev/null
32
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
37
	if [ $ext = ".lus" ]; then
38
            gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
39
            if [ $? -ne 0 ]; then
40
		rgcc1="INVALID";
41
            else
42
		rgcc1="VALID"
43
	    fi
44
	else
45
	    rgcc1="NONE"
46
	fi
33 47
	popd > /dev/null
34
        if [ $? -ne 0 ]; then
35
            rgcc1="INVALID";
36
        else
37
            rgcc1="VALID"
38
	fi	
39 48
    else
40
	$LUSTREC -d $build -verbose 0 $opts "$name".lus;
49
	$LUSTREC -d $build -verbose 0 $opts "$name""$ext";
41 50
        if [ $? -ne 0 ]; then
42 51
            rlustrec1="INVALID";
43 52
        else
44 53
            rlustrec1="VALID"
45 54
        fi
46 55
	pushd $build > /dev/null
47
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
56
	if [ $ext = ".lus" ]; then
57
            gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
58
            if [ $? -ne 0 ]; then
59
		rgcc1="INVALID";
60
            else
61
		rgcc1="VALID"
62
            fi
63
	else
64
	    rgcc1="NONE"
65
	fi
48 66
	popd > /dev/null
49
        if [ $? -ne 0 ]; then
50
            rgcc1="INVALID";
51
        else
52
            rgcc1="VALID"
53
        fi
54 67
    fi
55 68
    popd > /dev/null
56 69
    if [ $verbose -gt 0 ]; then
57
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
70
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
58 71
    else
59
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
72
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
60 73
    fi;
61 74
    done < $file_list
62 75
}
......
65 78
    while IFS=, read -r file main opts
66 79
    do
67 80
	name=`basename "$file" .lus`
81
	if [ `dirname "$file"`/"$name" = "$file" ]; then
82
	    return 0
83
	fi
68 84
	dir=${SRC_PREFIX}/`dirname "$file"`
69 85

  
70 86
	pushd $dir > /dev/null
......
78 94
    fi
79 95
    pushd $build > /dev/null
80 96
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
81
    popd > /dev/null
82 97
    if [ $? -ne 0 ]; then
83 98
        rgcc2="INVALID";
84 99
    else
85 100
        rgcc2="VALID"
86
    fi	
101
    fi
102
    popd > /dev/null
87 103
    if [ $verbose -gt 0 ]; then
88 104
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
89 105
    else
......
98 114
    while IFS=, read -r file main opts
99 115
    do
100 116
	name=`basename "$file" .lus`
117
	if [ "$name" = "$file" ]; then
118
	    return 0
119
	fi
101 120
	dir=${SRC_PREFIX}/`dirname "$file"`
102 121
	pushd $dir > /dev/null
103 122
    $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
......
108 127
    fi
109 128
    pushd $build > /dev/null
110 129
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
111
    popd > /dev/null
112 130
    if [ $? -ne 0 ]; then
113 131
        rgcc2="INVALID";
114 132
    else
115 133
        rgcc2="VALID"
116 134
    fi	
135
    popd > /dev/null
117 136
	# Cheching witness
118 137
    pushd $build > /dev/null
119 138
    $LUSTREC -verbose 0 -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
......
142 161
    while IFS=, read -r file main opts
143 162
    do
144 163
	name=`basename "$file" .lus`
164
	if [ "$name" = "$file" ]; then
165
	    return 0
166
	fi
145 167
	dir=${SRC_PREFIX}/`dirname "$file"`
146 168
	pushd $dir > /dev/null
147 169
	

Also available in: Unified diff