Skip to content
Snippets Groups Projects
Commit dba986fa authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[Tests] using @FRAMA_SHARE@ macro

parent 190cb4fe
No related branches found
No related tags found
No related merge requests found
/*run.config /*run.config
MACRO: SHARE @FRAMAC_SHARE@/compliance COMMENT: dependency to FRAMA-C share directory is implicit
MACRO: SHARE @FRAMAC_SHARE@/compliance
NOFRAMAC: NOFRAMAC:
EXECNOW: LOG json_@PTEST_NAME@_1.txt python3 -m json.tool < @SHARE@/c11_functions.json | head -n 2 > json_@PTEST_NAME@_1.txt 2> @DEV_NULL@ EXECNOW: LOG json_@PTEST_NAME@_1.txt python3 -m json.tool < @SHARE@/c11_functions.json | head -n 2 > json_@PTEST_NAME@_1.txt 2> @DEV_NULL@
EXECNOW: LOG json_@PTEST_NAME@_2.txt python3 -m json.tool < @SHARE@/glibc_functions.json | head -n 2 > json_@PTEST_NAME@_2.txt 2> @DEV_NULL@ EXECNOW: LOG json_@PTEST_NAME@_2.txt python3 -m json.tool < @SHARE@/glibc_functions.json | head -n 2 > json_@PTEST_NAME@_2.txt 2> @DEV_NULL@
......
...@@ -6,7 +6,7 @@ DEPS: jcdb2.c with_arguments.json compile_commands.json file_without_main.c ...@@ -6,7 +6,7 @@ DEPS: jcdb2.c with_arguments.json compile_commands.json file_without_main.c
MODULE: @PTEST_NAME@ MODULE: @PTEST_NAME@
OPT: -json-compilation-database with_arguments.json OPT: -json-compilation-database with_arguments.json
MODULE: MODULE:
EXECNOW: LOG list_files.res LOG list_files.err ../../../../install/default/share/frama-c/share/analysis-scripts/list_files.py %{dep:compile_commands_working.json} > list_files.res 2> list_files.err EXECNOW: LOG list_files.res LOG list_files.err @FRAMAC_SHARE@/analysis-scripts/list_files.py %{dep:compile_commands_working.json} > list_files.res 2> list_files.err
*/ */
......
/* run.config* /* run.config*
COMMENT: dependency to FRAMA-C share directory is implicit COMMENT: dependency to FRAMA-C share directory is implicit
PLUGIN: metrics @EVA_PLUGINS@ PLUGIN: metrics @EVA_PLUGINS@
OPT: -eva-no-builtins-auto @EVA_OPTIONS@ ../../../../install/default/share/frama-c/share/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" #include "string.h"
......
/* run.config* /* run.config*
COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...) COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
COMMENT: dependency to FRAMA-C share directory is implicit COMMENT: dependency to FRAMA-C share directory is implicit
CMD: gcc @PTEST_OPTIONS@ CMD: gcc @PTEST_OPTIONS@
OPT: -D__FC_MACHDEP_X86_64 ../../../../install/default/share/frama-c/share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o @DEV_NULL@ @PTEST_FILE@ OPT: -D__FC_MACHDEP_X86_64 @FRAMAC_SHARE@/libc/__fc_runtime.c -Wno-attributes -std=c99 -o @DEV_NULL@ @PTEST_FILE@
*/ */
int main() { int main() {
......
/* run.config /* run.config
COMMENT: dependency to FRAMA-C share directory is implicit COMMENT: dependency to FRAMA-C share directory is implicit
STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-include../../../../install/default/share/frama-c/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" 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 /* This file has been adapted from libc-test, which is licensed under the
following standard MIT license: following standard MIT license:
......
/* run.config /* run.config
COMMENT: dependency to FRAMA-C share directory is implicit COMMENT: dependency to FRAMA-C share directory is implicit
STDOPT: #"-cpp-extra-args=-include../../../../install/default/share/frama-c/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" 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 /* This file has been adapted from libc-test, which is licensed under the
following standard MIT license: following standard MIT license:
......
/* run.config /* run.config
COMMENT: dependency to FRAMA-C share directory is implicit COMMENT: dependency to FRAMA-C share directory is implicit
STDOPT: #"-cpp-extra-args=-include../../../../install/default/share/frama-c/share/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 /* This file has been adapted from libc-test, which is licensed under the
following standard MIT license: following standard MIT license:
......
/* run.config /* run.config
OPT: -pp-annot -cpp-extra-args="-I./share/libc" -pp-annot -eva @EVA_OPTIONS@ MACRO: LIBC @FRAMAC_SHARE@/LIBC
OPT: -pp-annot -cpp-extra-args="-I@LIBC@" -pp-annot -eva @EVA_OPTIONS@
*/ */
#include <stdbool.h> #include <stdbool.h>
#include <stdint.h> #include <stdint.h>
#include <stdlib.h> #include <stdlib.h>
......
/* run.config /* run.config
COMMENT: checks that linking string.h and its FC-pretty-printed version COMMENT: checks that linking string.h and its FC-pretty-printed version
COMMENT: does not get rejected by name clash in the logic. See bts 1598 COMMENT: does not get rejected by name clash in the logic. See bts 1598
OPT: -cpp-extra-args " -Ishare/libc -nostdinc" -print -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then @PTEST_FILE@ ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -ocode="" -print MACRO: LIBC @FRAMAC_SHARE@/libc
OPT: -cpp-extra-args " -I@LIBC@ -nostdinc" -print -then -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -print -then @PTEST_FILE@ ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -ocode="" -print
*/ */
#include "__fc_builtin.h" #include "__fc_builtin.h"
#include "assert.h" #include "assert.h"
//#include "complex.h" //#include "complex.h"
......
/* run.config /* run.config
CMD: @frama-c-cmd@ @PTEST_OPTIONS@ COMMENT: dependency to FRAMA-C share directory is implicit
OPT: ../../../../install/default/share/frama-c/share/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -print MACRO: LIBC @FRAMAC_SHARE@/libc
OPT: @PTEST_FILE@ ../../../../install/default/share/frama-c/share/libc/string.h @PTEST_FILE@ -print CMD: @frama-c-cmd@ @PTEST_OPTIONS@
OPT: @PTEST_FILE@ @PTEST_FILE@ ../../../../install/default/share/frama-c/share/libc/string.h -print OPT: @LIBC@/string.h @PTEST_FILE@ @PTEST_FILE@ -print
OPT: @PTEST_FILE@ @LIBC@/string.h @PTEST_FILE@ -print
OPT: @PTEST_FILE@ @PTEST_FILE@ @LIBC@/string.h -print
*/ */
#include "string.h" #include "string.h"
#include "stdlib.h" #include "stdlib.h"
char * char *
strdup(const char *str) strdup(const char *str)
{ {
......
/* run.config /* run.config
OPT: -cpp-extra-args="-Ishare/libc" -print COMMENT: dependency to FRAMA-C share directory is implicit
OPT: -cpp-extra-args="-I@FRAMAC_SHARE@/libc" -print
*/ */
#include "__fc_define_off_t.h" #include "__fc_define_off_t.h"
off_t x = 0; off_t x = 0;
......
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