Skip to content
Snippets Groups Projects
Commit d6ad6c26 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[tests] dune: fix test directory 'libc'

parent 261b09bb
No related branches found
No related tags found
No related merge requests found
/* run.config*
PLUGIN: @PTEST_PLUGIN@ metrics
OPT: -eva-no-builtins-auto @EVA_OPTIONS@ @PTEST_SHARE_DIR@/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc
OPT: -eva-no-builtins-auto @EVA_OPTIONS@ @FRAMAC_SHARE@/libc/string.c -eva -eva-slevel 6 -metrics-eva-cover -then -metrics-libc
*/
#include "string.h"
......
/* run.config*
PLUGIN: @EVA_PLUGINS@ metrics
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -cpp-extra-args='-nostdinc -I@PTEST_SHARE_DIR@/libc' @PTEST_FILE@ -save @PTEST_NAME@.sav >@PTEST_NAME@_sav.res 2>@PTEST_NAME@_sav.err
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -cpp-extra-args='-nostdinc -I@FRAMAC_SHARE@/libc' @PTEST_FILE@ -save @PTEST_NAME@.sav >@PTEST_NAME@_sav.res 2>@PTEST_NAME@_sav.err
MODULE: check_libc_naming_conventions, check_const
OPT: -load %{dep:@PTEST_NAME@.sav} -print -cpp-extra-args='-nostdinc -I@PTEST_SHARE_DIR@/libc' -eva @EVA_CONFIG@ -then -lib-entry -no-print
OPT: -load %{dep:@PTEST_NAME@.sav} -print -cpp-extra-args='-nostdinc -I@FRAMAC_SHARE@/libc' -eva @EVA_CONFIG@ -then -lib-entry -no-print
MODULE:
OPT: -print -print-libc -machdep x86_32
MODULE: check_parsing_individual_headers
......@@ -13,7 +13,7 @@
OPT: -kernel-msg-key printer:attrs
MODULE:
OPT: -load %{dep:@PTEST_NAME@.sav} -metrics -metrics-libc -then -lib-entry -metrics-no-libc | ./check_some_metrics.sh "> 100" "> 400" "< 2" "> 20" "= 1" "= 1" "= 0" "= 0" "= 0" "= 1"
CMD: %{dep:./check_full_libc.sh} @PTEST_SHARE_DIR@/libc
CMD: %{dep:./check_full_libc.sh} @FRAMAC_SHARE@/libc
OPT:
**/
#define __FC_REG_TEST
......
/* run.config*
COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
CMD: gcc -D__FC_MACHDEP_X86_64 @PTEST_SHARE_DIR@/libc/__fc_runtime.c -Wno-attributes -std=c99 -Wall -Wwrite-strings -o @DEV_NULL@
CMD: gcc -D__FC_MACHDEP_X86_64 @FRAMAC_SHARE@/libc/__fc_runtime.c -Wno-attributes -std=c99 -Wall -Wwrite-strings -o @DEV_NULL@
OPT:
*/
......
/* run.config
STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-include@PTEST_SHARE_DIR@/libc/string.c -eva-slevel-function strcpy:20,strncpy:5,strcmp:6,strchr:20,strrchr:20,strncat:4,memset:32,strlen:20,memcmp:8 -eva-no-skip-stdlib-specs"
STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-include@FRAMAC_SHARE@/libc/string.c -eva-slevel-function strcpy:20,strncpy:5,strcmp:6,strchr:20,strrchr:20,strncat:4,memset:32,strlen:20,memcmp:8 -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
......
/* run.config
STDOPT: #"-cpp-extra-args=-include@PTEST_SHARE_DIR@/libc/string.c -eva-slevel-function strchr:256,main:256 -eva-slevel-merge-after-loop main -eva-no-builtins-auto -eva-no-skip-stdlib-specs"
STDOPT: #"-cpp-extra-args=-include@FRAMAC_SHARE@/libc/string.c -eva-slevel-function strchr:256,main:256 -eva-slevel-merge-after-loop main -eva-no-builtins-auto -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
......
/* run.config
STDOPT: #"-cpp-extra-args=-include@PTEST_SHARE_DIR@/libc/string.c -eva-slevel-function strstr:30 -eva-no-skip-stdlib-specs"
STDOPT: #"-cpp-extra-args=-include@FRAMAC_SHARE@/libc/string.c -eva-slevel-function strstr:30 -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
......
PLUGIN: @EVA_PLUGINS@
OPT: -eva @EVA_CONFIG@ -cpp-extra-args='-nostdinc -I@PTEST_SHARE_DIR@/libc'
OPT: -eva @EVA_CONFIG@ -cpp-extra-args='-nostdinc -I@FRAMAC_SHARE@/libc'
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment