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

[Ptests] homogeneous workaround about acces to frama-c share"

parent 15e4c797
No related branches found
No related tags found
No related merge requests found
/* run.config
COMMENT: dependency to FRAMA-C share directory is implicit
DEPS: jcdb2.c with_arguments.json compile_commands.json file_without_main.c
CMXS: @PTEST_NAME@
OPT: -json-compilation-database ./ -print
......@@ -6,6 +7,9 @@ OPT: jcdb2.c -json-compilation-database with_arguments.json -print
OPT: -json-compilation-database with_arguments.json -load-module %{dep:@PTEST_NAME@.cmxs}
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
*/
#include <stdio.h>
#ifdef TOUNDEF
......
/* run.config*
COMMENT: dependency to FRAMA-C share directory is implicit
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
*/
#include "string.h"
void main() {
......
/* run.config*
COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
DEPS: ../../../share/libc/__fc_runtime.c
COMMENT: dependency to FRAMA-C share directory is implicit
CMD: gcc @OPTIONS@
OPT: -D__FC_MACHDEP_X86_64 ../../../share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null @PTEST_FILE@
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@
*/
int main() {
......
/* run.config
DEPS: ../../../share/libc/string.c
STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-include../../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"
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"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
......
/* run.config
DEPS: ../../../share/libc/string.c
STDOPT: #"-cpp-extra-args=-include../../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"
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"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
......
/* run.config
DEPS: ../../../share/libc/string.c
STDOPT: #"-cpp-extra-args=-include../../share/libc/string.c -eva-slevel-function strstr:30 -eva-no-skip-stdlib-specs"
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"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
......
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