vfprintf and several other library functions dereference a FILE*-typed stream
parameter to make sure pointer checks and bounds checks are triggered. As we do
not set up stdin, stdout, stderr to point to valid FILE-typed objects, make sure
we never attempt such dereferencing if the stream argument is
stdin/stdout/stderr (unless the use of any of those would in itself constitute
an error, as is the case in fseek, for example).
We model a number of library functions, but do not necessarily verify them
against any kind of specification. We should make sure that they are at least
free from memory errors. This commit introduces them effectively as a long to-do
list, where each test should eventually be completed and marked as CORE.
The tests were generated using the following script, with a manual removal of
java::java.io.InputStream.read:()I-01 afterwards:
#!/bin/bash
for lib in src/ansi-c/library/*.c src/cpp/library/*.c
do
echo "lib: $lib"
header=$(basename $lib .c)
echo "header: $header"
for f in $(git grep FUNCTION: $lib | cut -f3 -d" " | sort | uniq)
do
echo "f: $f"
test_dir="regression/cbmc-library/${f}-01"
if [ ! -d $test_dir ]
then
mkdir -p $test_dir
cat > $test_dir/main.c <<EOF
#include <$header.h>
#include <assert.h>
int main()
{
$f();
assert(0);
return 0;
}
EOF
git add $test_dir/main.c
cat > $test_dir/test.desc <<EOF
KNOWNBUG
main.c
--pointer-check --bounds-check
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
EOF
git add $test_dir/test.desc
fi
done
done
bla