Project

General

Profile

Revision 8f1c7e91 test/test-compile.sh

View differences:

test/test-compile.sh
51 51
        fi
52 52
    fi
53 53
    popd > /dev/null
54
    echo "lustrec ($rlustrec1), gcc($rgcc1), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
54
    echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
55 55
    done < $file_list
56 56
}
57 57

  
......
78 78
    else
79 79
        rgcc2="VALID"
80 80
    fi	
81
    echo "lustrec inlined ($rlustrec2), gcc ($rgcc2),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
81
    echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
82 82
    popd > /dev/null
83 83
done < $file_list
84 84
}
......
106 106
    fi	
107 107
	# Cheching witness
108 108
    pushd $build > /dev/null
109
    lustrec -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 2>/dev/null
109
    $LUSTREC -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 2>/dev/null
110 110
    popd > /dev/null
111 111
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
112 112
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
......
119 119
	rinlining="INVALID"
120 120
	exit 1
121 121
    fi  
122
    echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
122
    echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
123 123
    popd > /dev/null
124 124
done < $file_list
125 125

  
......
146 146
    else
147 147
        rhorn="VALID"
148 148
    fi
149
    echo "horn-pdr ($rhorn), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
149
    echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
150 150
    popd > /dev/null
151 151
done < $file_list
152 152
}

Also available in: Unified diff