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

[tests] avoid warnings about unused files with option -load

parent 0d8e028c
No related branches found
No related tags found
No related merge requests found
Showing
with 19 additions and 32 deletions
/* run.config /* run.config
COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
CMD: @frama-c@ @PTEST_OPTIONS@
COMMENT: do not compare generated journals since they depend on current time COMMENT: do not compare generated journals since they depend on current time
PLUGIN: @EVA_PLUGINS@ PLUGIN: @EVA_PLUGINS@
EXECNOW: BIN control_journal.ml @frama-c@ @PTEST_FILE@ -journal-enable -eva -deps -out @EVA_OPTIONS@ -main f -journal-name @PTEST_RESULT@/control_journal.ml > @DEV_NULL@ 2> @DEV_NULL@ EXECNOW: BIN control_journal.ml @frama-c@ @PTEST_FILE@ -journal-enable -eva -deps -out @EVA_OPTIONS@ -main f -journal-name @PTEST_RESULT@/control_journal.ml > @DEV_NULL@ 2> @DEV_NULL@
......
/* run.config /* run.config
COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
CMD: @frama-c@ @PTEST_OPTIONS@
PLUGIN: @EVA_PLUGINS@ PLUGIN: @EVA_PLUGINS@
EXECNOW: BIN control_journal2.ml @frama-c@ -journal-enable -eva -deps -out -main f -journal-name @PTEST_RESULT@/control_journal2.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@ EXECNOW: BIN control_journal2.ml @frama-c@ -journal-enable -eva -deps -out -main f -journal-name @PTEST_RESULT@/control_journal2.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@
SCRIPT: @PTEST_RESULT@/control_journal2.ml SCRIPT: @PTEST_RESULT@/control_journal2.ml
......
/* run.config /* run.config
COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
CMD: @frama-c@ @PTEST_OPTIONS@
PLUGIN: @EVA_PLUGINS@ sparecode PLUGIN: @EVA_PLUGINS@ sparecode
MODULE: @PTEST_NAME@ MODULE: @PTEST_NAME@
EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name @PTEST_RESULT@/intra_journal.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@ EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name @PTEST_RESULT@/intra_journal.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@
......
...@@ -29,7 +29,6 @@ ...@@ -29,7 +29,6 @@
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
[from] Computing for function f [from] Computing for function f
[from] Done for function f [from] Done for function f
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[from] ====== DEPENDENCIES COMPUTED ====== [from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate: These dependencies hold at termination for the executions that terminate:
[from] Function f: [from] Function f:
......
...@@ -29,7 +29,6 @@ ...@@ -29,7 +29,6 @@
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
[from] Computing for function f [from] Computing for function f
[from] Done for function f [from] Done for function f
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[from] ====== DEPENDENCIES COMPUTED ====== [from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate: These dependencies hold at termination for the executions that terminate:
[from] Function f: [from] Function f:
...@@ -57,9 +56,7 @@ ...@@ -57,9 +56,7 @@
1 function analyzed (out of 1): 100% coverage. 1 function analyzed (out of 1): 100% coverage.
In this function, 9 statements reached (out of 12): 75% coverage. In this function, 9 statements reached (out of 12): 75% coverage.
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis: No errors or warnings raised during the analysis.
by the Eva analyzer: 0 errors 0 warnings
by the Frama-C kernel: 0 errors 1 warning
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
1 alarm generated by the analysis: 1 alarm generated by the analysis:
1 integer overflow 1 integer overflow
......
1 1
2 2
3 3
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
1 1
2 2
3 3
...@@ -63,7 +63,6 @@ ...@@ -63,7 +63,6 @@
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
[from] Computing for function f [from] Computing for function f
[from] Done for function f [from] Done for function f
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[from] ====== DEPENDENCIES COMPUTED ====== [from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate: These dependencies hold at termination for the executions that terminate:
[from] Function f: [from] Function f:
......
...@@ -114,4 +114,3 @@ ...@@ -114,4 +114,3 @@
[pdg] done for function stop [pdg] done for function stop
[sparecode] remove unused global declarations... [sparecode] remove unused global declarations...
[sparecode] result in new project 'default without sparecode'. [sparecode] result in new project 'default without sparecode'.
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
/* run.config /* run.config
COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
CMD: @frama-c@ @PTEST_OPTIONS@
PLUGIN: PLUGIN:
MODULE: @PTEST_NAME@ MODULE: @PTEST_NAME@
EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav @frama-c@ @PTEST_FILE@ -main f -save @PTEST_RESULT@/@PTEST_NAME@.sav > @PTEST_RESULT@/@PTEST_NAME@_sav.res 2> @PTEST_RESULT@/@PTEST_NAME@_sav.err EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav @frama-c@ @PTEST_FILE@ -main f -save @PTEST_RESULT@/@PTEST_NAME@.sav > @PTEST_RESULT@/@PTEST_NAME@_sav.res 2> @PTEST_RESULT@/@PTEST_NAME@_sav.err
......
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
/* Generated by Frama-C */ /* Generated by Frama-C */
int f(void) int f(void)
{ {
......
...@@ -4,7 +4,6 @@ ...@@ -4,7 +4,6 @@
[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored. [kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored. [kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
[kernel] Warning: 15 states in saved file ignored. They are invalid in this Frama-C configuration. [kernel] Warning: 15 states in saved file ignored. They are invalid in this Frama-C configuration.
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
/* Generated by Frama-C */ /* Generated by Frama-C */
int f(void) int f(void)
{ {
......
/* run.config /* run.config
COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
CMD: @frama-c@ @PTEST_OPTIONS@
MODULE: @PTEST_NAME@ MODULE: @PTEST_NAME@
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @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@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
MODULE: MODULE:
......
/* run.config /* run.config
COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
CMD: @frama-c@ @PTEST_OPTIONS@
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -save @PTEST_NAME@.sav -machdep x86_32 -eva @EVA_OPTIONS@ @PTEST_FILE@ > @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@ -save @PTEST_NAME@.sav -machdep x86_32 -eva @EVA_OPTIONS@ @PTEST_FILE@ > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -out -input -deps" STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -out -input -deps"
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@" STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@"
......
/* run.config /* run.config
COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
CMD: @frama-c@ @PTEST_OPTIONS@
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ @PTEST_FILE@ -out -calldeps -eva-show-progress -main main1 -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@ @PTEST_FILE@ -out -calldeps -eva-show-progress -main main1 -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -main main2 -then -main main3" STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -main main2 -then -main main3"
*/ */
......
/* run.config /* run.config
COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
CMD: @frama-c@ @PTEST_OPTIONS@
MODULE: deps_A MODULE: deps_A
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @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@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@ -out -input -deps " STDOPT: +"-load %{dep:@PTEST_NAME@.sav} -eva @EVA_OPTIONS@ -out -input -deps "
......
/* run.config /* run.config
COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
CMD: @frama-c@ @PTEST_OPTIONS@
EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -quiet -eva @EVA_OPTIONS@ -save @PTEST_NAME@.sav @PTEST_FILE@ > @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@ -quiet -eva @EVA_OPTIONS@ -save @PTEST_NAME@.sav @PTEST_FILE@ > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
STDOPT: +"-quiet -load %{dep:@PTEST_NAME@.sav}" STDOPT: +"-quiet -load %{dep:@PTEST_NAME@.sav}"
STDOPT: +"-load %{dep:@PTEST_NAME@.sav}" STDOPT: +"-load %{dep:@PTEST_NAME@.sav}"
......
[kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration. [kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
/* Generated by Frama-C */ /* Generated by Frama-C */
int main(void) int main(void)
{ {
......
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
unknown (tried by Test) unknown (tried by Test)
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