Skip to content
Snippets Groups Projects
Commit 7f55a56f authored by François Bobot's avatar François Bobot
Browse files

Fix some oracles

parent ea074b22
No related branches found
No related tags found
No related merge requests found
Showing
with 83 additions and 32 deletions
/* run.config*
PLUGIN: report
CMXS: big_local_array_script
OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report
OPT: @EVA_OPTIONS@ -load-module big_local_array_script -then-on prj -print -report
......
/* run.config
PLUGIN: sparecode
OPT: -journal-disable -print
OPT: -journal-disable -semantic-const-folding @EVA_OPTIONS@
OPT: -journal-disable -sparecode-analysis @EVA_OPTIONS@
......
PLUGIN: impact
OPT: -journal-disable -impact-print @EVA_OPTIONS@
/* run.config
PLUGIN: sparecode
CMXS: @PTEST_NAME@
STDOPT: +"-load-module %{dep:@PTEST_NAME@.cmxs}"
*/
......
/* run.config
STDOPT: +"@PTEST_DIR@/aggressive_merging_2.i -aggressive-merging"
STDOPT: +"%{dep:aggressive_merging_2.i} -aggressive-merging"
*/
static inline void f(void) {
return;
......
/* run.config
DEPS: bts0323.h
STDOPT: +"bts0323-2.c"
*/
#include "bts0323.h"
......
/* run.config
DEPS: enum.h
STDOPT: +"enum2.c"
*/
......
/* run.config
OPT: @PTEST_DIR@/@PTEST_NAME@_1.i @PTEST_DIR@/@PTEST_NAME@_2.i -eva @EVA_CONFIG@
OPT: @PTEST_DIR@/@PTEST_NAME@_2.i @PTEST_DIR@/@PTEST_NAME@_1.i -eva @EVA_CONFIG@
OPT: %{dep:@PTEST_NAME@_1.i} %{dep:@PTEST_NAME@_2.i} -eva @EVA_CONFIG@
OPT: %{dep:@PTEST_NAME@_2.i} %{dep:@PTEST_NAME@_1.i} -eva @EVA_CONFIG@
*/
extern int a[] ;
......
/* run.config
CMXS: @PTEST_NAME@
OPT: -print -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} @PTEST_DIR@/@PTEST_NAME@_1.i
MODULE: @PTEST_NAME@.cmxs
OPT: -print %{dep:@PTEST_NAME@_1.i}
*/
void f(int x);
......
/* run.config
STDOPT: +"@PTEST_DIR@/inline_def_2.i"
STDOPT: +"%{dep:inline_def_2.i}"
*/
// inline definition can be used in this translation unit, but does not
......
/* run.config
STDOPT: +"@PTEST_DIR@/inline_def_bad_2.i"
STDOPT: +"%{dep:inline_def_bad_2.i}"
*/
extern inline f() { return 1; }
......
/* run.config
OPT: @PTEST_DIR@/merge_inline_2.c -aggressive-merging -print
OPT: %{dep:merge_inline_2.c} -aggressive-merging -print
*/
/* Test that we rename properly inlines even if they have prototypes and
......
/* run.config
OPT: -cpp-extra-args="-I @PTEST_DIR@" @PTEST_DIR@/@PTEST_NAME@_2.c @PTEST_DIR@/@PTEST_NAME@_3.c -print
OPT: -cpp-extra-args="-I @PTEST_DIR@" @PTEST_DIR@/@PTEST_NAME@_2.c @PTEST_DIR@/@PTEST_NAME@_3.c -print -kernel-warn-key="linker:drop-conflicting-unused=inactive"
DEPS: merge_union.h
OPT: -cpp-extra-args="-I @PTEST_DIR@" %{dep:@PTEST_NAME@_2.c} %{dep:@PTEST_NAME@_3.c} -print
OPT: -cpp-extra-args="-I @PTEST_DIR@" %{dep:@PTEST_NAME@_2.c} %{dep:@PTEST_NAME@_3.c} -print -kernel-warn-key="linker:drop-conflicting-unused=inactive"
*/
#include "merge_union.h"
......
/* run.config
DEPS: merge_unused.h
OPT: -cpp-extra-args="-I@PTEST_DIR@" @PTEST_DIR@/@PTEST_NAME@_2.c -print
OPT: -cpp-extra-args="-I@PTEST_DIR@" %{dep:@PTEST_NAME@_2.c} -print
*/
#pragma pack(1)
......
/* run.config
OPT: @PTEST_DIR@/@PTEST_NAME@_aux.i -print
OPT: %{dep:@PTEST_NAME@_aux.i} -print
*/
int open (const char* file, int flags, int mode) {
return -1;
......
/* run.config
OPT: string.h @PTEST_FILE@ @PTEST_FILE@ -cpp-extra-args="-Ishare/libc" -print
OPT: @PTEST_FILE@ string.h @PTEST_FILE@ -cpp-extra-args="-Ishare/libc" -print
OPT: @PTEST_FILE@ @PTEST_FILE@ string.h -cpp-extra-args="-Ishare/libc" -print
DEPS: ../../../share/libc/string.h
OPT: ../../../share/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -print
OPT: @PTEST_FILE@ ../../../share/libc/string.h @PTEST_FILE@ -print
OPT: @PTEST_FILE@ @PTEST_FILE@ ../../../share/libc/string.h -print
*/
#include "string.h"
......
[kernel] User Error: source file 'aggressive_merging_2.i' does not exist
[kernel] Frama-C aborted: invalid user input.
[kernel] Parsing aggressive_merging_1.i (no preprocessing)
[kernel] Parsing aggressive_merging_2.i (no preprocessing)
/* Generated by Frama-C */
__inline static void f(void)
{
return;
}
void foo(void)
{
f();
return;
}
void bar(void)
{
f();
return;
}
[kernel] Parsing anon_enum_libc.c (with preprocessing)
[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -I tmp/anon_enum_libc.c7cac46.i' '/home/bobot/Sources/frama-c/_build/default/result/anon_enum_libc.c'
[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -I tests/syntax -dD -nostdinc -m32 -o '/tmp/anon_enum_libc.c98bd8a.i' '/home/bobot/Sources/frama-c/_build/default/tests/syntax/result/anon_enum_libc.c'
See chapter "Preparing the Sources" in the Frama-C user manual for more details.
[kernel] User Error: stopping on file "anon_enum_libc.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
......
[kernel] Parsing assert_location.c (with preprocessing)
[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/assert_location.c3861fd.i' '/home/bobot/Sources/frama-c/_build/default/result/assert_location.c'
this is possibly due to missing preprocessor flags;
consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
See chapter "Preparing the Sources" in the Frama-C user manual for more details.
[kernel] User Error: stopping on file "assert_location.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
/* Generated by Frama-C */
#include "assert.h"
void h(void)
{
__FC_assert("I\'m in assert_location.h" != (char const *)0,
"assert_location.h",4,"\"I\'m in assert_location.h\"");
return;
}
void c(void)
{
__FC_assert("I\'m in assert_location.c" != (char const *)0,
"assert_location.c",9,"\"I\'m in assert_location.c\"");
return;
}
[kernel] Parsing bts0323.c (with preprocessing)
[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/bts0323.c61bb8a.i' '/home/bobot/Sources/frama-c/_build/default/result/bts0323.c'
this is possibly due to missing preprocessor flags;
consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
See chapter "Preparing the Sources" in the Frama-C user manual for more details.
[kernel] User Error: stopping on file "bts0323.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
[kernel] Parsing bts0323-2.c (with preprocessing)
/* Generated by Frama-C */
int x;
void g(void);
void f(void)
{
x = 0;
return;
}
int x = 1;
/*@ ensures x ≢ 0; */
void g(void)
{
x = 2;
return;
}
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