Skip to content
Snippets Groups Projects
Commit f8974ea2 authored by François Bobot's avatar François Bobot
Browse files

tests works in libc

parent 9a70f846
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 772 additions and 8326 deletions
Makefile
+ 1
− 1
View file @ f8974ea2
......@@ -168,7 +168,7 @@ force-reconfigure:
##############################################################################
.PHONY: tests
TESTS=cil float idct rte slicing scope value syntax misc builtins
TESTS=cil float idct rte slicing scope value syntax misc builtins libc
tests: config.sed
find tests -name dune | grep -e "oracle.*/\|result.*/" | xargs --no-run-if-empty rm
dune exec -- ptests/ptests.exe
......
share/dune
+ 6
− 0
View file @ f8974ea2
......@@ -29,6 +29,7 @@
(libc/sys/signal.h as libc/sys/signal.h)
(libc/sys/timex.h as libc/sys/timex.h)
(libc/sys/mman.h as libc/sys/mman.h)
(libc/sys/param.h as libc/sys/param.h)
(libc/__fc_define_dev_t.h as libc/__fc_define_dev_t.h)
(libc/glob.h as libc/glob.h)
(libc/__fc_define_id_t.h as libc/__fc_define_id_t.h)
......@@ -82,6 +83,7 @@
(libc/iconv.h as libc/iconv.h)
(libc/netinet/in.h as libc/netinet/in.h)
(libc/netinet/tcp.h as libc/netinet/tcp.h)
(libc/netinet/ip.h as libc/netinet/ip.h)
(libc/nl_types.h as libc/nl_types.h)
(libc/libgen.h as libc/libgen.h)
(libc/string.c as libc/string.c)
......@@ -174,4 +176,8 @@
(analysis-scripts/results_display.py as analysis-scripts/results_display.py)
(analysis-scripts/summary.py as analysis-scripts/summary.py)
(analysis-scripts/template.mk as analysis-scripts/template.mk)
(compliance/c11_functions.json as compliance/c11_functions.json)
(compliance/glibc_functions.json as compliance/glibc_functions.json)
(compliance/nonstandard_identifiers.json as compliance/nonstandard_identifiers.json)
(compliance/posix_identifiers.json as compliance/posix_identifiers.json)
))
tests/libc/check_full_libc.sh
+ 5
− 5
View file @ f8974ea2
#!/bin/sh
cd share/libc
LIBC=$(frama-c -print-share-path)/libc
for A in `ls *.h */*.h`;
for A in `find $LIBC -name "*.h" -printf "%P\n"`;
do
if ! grep -q $A ../../fc_libc.c ;
if ! grep -q $A fc_libc.c ;
then echo "#include \"$A"\";
fi ;
done;
for A in `ls *.c`;
for A in `find $LIBC -name "*.c" -printf "%P\n"`;
do
if ! grep -q $A __fc_runtime.c ../../fc_libc.c ;
if ! grep -q $A $LIBC/__fc_runtime.c fc_libc.c ;
then echo Not included implementation \'$A\';
fi ;
done;
tests/libc/check_parsing_individual_headers.ml
+ 2
− 2
View file @ f8974ea2
......@@ -8,7 +8,7 @@ let is_header f = Str.string_match header_re f 0
(* Files which are *not* supposed to be parsed *)
let blacklist () =
let libc = (Filename.concat (Sys.getenv "FRAMAC_SHARE") "libc") in
let libc = (Filename.concat Fc_config.datadir "libc") in
List.map (fun f ->
Datatype.Filepath.of_string (Filename.concat libc f))
["tgmath.h"; "complex.h"; "__fc_machdep_linux_shared.h"]
......@@ -42,4 +42,4 @@ let collect_headers libc_dir =
) all_headers
let () =
Db.Main.apply (collect_headers (Filename.concat (Sys.getenv "FRAMAC_SHARE") "libc"))
Db.Main.apply (collect_headers (Filename.concat Fc_config.datadir "libc"))
tests/libc/coverage.c
+ 2
− 1
View file @ f8974ea2
/* run.config*
PLUGIN: metrics
DEPS: ../../../share/libc/string.c
OPT: -eva-no-builtins-auto @EVA_OPTIONS@ ../../share/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc
OPT: -eva-no-builtins-auto @EVA_OPTIONS@ ../../../share/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc
*/
#include "string.h"
......
tests/libc/fc_libc.c
+ 6
− 4
View file @ f8974ea2
......@@ -4,11 +4,13 @@
CMXS: check_parsing_individual_headers
CMXS: check_libc_anonymous_tags
CMXS: check_compliance
OPT: -load-module check_libc_naming_conventions -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module check_const -load-module metrics -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc
PLUGIN: metrics
OPT: -load-module %{dep:check_libc_naming_conventions.cmxs} -print -cpp-extra-args='-nostdinc' -metrics -metrics-libc -load-module %{dep:check_const.cmxs} -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc
OPT: -print -print-libc
OPT: -load-module check_parsing_individual_headers
OPT: -load-module check_libc_anonymous_tags
OPT: -load-module check_compliance -kernel-msg-key printer:attrs
OPT: -load-module %{dep:check_parsing_individual_headers.cmxs}
OPT: -load-module %{dep:check_libc_anonymous_tags.cmxs}
OPT: -load-module %{dep:check_compliance.cmxs} -kernel-msg-key printer:attrs
DEPS: ./check_full_libc.sh
CMD: ./check_full_libc.sh
OPT:
**/
......
tests/libc/oracle/coverage.res.oracle
+ 38
− 2
View file @ f8974ea2
[kernel] User Error: source file 'share/libc/string.c' does not exist
[kernel] Frama-C aborted: invalid user input.
[kernel] Parsing coverage.c (with preprocessing)
[kernel] Parsing /home/bobot/Sources/frama-c/_build/default/share/libc/string.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva] computing for function strlen <- main.
Called from coverage.c:11.
[eva] Recording results for strlen
[eva] Done for function strlen
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function strlen:
i ∈ {6}
[eva:final-states] Values at end of function main:
s ∈ {{ "blabli" }}
l ∈ {6}
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 1 (out of 1)
Semantically reached functions = 1
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
4 stmts in analyzed functions, 4 stmts analyzed (100.0%)
main: 4 stmts out of 4 (100.0%)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 2 (out of 116)
Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
10 stmts in analyzed functions, 10 stmts analyzed (100.0%)
main: 4 stmts out of 4 (100.0%)
strlen: 6 stmts out of 6 (100.0%)
tests/libc/oracle/fc_libc.0.res.oracle
+ 7
− 6
View file @ f8974ea2
......@@ -4,10 +4,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva] fc_libc.c:155: assertion got status valid.
[eva] fc_libc.c:156: assertion got status valid.
[eva] fc_libc.c:157: assertion got status valid.
[eva] fc_libc.c:158: assertion got status valid.
[eva] fc_libc.c:159: assertion got status valid.
[eva] fc_libc.c:160: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
......@@ -41,11 +41,12 @@
wcscpy (0 call); wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call);
wmemcpy (0 call); wmemset (0 call);
Undefined functions (412)
Undefined functions (415)
=========================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
Frama_C_long_long_interval (0 call);
Frama_C_abstract_cardinal (0 call); Frama_C_abstract_max (0 call);
Frama_C_abstract_min (0 call); Frama_C_int_interval (0 call);
Frama_C_long_interval (0 call); Frama_C_long_long_interval (0 call);
Frama_C_real_interval_as_double (0 call); Frama_C_short_interval (0 call);
Frama_C_size_t_interval (0 call); Frama_C_unsigned_char_interval (0 call);
Frama_C_unsigned_int_interval (0 call);
......@@ -187,7 +188,7 @@
Goto = 97
Assignment = 459
Exit point = 83
Function = 495
Function = 498
Function call = 93
Pointer dereferencing = 159
Cyclomatic complexity = 296
......
tests/libc/oracle/fc_libc.1.res.oracle
+ 0
− 8174
View file @ f8974ea2
This diff is collapsed.
tests/libc/oracle/fc_libc.2.res.oracle
+ 125
− 125
View file @ f8974ea2
[kernel] Parsing share/libc/__fc_alloc_axiomatic.h (with preprocessing)
[kernel] Parsing share/libc/__fc_builtin.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_blkcnt_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_blksize_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_clockid_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_dev_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_eof.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_fd_set_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_file.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_fpos_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_id_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_ino_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_intptr_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_iovec.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_key_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_mode_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_nlink_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_null.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_off_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_pid_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_pthread_types.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_sa_family_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_seek_macros.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_sigset_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_size_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_sockaddr.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_ssize_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_stat.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_suseconds_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_time_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_timer_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_timespec.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_uid_and_gid.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_useconds_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_wchar_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_define_wint_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_gcc_builtins.h (with preprocessing)
[kernel] Parsing share/libc/__fc_inet.h (with preprocessing)
[kernel] Parsing share/libc/__fc_integer.h (with preprocessing)
[kernel] Parsing share/libc/__fc_machdep.h (with preprocessing)
skipping share/libc/__fc_machdep_linux_shared.h
[kernel] Parsing share/libc/__fc_select.h (with preprocessing)
[kernel] Parsing share/libc/__fc_string_axiomatic.h (with preprocessing)
[kernel] Parsing share/libc/alloca.h (with preprocessing)
[kernel] Parsing share/libc/arpa/inet.h (with preprocessing)
[kernel] Parsing share/libc/assert.h (with preprocessing)
[kernel] Parsing share/libc/byteswap.h (with preprocessing)
skipping share/libc/complex.h
[kernel] Parsing share/libc/ctype.h (with preprocessing)
[kernel] Parsing share/libc/dirent.h (with preprocessing)
[kernel] Parsing share/libc/dlfcn.h (with preprocessing)
[kernel] Parsing share/libc/endian.h (with preprocessing)
[kernel] Parsing share/libc/errno.h (with preprocessing)
[kernel] Parsing share/libc/fcntl.h (with preprocessing)
[kernel] Parsing share/libc/features.h (with preprocessing)
[kernel] Parsing share/libc/fenv.h (with preprocessing)
[kernel] Parsing share/libc/float.h (with preprocessing)
[kernel] Parsing share/libc/fnmatch.h (with preprocessing)
[kernel] Parsing share/libc/ftw.h (with preprocessing)
[kernel] Parsing share/libc/getopt.h (with preprocessing)
[kernel] Parsing share/libc/glob.h (with preprocessing)
[kernel] Parsing share/libc/grp.h (with preprocessing)
[kernel] Parsing share/libc/iconv.h (with preprocessing)
[kernel] Parsing share/libc/ifaddrs.h (with preprocessing)
[kernel] Parsing share/libc/inttypes.h (with preprocessing)
[kernel] Parsing share/libc/iso646.h (with preprocessing)
[kernel] Parsing share/libc/libgen.h (with preprocessing)
[kernel] Parsing share/libc/limits.h (with preprocessing)
[kernel] Parsing share/libc/locale.h (with preprocessing)
[kernel] Parsing share/libc/malloc.h (with preprocessing)
[kernel] Parsing share/libc/math.h (with preprocessing)
[kernel] Parsing share/libc/memory.h (with preprocessing)
[kernel] Parsing share/libc/net/if.h (with preprocessing)
[kernel] Parsing share/libc/netdb.h (with preprocessing)
[kernel] Parsing share/libc/netinet/in.h (with preprocessing)
[kernel] Parsing share/libc/netinet/ip.h (with preprocessing)
[kernel] Parsing share/libc/netinet/tcp.h (with preprocessing)
[kernel] Parsing share/libc/nl_types.h (with preprocessing)
[kernel] Parsing share/libc/poll.h (with preprocessing)
[kernel] Parsing share/libc/pthread.h (with preprocessing)
[kernel] Parsing share/libc/pwd.h (with preprocessing)
[kernel] Parsing share/libc/regex.h (with preprocessing)
[kernel] Parsing share/libc/resolv.h (with preprocessing)
[kernel] Parsing share/libc/sched.h (with preprocessing)
[kernel] Parsing share/libc/semaphore.h (with preprocessing)
[kernel] Parsing share/libc/setjmp.h (with preprocessing)
[kernel] Parsing share/libc/signal.h (with preprocessing)
[kernel] Parsing share/libc/stdarg.h (with preprocessing)
[kernel] Parsing share/libc/stdbool.h (with preprocessing)
[kernel] Parsing share/libc/stddef.h (with preprocessing)
[kernel] Parsing share/libc/stdint.h (with preprocessing)
[kernel] Parsing share/libc/stdio.h (with preprocessing)
[kernel] Parsing share/libc/stdlib.h (with preprocessing)
[kernel] Parsing share/libc/string.h (with preprocessing)
[kernel] Parsing share/libc/strings.h (with preprocessing)
[kernel] Parsing share/libc/stropts.h (with preprocessing)
[kernel] Parsing share/libc/sys/file.h (with preprocessing)
[kernel] Parsing share/libc/sys/ioctl.h (with preprocessing)
[kernel] Parsing share/libc/sys/ipc.h (with preprocessing)
[kernel] Parsing share/libc/sys/mman.h (with preprocessing)
[kernel] Parsing share/libc/sys/param.h (with preprocessing)
[kernel] Parsing share/libc/sys/random.h (with preprocessing)
[kernel] Parsing share/libc/sys/resource.h (with preprocessing)
[kernel] Parsing share/libc/sys/select.h (with preprocessing)
[kernel] Parsing share/libc/sys/shm.h (with preprocessing)
[kernel] Parsing share/libc/sys/signal.h (with preprocessing)
[kernel] Parsing share/libc/sys/socket.h (with preprocessing)
[kernel] Parsing share/libc/sys/stat.h (with preprocessing)
[kernel] Parsing share/libc/sys/time.h (with preprocessing)
[kernel] Parsing share/libc/sys/times.h (with preprocessing)
[kernel] Parsing share/libc/sys/timex.h (with preprocessing)
[kernel] Parsing share/libc/sys/types.h (with preprocessing)
[kernel] Parsing share/libc/sys/uio.h (with preprocessing)
[kernel] Parsing share/libc/sys/un.h (with preprocessing)
[kernel] Parsing share/libc/sys/utsname.h (with preprocessing)
[kernel] Parsing share/libc/sys/wait.h (with preprocessing)
[kernel] Parsing share/libc/syslog.h (with preprocessing)
[kernel] Parsing share/libc/termios.h (with preprocessing)
skipping share/libc/tgmath.h
[kernel] Parsing share/libc/time.h (with preprocessing)
[kernel] Parsing share/libc/unistd.h (with preprocessing)
[kernel] Parsing share/libc/utime.h (with preprocessing)
[kernel] Parsing share/libc/utmpx.h (with preprocessing)
[kernel] Parsing share/libc/wchar.h (with preprocessing)
[kernel] Parsing share/libc/wctype.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_alloc_axiomatic.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_blkcnt_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_blksize_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_clockid_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_dev_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_eof.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_fd_set_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_file.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_fpos_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_id_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_ino_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_intptr_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_iovec.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_key_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_mode_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_nlink_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_null.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_off_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_pid_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_pthread_types.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_sa_family_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_seek_macros.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_sigset_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_size_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_sockaddr.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_ssize_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_stat.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_suseconds_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_time_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_timer_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_timespec.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_uid_and_gid.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_useconds_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_wchar_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_define_wint_t.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_gcc_builtins.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_inet.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_integer.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_machdep.h (with preprocessing)
skipping FRAMAC_SHARE/libc/__fc_machdep_linux_shared.h
[kernel] Parsing FRAMAC_SHARE/libc/__fc_select.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/__fc_string_axiomatic.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/alloca.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/arpa/inet.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/assert.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/byteswap.h (with preprocessing)
skipping FRAMAC_SHARE/libc/complex.h
[kernel] Parsing FRAMAC_SHARE/libc/ctype.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/dirent.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/dlfcn.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/endian.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/errno.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/fcntl.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/features.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/fenv.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/float.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/fnmatch.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/ftw.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/getopt.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/glob.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/grp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/iconv.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/ifaddrs.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/inttypes.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/iso646.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/libgen.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/limits.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/locale.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/malloc.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/math.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/memory.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/net/if.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/netdb.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/netinet/in.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/netinet/ip.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/netinet/tcp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/nl_types.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/poll.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/pthread.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/pwd.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/regex.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/resolv.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sched.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/semaphore.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/setjmp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/signal.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/stdarg.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/stdbool.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/stddef.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/stdint.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/stdio.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/stdlib.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/string.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/strings.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/stropts.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/file.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/ioctl.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/ipc.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/mman.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/param.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/random.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/resource.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/select.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/shm.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/signal.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/socket.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/stat.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/time.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/times.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/timex.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/types.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/uio.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/un.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/utsname.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/sys/wait.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/syslog.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/termios.h (with preprocessing)
skipping FRAMAC_SHARE/libc/tgmath.h
[kernel] Parsing FRAMAC_SHARE/libc/time.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/unistd.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/utime.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/utmpx.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/wchar.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/wctype.h (with preprocessing)
[kernel] Parsing fc_libc.c (with preprocessing)
tests/libc/oracle/string_c_strchr.res.oracle
+ 579
− 5
View file @ f8974ea2
[kernel] Parsing string_c_strchr.c (with preprocessing)
[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -includeshare/libc/string.c -nostdinc -Ishare/libc -dD -nostdinc -m32 -o '/tmp/string_c_strchr.c2df54c.i' '/home/bobot/Sources/frama-c/_build/default/result/string_c_strchr.c'
See chapter "Preparing the Sources" in the Frama-C user manual for more details.
[kernel] User Error: stopping on file "string_c_strchr.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva] string_c_strchr.c:58: Trace partitioning superposing up to 100 states
[eva] string_c_strchr.c:60: Trace partitioning superposing up to 200 states
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:63.
[eva] string_c_strchr.c:63:
function strchr: precondition 'valid_string_s' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:168:
function strchr, behavior not_found: postcondition 'result_null' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:171:
function strchr, behavior default: postcondition 'result_null_or_same_base' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:64.
[eva] string_c_strchr.c:64:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:65.
[eva] string_c_strchr.c:65:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:66.
[eva] string_c_strchr.c:66:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:67.
[eva] string_c_strchr.c:67:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:68.
[eva] string_c_strchr.c:68:
function strchr: precondition 'valid_string_s' got status valid.
[eva] FRAMAC_SHARE/libc/string.c:229:
Trace partitioning superposing up to 100 states
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:69.
[eva] string_c_strchr.c:69:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:71.
[eva] string_c_strchr.c:71:
function strchr: precondition 'valid_string_s' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:161:
function strchr, behavior found: postcondition 'result_char' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:162:
function strchr, behavior found: postcondition 'result_same_base' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:163:
function strchr, behavior found: postcondition 'result_in_length' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:164:
function strchr, behavior found: postcondition 'result_valid_string' got status valid.
[eva:alarm] FRAMAC_SHARE/libc/string.h:165: Warning:
function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:72.
[eva] string_c_strchr.c:72:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:73.
[eva] string_c_strchr.c:73:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:74.
[eva] string_c_strchr.c:74:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:75.
[eva] string_c_strchr.c:75:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:76.
[eva] string_c_strchr.c:76:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:77.
[eva] string_c_strchr.c:77:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:78.
[eva] string_c_strchr.c:78:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:79.
[eva] string_c_strchr.c:79:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:80.
[eva] string_c_strchr.c:80:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:81.
[eva] string_c_strchr.c:81:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:82.
[eva] string_c_strchr.c:82:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:83.
[eva] string_c_strchr.c:83:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:84.
[eva] string_c_strchr.c:84:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:85.
[eva] string_c_strchr.c:85:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:86.
[eva] string_c_strchr.c:86:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:87.
[eva] string_c_strchr.c:87:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:88.
[eva] string_c_strchr.c:88:
function strchr: precondition 'valid_string_s' got status valid.
[eva] FRAMAC_SHARE/libc/string.c:229:
Trace partitioning superposing up to 200 states
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
Called from string_c_strchr.c:89.
[eva] string_c_strchr.c:89:
function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function strchr:
ch ∈ [--..--]
i ∈ [0..255]
__retres ∈
{{ NULL ; &s{[0], [1], [9], [10], [126], [127], [254], [255]} ;
"" ; "a" ; "a" ; "a" + {1} ; "abb" + {1} ; "aabb" + {2} ;
"aaabb" + {3} ; "aaaabb" + {4} ; "aaaaabb" + {5} ;
"aaaaaabb" + {6} ; "abc abc" + {2} }}
[eva:final-states] Values at end of function main:
i ∈ {256}
a[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {3}
[3] ∈ {4}
[4] ∈ {5}
[5] ∈ {6}
[6] ∈ {7}
[7] ∈ {8}
[8] ∈ {9}
[9] ∈ {10}
[10] ∈ {11}
[11] ∈ {12}
[12] ∈ {13}
[13] ∈ {14}
[14] ∈ {15}
[15] ∈ {16}
[16] ∈ {17}
[17] ∈ {18}
[18] ∈ {19}
[19] ∈ {20}
[20] ∈ {21}
[21] ∈ {22}
[22] ∈ {23}
[23] ∈ {24}
[24] ∈ {25}
[25] ∈ {26}
[26] ∈ {27}
[27] ∈ {28}
[28] ∈ {29}
[29] ∈ {30}
[30] ∈ {31}
[31] ∈ {32}
[32] ∈ {33}
[33] ∈ {34}
[34] ∈ {35}
[35] ∈ {36}
[36] ∈ {37}
[37] ∈ {38}
[38] ∈ {39}
[39] ∈ {40}
[40] ∈ {41}
[41] ∈ {42}
[42] ∈ {43}
[43] ∈ {44}
[44] ∈ {45}
[45] ∈ {46}
[46] ∈ {47}
[47] ∈ {48}
[48] ∈ {49}
[49] ∈ {50}
[50] ∈ {51}
[51] ∈ {52}
[52] ∈ {53}
[53] ∈ {54}
[54] ∈ {55}
[55] ∈ {56}
[56] ∈ {57}
[57] ∈ {58}
[58] ∈ {59}
[59] ∈ {60}
[60] ∈ {61}
[61] ∈ {62}
[62] ∈ {63}
[63] ∈ {64}
[64] ∈ {65}
[65] ∈ {66}
[66] ∈ {67}
[67] ∈ {68}
[68] ∈ {69}
[69] ∈ {70}
[70] ∈ {71}
[71] ∈ {72}
[72] ∈ {73}
[73] ∈ {74}
[74] ∈ {75}
[75] ∈ {76}
[76] ∈ {77}
[77] ∈ {78}
[78] ∈ {79}
[79] ∈ {80}
[80] ∈ {81}
[81] ∈ {82}
[82] ∈ {83}
[83] ∈ {84}
[84] ∈ {85}
[85] ∈ {86}
[86] ∈ {87}
[87] ∈ {88}
[88] ∈ {89}
[89] ∈ {90}
[90] ∈ {91}
[91] ∈ {92}
[92] ∈ {93}
[93] ∈ {94}
[94] ∈ {95}
[95] ∈ {96}
[96] ∈ {97}
[97] ∈ {98}
[98] ∈ {99}
[99] ∈ {100}
[100] ∈ {101}
[101] ∈ {102}
[102] ∈ {103}
[103] ∈ {104}
[104] ∈ {105}
[105] ∈ {106}
[106] ∈ {107}
[107] ∈ {108}
[108] ∈ {109}
[109] ∈ {110}
[110] ∈ {111}
[111] ∈ {112}
[112] ∈ {113}
[113] ∈ {114}
[114] ∈ {115}
[115] ∈ {116}
[116] ∈ {117}
[117] ∈ {118}
[118] ∈ {119}
[119] ∈ {120}
[120] ∈ {121}
[121] ∈ {122}
[122] ∈ {123}
[123] ∈ {124}
[124] ∈ {125}
[125] ∈ {126}
[126] ∈ {127}
[127] ∈ {0}
s[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {3}
[3] ∈ {4}
[4] ∈ {5}
[5] ∈ {6}
[6] ∈ {7}
[7] ∈ {8}
[8] ∈ {9}
[9] ∈ {10}
[10] ∈ {11}
[11] ∈ {12}
[12] ∈ {13}
[13] ∈ {14}
[14] ∈ {15}
[15] ∈ {16}
[16] ∈ {17}
[17] ∈ {18}
[18] ∈ {19}
[19] ∈ {20}
[20] ∈ {21}
[21] ∈ {22}
[22] ∈ {23}
[23] ∈ {24}
[24] ∈ {25}
[25] ∈ {26}
[26] ∈ {27}
[27] ∈ {28}
[28] ∈ {29}
[29] ∈ {30}
[30] ∈ {31}
[31] ∈ {32}
[32] ∈ {33}
[33] ∈ {34}
[34] ∈ {35}
[35] ∈ {36}
[36] ∈ {37}
[37] ∈ {38}
[38] ∈ {39}
[39] ∈ {40}
[40] ∈ {41}
[41] ∈ {42}
[42] ∈ {43}
[43] ∈ {44}
[44] ∈ {45}
[45] ∈ {46}
[46] ∈ {47}
[47] ∈ {48}
[48] ∈ {49}
[49] ∈ {50}
[50] ∈ {51}
[51] ∈ {52}
[52] ∈ {53}
[53] ∈ {54}
[54] ∈ {55}
[55] ∈ {56}
[56] ∈ {57}
[57] ∈ {58}
[58] ∈ {59}
[59] ∈ {60}
[60] ∈ {61}
[61] ∈ {62}
[62] ∈ {63}
[63] ∈ {64}
[64] ∈ {65}
[65] ∈ {66}
[66] ∈ {67}
[67] ∈ {68}
[68] ∈ {69}
[69] ∈ {70}
[70] ∈ {71}
[71] ∈ {72}
[72] ∈ {73}
[73] ∈ {74}
[74] ∈ {75}
[75] ∈ {76}
[76] ∈ {77}
[77] ∈ {78}
[78] ∈ {79}
[79] ∈ {80}
[80] ∈ {81}
[81] ∈ {82}
[82] ∈ {83}
[83] ∈ {84}
[84] ∈ {85}
[85] ∈ {86}
[86] ∈ {87}
[87] ∈ {88}
[88] ∈ {89}
[89] ∈ {90}
[90] ∈ {91}
[91] ∈ {92}
[92] ∈ {93}
[93] ∈ {94}
[94] ∈ {95}
[95] ∈ {96}
[96] ∈ {97}
[97] ∈ {98}
[98] ∈ {99}
[99] ∈ {100}
[100] ∈ {101}
[101] ∈ {102}
[102] ∈ {103}
[103] ∈ {104}
[104] ∈ {105}
[105] ∈ {106}
[106] ∈ {107}
[107] ∈ {108}
[108] ∈ {109}
[109] ∈ {110}
[110] ∈ {111}
[111] ∈ {112}
[112] ∈ {113}
[113] ∈ {114}
[114] ∈ {115}
[115] ∈ {116}
[116] ∈ {117}
[117] ∈ {118}
[118] ∈ {119}
[119] ∈ {120}
[120] ∈ {121}
[121] ∈ {122}
[122] ∈ {123}
[123] ∈ {124}
[124] ∈ {125}
[125] ∈ {126}
[126] ∈ {127}
[127] ∈ {128}
[128] ∈ {129}
[129] ∈ {130}
[130] ∈ {131}
[131] ∈ {132}
[132] ∈ {133}
[133] ∈ {134}
[134] ∈ {135}
[135] ∈ {136}
[136] ∈ {137}
[137] ∈ {138}
[138] ∈ {139}
[139] ∈ {140}
[140] ∈ {141}
[141] ∈ {142}
[142] ∈ {143}
[143] ∈ {144}
[144] ∈ {145}
[145] ∈ {146}
[146] ∈ {147}
[147] ∈ {148}
[148] ∈ {149}
[149] ∈ {150}
[150] ∈ {151}
[151] ∈ {152}
[152] ∈ {153}
[153] ∈ {154}
[154] ∈ {155}
[155] ∈ {156}
[156] ∈ {157}
[157] ∈ {158}
[158] ∈ {159}
[159] ∈ {160}
[160] ∈ {161}
[161] ∈ {162}
[162] ∈ {163}
[163] ∈ {164}
[164] ∈ {165}
[165] ∈ {166}
[166] ∈ {167}
[167] ∈ {168}
[168] ∈ {169}
[169] ∈ {170}
[170] ∈ {171}
[171] ∈ {172}
[172] ∈ {173}
[173] ∈ {174}
[174] ∈ {175}
[175] ∈ {176}
[176] ∈ {177}
[177] ∈ {178}
[178] ∈ {179}
[179] ∈ {180}
[180] ∈ {181}
[181] ∈ {182}
[182] ∈ {183}
[183] ∈ {184}
[184] ∈ {185}
[185] ∈ {186}
[186] ∈ {187}
[187] ∈ {188}
[188] ∈ {189}
[189] ∈ {190}
[190] ∈ {191}
[191] ∈ {192}
[192] ∈ {193}
[193] ∈ {194}
[194] ∈ {195}
[195] ∈ {196}
[196] ∈ {197}
[197] ∈ {198}
[198] ∈ {199}
[199] ∈ {200}
[200] ∈ {201}
[201] ∈ {202}
[202] ∈ {203}
[203] ∈ {204}
[204] ∈ {205}
[205] ∈ {206}
[206] ∈ {207}
[207] ∈ {208}
[208] ∈ {209}
[209] ∈ {210}
[210] ∈ {211}
[211] ∈ {212}
[212] ∈ {213}
[213] ∈ {214}
[214] ∈ {215}
[215] ∈ {216}
[216] ∈ {217}
[217] ∈ {218}
[218] ∈ {219}
[219] ∈ {220}
[220] ∈ {221}
[221] ∈ {222}
[222] ∈ {223}
[223] ∈ {224}
[224] ∈ {225}
[225] ∈ {226}
[226] ∈ {227}
[227] ∈ {228}
[228] ∈ {229}
[229] ∈ {230}
[230] ∈ {231}
[231] ∈ {232}
[232] ∈ {233}
[233] ∈ {234}
[234] ∈ {235}
[235] ∈ {236}
[236] ∈ {237}
[237] ∈ {238}
[238] ∈ {239}
[239] ∈ {240}
[240] ∈ {241}
[241] ∈ {242}
[242] ∈ {243}
[243] ∈ {244}
[244] ∈ {245}
[245] ∈ {246}
[246] ∈ {247}
[247] ∈ {248}
[248] ∈ {249}
[249] ∈ {250}
[250] ∈ {251}
[251] ∈ {252}
[252] ∈ {253}
[253] ∈ {254}
[254] ∈ {255}
[255] ∈ {0}
__retres ∈ {0}
tests/libc/runtime.c
+ 1
− 1
View file @ f8974ea2
/* run.config*
COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
DEPS: ../../../share/libc/__fc_runtime.c
CMD: gcc -D__FC_MACHDEP_X86_64 ../../share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null
CMD: gcc -D__FC_MACHDEP_X86_64 ../../../share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null
OPT:
*/
......
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