Commit 0f690976 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Fix c_cursor session and add it to regression tests

parent a413a195
......@@ -307,6 +307,45 @@ extract_and_test_wmp () {
fi
}
extract_and_test_c () {
dir=$1
shift
printf " $dir... "
printf "clean... "
if BENCH=yes make -C $dir clean > /dev/null; then
printf "extract... "
if BENCH=yes make -C $dir extract > /dev/null; then
printf "compile... "
if BENCH=yes make -C $dir cfiles > /dev/null; then
printf "execute... "
if BENCH=yes make -C $dir tests > /dev/null; then
echo "ok"
else
echo "execution failed!"
echo BENCH=yes make -C $dir tests
BENCH=yes make -C $dir tests
exit 1
fi
else
echo "compilation failed!"
echo BENCH=yes make -C $dir cfiles
BENCH=yes make -C $dir cfiles
exit 1
fi
else
echo "extract failed!"
echo BENCH=yes make -C $dir extract
BENCH=yes make -C $dir extract
exit 1
fi
else
echo "clean failed!"
echo BENCH=yes make -C $dir clean
BENCH=yes make -C $dir clean
exit 1
fi
}
list_stuff () {
pgm="bin/why3$suffix"
printf ' %s ' "$1"
......@@ -476,6 +515,7 @@ echo ""
echo "=== Checking extraction to C ==="
extract_and_test_wmp examples/multiprecision
extract_and_test_c examples/c_cursor
echo ""
echo "=== Checking replay without shapes ==="
......@@ -496,6 +536,7 @@ replay examples/WP_revisited --merging-only
replay examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps --merging-only"
replay examples/bitvectors "-L examples/bitvectors --merging-only"
replay examples/avl "-L examples/avl --merging-only"
replay examples/c_cursor "-L examples/c_cursor --merging-only"
replay examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication --merging-only"
replay examples/double_wp "-L examples/double_wp --merging-only"
#replay examples/in_progress/ring_decision "-L examples/in_progress/ring_decision --merging-only"
......
......@@ -20,7 +20,8 @@ why3:
make -C ../..
extract: why3 dir
$(WHY3) extract -D cursor.drv -D c -L . -o build/ptrcursor.c ccursor.PtrCursor
$(WHY3) extract -D cursor.drv -D c -L . --recursive --modular \
--interface --debug=c_no_error_msgs -o build/ ccursor.PtrCursor
cfiles: extract
gcc -Wall -g -pedantic -Wno-unused-function -std=c11 build/ptrcursor.c -Ibuild -o build/tests
......
......@@ -10,6 +10,7 @@ module PtrCursor
val ghost dummy_nonnull () : ptr int32
ensures { is_not_null result /\ plength result = 1 /\ offset result = 0 }
ensures { min result = 0 /\ max result = plength result }
ensures { writable result }
ensures { (data result)[0] = 0 }
type cursor = {
......@@ -27,6 +28,7 @@ module PtrCursor
min current = 0 /\
max current = len /\
is_not_null current /\
writable current /\
forall i. 0 <= i < len -> (data current)[i] < bound) }
by { current = dummy_nonnull (); new = true;
len = 1; freed = false; bound = 42 }
......
This diff is collapsed.
......@@ -82,6 +82,7 @@ echo ""
run_dir . ""
run_dir double_wp "-L double_wp"
run_dir avl "-L avl"
run_dir c_cursor "-L c_cursor"
run_dir foveoos11-cm ""
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
run_dir verifythis_2016_matrix_multiplication "-L verifythis_2016_matrix_multiplication"
......
Supports Markdown
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