diff --git a/bin/dune b/bin/dune new file mode 100644 index 0000000000000000000000000000000000000000..e38e8035b421dcf73dd7cdb9afe8e5438de2fa51 --- /dev/null +++ b/bin/dune @@ -0,0 +1,9 @@ +(install + (package frama-c) + (section bin) + (files + (frama-c-script as frama-c-script) + (frama-c-config as frama-c-config) + (local_export.sh as local_export.sh) + ) +) diff --git a/bin/frama-c-config b/bin/frama-c-config index be9eed99a62f14309d63061b1a2b55d1bc884f28..27af8373ccab00893ee9a302a1204d943a858720 100755 --- a/bin/frama-c-config +++ b/bin/frama-c-config @@ -24,4 +24,4 @@ . $(dirname $0)/local_export.sh -exec $BINDIR/fc-config "$@" +exec $BINDIR/frama-c -no-autoload-plugins "$@" diff --git a/dune b/dune index 66a430ca57cd17fe6d6aee55f54cd56539728f8b..745177cd8363402ae2620fc2851f9f5233e0531c 100644 --- a/dune +++ b/dune @@ -1 +1 @@ -(dirs src ptests tests share) +(dirs src ptests tests share bin) diff --git a/tests/fc_script/main.c b/tests/fc_script/main.c index 99e9a5a94e320b377ce9179da25d25cab2b6b3d9..97b7d281575192c385a17f7d477ea60496a20a21 100644 --- a/tests/fc_script/main.c +++ b/tests/fc_script/main.c @@ -1,12 +1,12 @@ /* run.config NOFRAMAC: testing frama-c-script, not frama-c itself - DEPS: for-find-fun2.c for-find-fun.c main2.c main3.c - EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err PTESTS_TESTING= frama-c-script make-template . < %{dep:make_template.input} > make_template.res 2> make_template.err - EXECNOW: LOG list_files.res LOG list_files.err frama-c-script list-files %{dep:list_files.json} > list_files.res 2> list_files.err - EXECNOW: LOG flamegraph.html LOG flamegraph.res LOG flamegraph.err NOGUI=1 frama-c-script flamegraph %{dep:flamegraph.txt} . > flamegraph.res 2> flamegraph.err && rm -f flamegraph.svg - EXECNOW: LOG find_fun1.res LOG find_fun1.err frama-c-script find-fun main2 . > find_fun1.res 2> find_fun1.err - EXECNOW: LOG find_fun2.res LOG find_fun2.err frama-c-script find-fun main3 . > find_fun2.res 2> find_fun2.err - EXECNOW: LOG find_fun3.res LOG find_fun3.err frama-c-script find-fun false_positive . > find_fun3.res 2> find_fun3.err + DEPS: for-find-fun2.c for-find-fun.c main.c main2.c main3.c + EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err PTESTS_TESTING= %{bin:frama-c-script} make-template . < %{dep:make_template.input} > make_template.res 2> make_template.err + EXECNOW: LOG list_files.res LOG list_files.err %{bin:frama-c-script} list-files %{dep:list_files.json} > list_files.res 2> list_files.err + EXECNOW: LOG flamegraph.html LOG flamegraph.res LOG flamegraph.err NOGUI=1 %{bin:frama-c-script} flamegraph %{dep:flamegraph.txt} . > flamegraph.res 2> flamegraph.err && rm -f flamegraph.svg + EXECNOW: LOG find_fun1.res LOG find_fun1.err %{bin:frama-c-script} find-fun main2 . > find_fun1.res 2> find_fun1.err + EXECNOW: LOG find_fun2.res LOG find_fun2.err %{bin:frama-c-script} find-fun main3 . > find_fun2.res 2> find_fun2.err + EXECNOW: LOG find_fun3.res LOG find_fun3.err %{bin:frama-c-script} find-fun false_positive . > find_fun3.res 2> find_fun3.err */ void main() { diff --git a/tests/fc_script/oracle/GNUmakefile b/tests/fc_script/oracle/GNUmakefile index e33adeea38d003482232cf4a137db198f89e7ee6..a824473331f8b9c665634043c86b81d55b10102a 100644 --- a/tests/fc_script/oracle/GNUmakefile +++ b/tests/fc_script/oracle/GNUmakefile @@ -19,9 +19,9 @@ CPPFLAGS += \ ## General flags FCFLAGS += \ - -json-compilation-database ../compile_commands.json \ + -json-compilation-database ./compile_commands.json \ -main eva_main \ - -add-symbolic-path=.:.. \ + -add-symbolic-path=.:. \ -kernel-warn-key annot:missing-spec=abort \ -kernel-warn-key typing:implicit-function-declaration=abort \ @@ -31,7 +31,7 @@ EVAFLAGS += \ ## GUI-only flags FCGUIFLAGS += \ - -add-symbolic-path=.:.. \ + -add-symbolic-path=.:. \ ## Analysis targets (suffixed with .eva) TARGETS = fc_script_main.eva @@ -39,11 +39,11 @@ TARGETS = fc_script_main.eva ### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites fc_script_main.parse: \ fc_stubs.c \ - ../for-find-fun.c \ - ../for-find-fun2.c \ - ../main.c \ - ../main2.c \ - ../main3.c \ + ./for-find-fun.c \ + ./for-find-fun2.c \ + ./main.c \ + ./main2.c \ + ./main3.c \ ### Epilogue. Do not modify this block. ####################################### include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk diff --git a/tests/fc_script/oracle/make_template.res b/tests/fc_script/oracle/make_template.res index eb6734b3ca4224a9a3b0f2b872a3d83b8317b4f6..fb1240c15cd993966a33449fdccbfa7ab72d65ba 100644 --- a/tests/fc_script/oracle/make_template.res +++ b/tests/fc_script/oracle/make_template.res @@ -1,15 +1,15 @@ -Preparing template: result/GNUmakefile +Preparing template: GNUmakefile Running ptests: setting up mock files... -warning: result/GNUmakefile already exists. Overwrite? [y/N] Main target name: Source files (default: **/*.c): The following sources were matched (relative to result): - ../for-find-fun.c - ../for-find-fun2.c - ../main.c # defines 'main' - ../main2.c - ../main3.c # defines 'main' +warning: GNUmakefile already exists. Overwrite? [y/N] Main target name: Source files (default: **/*.c): The following sources were matched (relative to .): + ./for-find-fun.c + ./for-find-fun2.c + ./main.c # defines 'main' + ./main2.c + ./main3.c # defines 'main' warning: 'main' seems to be defined multiple times. Is this ok? [Y/n] compile_commands.json exists, add option -json-compilation-database? [Y/n] Add stub for function main (only needed if it uses command-line arguments)? [y/N] Please define the architectural model (machdep) of the target machine. Known machdeps: x86_16 x86_32 x86_64 gcc_x86_16 gcc_x86_32 gcc_x86_64 ppc_32 msvc_x86_64 -Please enter the machdep [x86_32]: 'invalid_machdep' is not a standard machdep. Proceed anyway? [y/N]Please enter the machdep [x86_32]: warning: result/fc_stubs.c already exists. Overwrite? [y/N] Created stub for main function: result/fc_stubs.c -Template created: result/GNUmakefile +Please enter the machdep [x86_32]: 'invalid_machdep' is not a standard machdep. Proceed anyway? [y/N]Please enter the machdep [x86_32]: warning: fc_stubs.c already exists. Overwrite? [y/N] Created stub for main function: fc_stubs.c +Template created: GNUmakefile Running ptests: cleaning up after tests...