Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 963257d7 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

ce-bench: remove steps information from the output

parent a52c75c5
......@@ -77,12 +77,15 @@ run () {
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
# This ad hoc sed removes diff between Timeout and Unknown (unknown)
# when running from platform with different speed.
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' | \
sed -r 's/(Timeout.*$|Unknown \(unknown\).*$)/Timeout or Unknown/' | \
# ad hoc sed to remove the directory of the stdlib that can be found
# inside labels attribute [@at:'Old:loc:/home/.../stdlib/array.mlw
# TODO temporary as this comes from incorrect locations generated in
# a[i] <- x like terms.
sed -r 's/\:loc\:.*\]/\:loc\:location\]/' >> "$f.out"
sed -r 's/\:loc\:.*\]/\:loc\:location\]/' | \
# Remove steps informations
sed -r 's/Unknown \(sat\).*$/Unknown \(sat\)/' | \
sed -r 's/Valid \(.*$/Valid/' >> "$f.out"
str_oracle=$(tr -d ' \n' < "${oracle_file}")
str_out=$(tr -d ' \n' < "$f.out")
decide_fail $f
Markdown is supported
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