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

[tests] split tests/jcdb/jcdb.c in adding tests/jcdb/logic-pp-include.c

parent ff6d1756
No related branches found
No related tags found
No related merge requests found
/* run.config /* run.config
DEPS: compile_commands.json
COMMENT: parsing option are defined in the default json file "compile_commands.json"
OPT: -json-compilation-database @PTEST_DIR@ -print OPT: -json-compilation-database @PTEST_DIR@ -print
OPT: @PTEST_DIR@/jcdb2.c -json-compilation-database @PTEST_DIR@/with_arguments.json -print DEPS:
OPT: %{dep:@PTEST_DIR@/jcdb2.c} -json-compilation-database %{dep:@PTEST_DIR@/with_arguments.json} -print
MODULE: @PTEST_NAME@ MODULE: @PTEST_NAME@
OPT: -json-compilation-database @PTEST_DIR@/with_arguments.json -no-autoload-plugins OPT: -json-compilation-database %{dep:@PTEST_DIR@/with_arguments.json}
MODULE: MODULE:
EXECNOW: LOG list_files.res LOG list_files.err share/analysis-scripts/list_files.py @PTEST_DIR@/compile_commands_working.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err EXECNOW: LOG list_files.res LOG list_files.err %{bin:frama-c-script} list-files %{dep:@PTEST_DIR@/compile_commands_working.json} > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
EXECNOW: LOG logic-pp-include.res LOG logic-pp-include.err @frama-c@ -json-compilation-database @PTEST_DIR@/logic-pp-include @PTEST_DIR@/logic-pp-include/no-stdio.c -print > @PTEST_DIR@/result/logic-pp-include.res 2> @PTEST_DIR@/result/logic-pp-include.err
*/ */
#include <stdio.h> #include <stdio.h>
......
/* run.config
COMMENT: test related to a bugfix in the management of relative sub-directories:
DEPS: logic-pp-include/compile_commands.json
OPT: -json-compilation-database @PTEST_DIR@/logic-pp-include %{dep:@PTEST_DIR@/logic-pp-include/no-stdio.c} -print
*/
// compile_commands.json must have "-includestdio.h" and define ZERO /* run.config
OPT: -json-compilation-database %{dep:@PTEST_DIR@/no-stdio.json} -print
*/
// no-stdio.json must have "-includestdio.h" and define ZERO
//@ ensures \result == ZERO; //@ ensures \result == ZERO;
int main(){ int main(){
......
[kernel] Parsing tests/jcdb/logic-pp-include.c (with preprocessing)
[kernel] Parsing tests/jcdb/logic-pp-include/no-stdio.c (with preprocessing) [kernel] Parsing tests/jcdb/logic-pp-include/no-stdio.c (with preprocessing)
/* Generated by Frama-C */ /* Generated by Frama-C */
#include "errno.h" #include "errno.h"
......
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