diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 4ed528781c7d98bf2187989644af7d3c889a60e8..274977fc09e7e2d98140faff8d5c314b11dd03bf 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -1142,7 +1142,7 @@ let command_string ~result_fmt ~oracle_fmt command =
"(rule\n \
(targets %S %S %a)\n \
(deps %a %S (package frama-c)%a)\n \
- (action (with-stderr-to %S (with-stdout-to %S %s(with-accepted-exit-codes (or 0 1 4 125) (system %S))%s)))\n\
+ (action (with-stderr-to %S (with-stdout-to %S %s(with-accepted-exit-codes (or 0 1 4 125 127) (system %S))%s)))\n\
)@."
errlog
res
@@ -1159,16 +1159,13 @@ let command_string ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(rule\n \
(alias %S)\n \
- (deps %a %S (package frama-c)%t)\n \
+ (deps %a %S (package frama-c)%a (universe))\n \
(action (system %S))\n\
)\n"
command.file
print_list deps
(get_ptest_file command)
- (fun fmt ->
- List.iter
- (fun d -> Format.fprintf fmt " (package %S)" ("frama-c-"^d))
- command.plugins)
+ Fmt.(list (package_as_deps (quote plugin_as_package))) command.plugins
command_string;
let oracle_prefix = oracle_prefix command in
diff --git a/tests/saveload/deps.i b/tests/saveload/deps.i
index a9290b7c510e5d3d4aa25c834eb7828972407f2b..fa94aacd688dc15b07cdb13b7fa9011aef885519 100644
--- a/tests/saveload/deps.i
+++ b/tests/saveload/deps.i
@@ -1,11 +1,11 @@
/* run.config
CMXS: deps_A deps_B deps_C deps_D deps_E
- EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -load-module %{dep:deps_A.cmxs} -eva @EVA_OPTIONS@ -out -input -deps ./deps.i -save ./result/deps.sav > ./result/deps_sav.res 2> ./result/deps_sav.err
- STDOPT: +"-load-module ./deps_A -load ./result/deps.sav -eva @EVA_OPTIONS@ -out -input -deps "
- STDOPT: +"-load-module ./deps_B -load ./result/deps.sav -out -input -deps "
- STDOPT: +"-load-module ./deps_C -load ./result/deps.sav -out -input -deps "
- STDOPT: +"-load-module ./deps_D -load ./result/deps.sav -out -input -deps "
- STDOPT: +"-load-module ./deps_E -load ./result/deps.sav -out -input -deps "
+ EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -load-module %{dep:deps_A.cmxs} -eva @EVA_OPTIONS@ -out -input -deps ./deps.i -save deps.sav > ./result/deps_sav.res 2> ./result/deps_sav.err
+ STDOPT: +"-load-module %{deps:deps_A} -load ./result/deps.sav -eva @EVA_OPTIONS@ -out -input -deps "
+ STDOPT: +"-load-module %{deps:deps_B} -load ./result/deps.sav -out -input -deps "
+ STDOPT: +"-load-module %{deps:deps_C} -load ./result/deps.sav -out -input -deps "
+ STDOPT: +"-load-module %{deps:deps_D} -load ./result/deps.sav -out -input -deps "
+ STDOPT: +"-load-module %{deps:deps_E} -load ./result/deps.sav -out -input -deps "
*/
int main() {
diff --git a/tests/sparecode/test_config b/tests/sparecode/test_config
index a9330dd48d062e0b27b9bb948a88af6f4250c17a..a8bbd0d9d8faa5a8f89abeb1dbe9faf40a92c499 100644
--- a/tests/sparecode/test_config
+++ b/tests/sparecode/test_config
@@ -1 +1,2 @@
+PLUGIN: sparecode slicing
OPT: -journal-disable @EVA_OPTIONS@ -sparecode-debug 1
diff --git a/tests/spec/anon_arg_2.i b/tests/spec/anon_arg_2.i
index 9e3ef0cb8d077d0db7b384d04bbb470a969ddda2..80197a9b0f7a8f0442765c3be2a4027286a339f0 100644
--- a/tests/spec/anon_arg_2.i
+++ b/tests/spec/anon_arg_2.i
@@ -1,5 +1,5 @@
/* run.config*
-STDOPT: #"@PTEST_DIR@/anon_arg_1.i @PTEST_FILE@"
+STDOPT: #"%{dep:anon_arg_1.i} @PTEST_FILE@"
*/
/*@ requires \valid(p);
diff --git a/tests/spec/axiom_included.c b/tests/spec/axiom_included.c
index 4b30e4e5337afb1d2aa99c35af474bf6cde53b12..2b3bb5dece35ac1aa9e3a351743d040cbca306c2 100644
--- a/tests/spec/axiom_included.c
+++ b/tests/spec/axiom_included.c
@@ -1,5 +1,6 @@
/* run.config
- STDOPT: +"axiom_included_1.c"
+ DEPS: axiom_included.h
+ STDOPT: +"%{dep:axiom_included_1.c}"
*/
#include "axiom_included.h"
diff --git a/tests/spec/bts0578.i b/tests/spec/bts0578.i
index 2e1bf64bb4c52accb79a6adf81d4e8a16a2f3c22..4ecccedf4d073f6320b8d7d2f2b96277498d535a 100644
--- a/tests/spec/bts0578.i
+++ b/tests/spec/bts0578.i
@@ -1,6 +1,6 @@
/* run.config
- CMXS: @PTEST_NAME@
- OPT: -print -load-module ./@PTEST_DIR@/@PTEST_NAME@
+ MODULE: @PTEST_NAME@.cmxs
+ OPT: -print
*/
/*@ behavior foo: ensures \true; */
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 66c93e7d3a8fb3ec726efdd2efa913a36d46b1ba..8f06f2a0a58ec2606ece2a9199c322cca09e20bb 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: wp
OPT: -wp -wp-prover qed -wp-msg-key shell
OPT: -eva -eva-use-spec f
OPT: -print
diff --git a/tests/spec/lib.c b/tests/spec/lib.c
index 8a1d566beafbbde7c3b41ff08a7f0546b83ab707..54cd5a85a142c9c2d669b6e74d8f2646793ade8a 100644
--- a/tests/spec/lib.c
+++ b/tests/spec/lib.c
@@ -1,5 +1,5 @@
/* run.config
- OPT: -cpp-extra-args="-Itests/spec" -cpp-extra-args="-include lib.h" -print -journal-disable
+ OPT: -cpp-extra-args="-include %{dep:lib.h}" -print -journal-disable
*/
/*@ ensures f((int)0) == (int)0; */
diff --git a/tests/spec/merge_1.i b/tests/spec/merge_1.i
index ac6d0792236fef46546b1c3bcbde0c4ca02b1b48..409e6b7683fe7a141a9f350dc8f6ed08ef9a4675 100644
--- a/tests/spec/merge_1.i
+++ b/tests/spec/merge_1.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"merge_2.i"
+ STDOPT: +"%{dep:merge_2.i}"
*/
/*@ requires \valid(s);
@ assigns \nothing;
diff --git a/tests/spec/merge_bts938.c b/tests/spec/merge_bts938.c
index 8ee32add093c45936b1b21e50cde92727ca5811a..efd3962eb5d4cdca50a580cb13595983e6d94555 100644
--- a/tests/spec/merge_bts938.c
+++ b/tests/spec/merge_bts938.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"merge_bts938_1.c"
+ STDOPT: +"%{deps:merge_bts938_1.c}"
*/
#include "merge_bts938.h"
diff --git a/tests/spec/merge_different_assigns.i b/tests/spec/merge_different_assigns.i
index 63fea95aa5b4c1f1c6f6bc810151731db8eae070..b9166ff75bc684374fcd738aecb23c3131012785 100644
--- a/tests/spec/merge_different_assigns.i
+++ b/tests/spec/merge_different_assigns.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"merge_different_assigns_bis.i"
+ STDOPT: +"%{dep:merge_different_assigns_bis.i}"
*/
int x, z, t, u, v, w;
diff --git a/tests/spec/multi_axiomatic_1.i b/tests/spec/multi_axiomatic_1.i
index cfe295495cc769ee756d766794a22dc1902790ea..8430c9c2bbfed11fc674ca4998a0db5a6e8b8a84 100644
--- a/tests/spec/multi_axiomatic_1.i
+++ b/tests/spec/multi_axiomatic_1.i
@@ -1,5 +1,5 @@
/* run.config
-OPT: @PTEST_DIR@/multi_axiomatic_2.i -print
+OPT: %{dep:multi_axiomatic_2.i} -print
*/
/*@
diff --git a/tests/spec/oracle/acsl_basic_allocator.res.oracle b/tests/spec/oracle/acsl_basic_allocator.res.oracle
index cf8150d4acbdae0f179150964f4eda50b1216eb8..6d2b0811ba69bc10fbfb29d0b59134a6fde783f1 100644
--- a/tests/spec/oracle/acsl_basic_allocator.res.oracle
+++ b/tests/spec/oracle/acsl_basic_allocator.res.oracle
@@ -1,8 +1,99 @@
[kernel] Parsing acsl_basic_allocator.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/acsl_basic_allocator.cefdc9d.i' '/home/bobot/Sources/frama-c/_build/default/result/acsl_basic_allocator.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 "acsl_basic_allocator.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+/* Generated by Frama-C */
+#include "stdlib.h"
+enum _bool {
+ false = 0,
+ true = 1
+};
+typedef enum _bool bool;
+struct _memory_block {
+ size_t size ;
+ bool free ;
+ char *data ;
+};
+typedef struct _memory_block memory_block;
+struct _memory_block_list {
+ memory_block *block ;
+ struct _memory_block_list *next ;
+};
+typedef struct _memory_block_list memory_block_list;
+typedef memory_block_list *memory_pool;
+/*@
+type invariant inv_memory_block(memory_block mb) =
+ 0 < mb.size ∧ \offset(mb.data) ≡ 0 ∧
+ \block_length(mb.data) ≡ mb.size;
+ */
+/*@
+predicate used_memory_block{L}(memory_block mb) =
+ mb.free ≡ false ∧ inv_memory_block(mb);
+ */
+/*@
+predicate freed_memory_block{L}(memory_block mb) =
+ mb.free ≡ true ∧ inv_memory_block(mb);
+ */
+/*@
+predicate valid_memory_block{L}(memory_block *mb) =
+ \valid(mb) ∧ inv_memory_block(*mb);
+ */
+/*@
+predicate valid_used_memory_block{L}(memory_block *mb) =
+ \valid(mb) ∧ used_memory_block(*mb);
+ */
+/*@
+predicate valid_freed_memory_block{L}(memory_block *mb) =
+ \valid(mb) ∧ freed_memory_block(*mb);
+ */
+/*@
+predicate valid_memory_block_list{L}(memory_block_list *mbl) =
+ \valid(mbl) ∧ valid_memory_block(mbl->block) ∧
+ (mbl->next ≡ \null ∨ valid_memory_block_list(mbl->next));
+ */
+/*@
+predicate valid_memory_pool{L}(memory_pool *mp) =
+ \valid(mp) ∧ valid_memory_block_list(*mp);
+
+*/
+/*@ requires valid_memory_pool(arena) ∧ 0 < s;
+ ensures valid_used_memory_block(\result);
+ */
+memory_block *memory_alloc(memory_pool *arena, size_t s)
+{
+ memory_block *__retres;
+ memory_block *mb;
+ size_t mb_size;
+ char *mb_data;
+ memory_block_list *mbl = *arena;
+ while (mbl != (memory_block_list *)0) {
+ mb = mbl->block;
+ if (mb->free)
+ if (s <= mb->size) {
+ mb->free = false;
+ __retres = mb;
+ goto return_label;
+ }
+ mbl = mbl->next;
+ }
+ if ((size_t)1000 < s) mb_size = s; else mb_size = (unsigned int)1000;
+ mb_data = (char *)malloc(mb_size);
+ mb = (memory_block *)malloc(sizeof(memory_block));
+ mb->size = mb_size;
+ mb->free = false;
+ mb->data = mb_data;
+ mbl = (memory_block_list *)malloc(sizeof(memory_block_list));
+ mbl->block = mb;
+ mbl->next = *arena;
+ *arena = mbl;
+ __retres = mb;
+ return_label: return __retres;
+}
+
+/*@ requires valid_memory_pool(arena) ∧ valid_used_memory_block(block);
+ ensures valid_freed_memory_block(\old(block));
+ */
+void memory_free(memory_pool *arena, memory_block *block)
+{
+ block->free = true;
+ return;
+}
+
+
diff --git a/tests/spec/oracle/annot_decl_bts1009.res.oracle b/tests/spec/oracle/annot_decl_bts1009.res.oracle
index 6c592eecabf7ec22b4f756d23888026f2335da8f..24b7d528817faf8c506b1b0619b23082306e79d8 100644
--- a/tests/spec/oracle/annot_decl_bts1009.res.oracle
+++ b/tests/spec/oracle/annot_decl_bts1009.res.oracle
@@ -1,13 +1,5 @@
-<<<<<<< HEAD
[kernel] Parsing annot_decl_bts1009.i (no preprocessing)
-[kernel:annot-error] Warning:
-||||||| 362083a770
-[kernel] Parsing tests/spec/annot_decl_bts1009.i (no preprocessing)
-[kernel:annot-error] Warning:
-=======
-[kernel] Parsing tests/spec/annot_decl_bts1009.i (no preprocessing)
-[kernel:annot-error] tests/spec/annot_decl_bts1009.i:5: Warning:
->>>>>>> origin/master
+[kernel:annot-error] annot_decl_bts1009.i:5: Warning:
Statement contract and ACSL pragmas over a local definition are not implemented. Ignoring annotation
/* Generated by Frama-C */
void f(void)
diff --git a/tests/spec/oracle/anon_arg_2.res.oracle b/tests/spec/oracle/anon_arg_2.res.oracle
index d9ebdefad9432ef70060ae71dc578f025ebdfe25..4dac36af6cc13f92514ec30a789f66e576079ef8 100644
--- a/tests/spec/oracle/anon_arg_2.res.oracle
+++ b/tests/spec/oracle/anon_arg_2.res.oracle
@@ -1,2 +1,19 @@
-[kernel] User Error: source file 'anon_arg_1.i' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing anon_arg_1.i (no preprocessing)
+[kernel] Parsing anon_arg_2.i (no preprocessing)
+[kernel] anon_arg_1.i:7: Warning: found two contracts. Merging them
+/* Generated by Frama-C */
+/*@ requires \valid(p);
+ ensures \result ≡ \old(x) ∧ *\old(p) ≡ \old(x);
+ assigns *p;
+ assigns *p \from x;
+ */
+int f(int *p, int x);
+
+/*@ requires \valid(p);
+ ensures \result ≡ \old(x);
+ ensures *\old(p) ≡ \result;
+ assigns *p;
+ */
+int g(int *p, int x);
+
+
diff --git a/tests/spec/oracle/array_typedef.res.oracle b/tests/spec/oracle/array_typedef.res.oracle
index 585ed5bea148de32867ccbf8c2c389a90a8a631e..f9f255b9bffd819202ec7c9e7897735d742b7568 100644
--- a/tests/spec/oracle/array_typedef.res.oracle
+++ b/tests/spec/oracle/array_typedef.res.oracle
@@ -24,7 +24,8 @@
[eva] computing for function send_addr <- send_msg <- main.
Called from array_typedef.c:15.
[eva] using specification for function send_addr
-[eva] array_typedef.c:12: Warning: no \from part for clause 'assigns \empty;'
+[eva] array_typedef.c:12: Warning:
+ no \from part for clause 'assigns \empty;'
[eva] Done for function send_addr
[eva] Recording results for send_msg
[eva] Done for function send_msg
diff --git a/tests/spec/oracle/assignable_location.res.oracle b/tests/spec/oracle/assignable_location.res.oracle
index 43aec8f2843d2a74125606458a2ab449ea22c65a..db7ee46c1317afa32bd2542d3f555d3aaf6383dd 100644
--- a/tests/spec/oracle/assignable_location.res.oracle
+++ b/tests/spec/oracle/assignable_location.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing assignable_location.i (no preprocessing)
-[kernel:annot-error] assignable_location.i:36: Warning: unexpected token ';'
+[kernel:annot-error] assignable_location.i:36: Warning:
+ unexpected token ';'
[kernel:annot-error] assignable_location.i:28: Warning:
not an addressable left value: \result. Ignoring logic specification of function annotations_to_reject
[kernel:annot-error] assignable_location.i:30: Warning:
diff --git a/tests/spec/oracle/axiom_included.res.oracle b/tests/spec/oracle/axiom_included.res.oracle
index b79a2467ca2c452e50b6a307f7431d54eec3fefd..a0b318d9f592cfc8285decb78478627bfd3c538f 100644
--- a/tests/spec/oracle/axiom_included.res.oracle
+++ b/tests/spec/oracle/axiom_included.res.oracle
@@ -1,8 +1,9 @@
[kernel] Parsing axiom_included.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/axiom_included.c474bb9.i' '/home/bobot/Sources/frama-c/_build/default/result/axiom_included.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 "axiom_included.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing axiom_included_1.c (with preprocessing)
+/* Generated by Frama-C */
+/*@ axiomatic foo {
+ axiom foo: \true;
+
+ }
+ */
+
diff --git a/tests/spec/oracle/behavior_assert.0.res.oracle b/tests/spec/oracle/behavior_assert.0.res.oracle
index fe15f248e830cb27cb88f91d292476f9a88420e0..a909a19c510601910ec2594b53fa50727fddca06 100644
--- a/tests/spec/oracle/behavior_assert.0.res.oracle
+++ b/tests/spec/oracle/behavior_assert.0.res.oracle
@@ -8,7 +8,8 @@
c ∈ [--..--]
[eva] computing for function f <- main.
Called from behavior_assert.c:90.
-[eva:alarm] behavior_assert.c:14: Warning: assertion got status invalid.
+[eva:alarm] behavior_assert.c:14: Warning:
+ assertion got status invalid.
[eva] behavior_assert.c:16: assertion got status valid.
[eva] Recording results for f
[eva] Done for function f
@@ -32,7 +33,8 @@
Called from behavior_assert.c:52.
[eva] Recording results for abs
[eva] Done for function abs
-[eva:alarm] behavior_assert.c:55: Warning: assertion got status unknown.
+[eva:alarm] behavior_assert.c:55: Warning:
+ assertion got status unknown.
[eva] behavior_assert.c:45:
function h1, behavior not_null: postcondition got status valid.
[eva] Recording results for h1
@@ -43,7 +45,8 @@
[eva] computing for function k <- main.
Called from behavior_assert.c:93.
[eva] behavior_assert.c:85: assertion got status valid.
-[eva:alarm] behavior_assert.c:86: Warning: assertion got status invalid.
+[eva:alarm] behavior_assert.c:86: Warning:
+ assertion got status invalid.
[eva] Recording results for k
[eva] Done for function k
[eva] Recording results for main
diff --git a/tests/spec/oracle/behavior_assert.1.res.oracle b/tests/spec/oracle/behavior_assert.1.res.oracle
index 13875b4928195780d81e13492ab3b780475cf103..e206e4995a9bf2b7ec08d73dd1da716fd1d02e0e 100644
--- a/tests/spec/oracle/behavior_assert.1.res.oracle
+++ b/tests/spec/oracle/behavior_assert.1.res.oracle
@@ -32,7 +32,8 @@
Called from behavior_assert.c:52.
[eva] Recording results for abs
[eva] Done for function abs
-[eva:alarm] behavior_assert.c:55: Warning: assertion got status unknown.
+[eva:alarm] behavior_assert.c:55: Warning:
+ assertion got status unknown.
[eva] behavior_assert.c:45:
function h1, behavior not_null: postcondition got status valid.
[eva] Recording results for h1
diff --git a/tests/spec/oracle/clash_double_file_bts1598.res.oracle b/tests/spec/oracle/clash_double_file_bts1598.res.oracle
index 19ba21bf7c8a1977344f466ea3618ae2de4535a1..93fcee65eebc96267259b2dad61d5bf3884535e2 100644
--- a/tests/spec/oracle/clash_double_file_bts1598.res.oracle
+++ b/tests/spec/oracle/clash_double_file_bts1598.res.oracle
@@ -19,7 +19,7 @@
#include "wchar.h"
[kernel] Parsing clash_double_file_bts1598.c (with preprocessing)
-[kernel] Parsing foo.c (with preprocessing)
+[kernel] Parsing result/foo.c (with preprocessing)
/* Generated by Frama-C */
#include "__fc_builtin.h"
#include "assert.h"
diff --git a/tests/spec/oracle/doxygen.res.oracle b/tests/spec/oracle/doxygen.res.oracle
index 80866aac793c04a6e8611e18628806f13f1f6534..5a7807914f0a4e1254d12bce95df5323e7b2e5c9 100644
--- a/tests/spec/oracle/doxygen.res.oracle
+++ b/tests/spec/oracle/doxygen.res.oracle
@@ -23,57 +23,20 @@ void main();
/* Generated by Frama-C */
/* run.config
OPT: -keep-comments -print -then -pp-annot
-<<<<<<< HEAD
- */
-/* run.config
- OPT: -keep-comments -print -then -pp-annot
- */
-/* @{ */
-/* @{ */
-/* @{ Bla */
-/* @{ Bla */
-/* @{ */
-/* @{ */
-/* @{ Blu */
-/* @{ Blu */
-||||||| 362083a770
- */
-/* @{ */
-/* @{ Bla */
-/* @{ */
-/* @{ Blu */
-=======
*/
//@{
//@{ Bla
//@{
//@{ Blu
->>>>>>> origin/master
void doxygen_group(void)
{
return;
}
-<<<<<<< HEAD
-/* @} Bli */
-/* @} Bli */
-/* @} */
-/* @} */
-/* @} */
-/* @} */
-/* @} Bly */
-/* @} Bly */
-||||||| 362083a770
-/* @} Bli */
-/* @} */
-/* @} */
-/* @} Bly */
-=======
//@} Bli
//@}
//@}
//@} Bly
->>>>>>> origin/master
void main();
diff --git a/tests/spec/oracle/error_msg.res.oracle b/tests/spec/oracle/error_msg.res.oracle
index e973fed7c597f2a83442ffed9c462d0d08a8f1c2..246a6346f7574e00fdb42bbdd5e48c48728b20df 100644
--- a/tests/spec/oracle/error_msg.res.oracle
+++ b/tests/spec/oracle/error_msg.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing error_msg.i (no preprocessing)
-[kernel:annot-error] error_msg.i:4: Warning: expecting ';' before ensures
+[kernel:annot-error] error_msg.i:4: Warning:
+ expecting ';' before ensures
[kernel:annot-error] error_msg.i:8: Warning:
expecting ';' before end of annotation
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle
index 391634ac903d7d727471bf1b9ed212817085093b..f0d439c4204a3fbb7dbab8fcae394ecf1af7f1d2 100644
--- a/tests/spec/oracle/generalized_check.0.res.oracle
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -1,12 +1,12 @@
# frama-c -wp [...]
-[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+[kernel] Parsing generalized_check.i (no preprocessing)
[wp] Running WP plugin...
-[wp] tests/spec/generalized_check.i:30: Warning:
+[wp] generalized_check.i:30: Warning:
Unsupported generalized invariant, use loop invariant instead.
Ignored invariant
check invariant \true;
[wp] Warning: Missing RTE guards
-[wp] tests/spec/generalized_check.i:37: Warning:
+[wp] generalized_check.i:37: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 11 goals scheduled
[wp] [Qed] Goal typed_f_assigns : Valid
diff --git a/tests/spec/oracle/generalized_check.1.res.oracle b/tests/spec/oracle/generalized_check.1.res.oracle
index f93e7228b403b708b01b4386186ab29d200d1a5a..4d035120bc08cc3dbcfab9ba150f09ebcf35cfaf 100644
--- a/tests/spec/oracle/generalized_check.1.res.oracle
+++ b/tests/spec/oracle/generalized_check.1.res.oracle
@@ -1,24 +1,24 @@
-[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+[kernel] Parsing generalized_check.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/spec/generalized_check.i:23: Warning:
+[eva:alarm] generalized_check.i:23: Warning:
accessing uninitialized left-value. assert \initialized(&c);
[eva] using specification for function f
-[eva:alarm] tests/spec/generalized_check.i:24: Warning:
+[eva:alarm] generalized_check.i:24: Warning:
function f: precondition 'f_valid_x' got status unknown.
-[eva] tests/spec/generalized_check.i:9: Warning:
+[eva] generalized_check.i:9: Warning:
no \from part for clause 'assigns *x;'
-[eva:alarm] tests/spec/generalized_check.i:25: Warning:
+[eva:alarm] generalized_check.i:25: Warning:
check 'main_valid_ko' got status unknown.
-[eva:alarm] tests/spec/generalized_check.i:26: Warning:
+[eva:alarm] generalized_check.i:26: Warning:
check 'main_p_content_ko' got status unknown.
-[eva:alarm] tests/spec/generalized_check.i:32: Warning:
+[eva:alarm] generalized_check.i:32: Warning:
loop invariant 'false_but_preserved' got status invalid.
-[eva] tests/spec/generalized_check.i:35: starting to merge loop iterations
-[eva:alarm] tests/spec/generalized_check.i:36: Warning:
+[eva] generalized_check.i:35: starting to merge loop iterations
+[eva:alarm] generalized_check.i:36: Warning:
check 'implied_by_false_invariant' got status invalid.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/spec/oracle/generalized_check.2.res.oracle b/tests/spec/oracle/generalized_check.2.res.oracle
index dd870d5dc009e1cf2c1e19963f7f6d1bbae27bfb..7e0503ac2ae81e3733b87703e497dee35f843332 100644
--- a/tests/spec/oracle/generalized_check.2.res.oracle
+++ b/tests/spec/oracle/generalized_check.2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+[kernel] Parsing generalized_check.i (no preprocessing)
/* Generated by Frama-C */
/*@ check lemma easy_proof: \false;
*/
diff --git a/tests/spec/oracle/lib.res.oracle b/tests/spec/oracle/lib.res.oracle
index 080c8c4cf136a9c179298dca6232f97284c6194b..831442a8fe07b2f6c8265fdc14eb77d7e380c427 100644
--- a/tests/spec/oracle/lib.res.oracle
+++ b/tests/spec/oracle/lib.res.oracle
@@ -1,6 +1,15 @@
[kernel] Parsing lib.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 -Itmp/lib.c4c267f.i' '/home/bobot/Sources/frama-c/_build/default/result/lib.c'
- See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "lib.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] lib.h:1: Warning:
+ parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
+/* Generated by Frama-C */
+/*@ logic int f(int i) ;
+ */
+/*@ ensures f((int)0) ≡ (int)0; */
+int main(void)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/spec/oracle/merge_bts938.res.oracle b/tests/spec/oracle/merge_bts938.res.oracle
index 1661ab65689688d76107980b025872d87e042d3a..4970ba6c84524bb8f6f0c23ea0db8de65cff60d1 100644
--- a/tests/spec/oracle/merge_bts938.res.oracle
+++ b/tests/spec/oracle/merge_bts938.res.oracle
@@ -1,8 +1,26 @@
[kernel] Parsing merge_bts938.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/merge_bts938.c371829.i' '/home/bobot/Sources/frama-c/_build/default/result/merge_bts938.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 "merge_bts938.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] merge_bts938.c:7: Warning:
+ found two contracts (old location: merge_bts938.h:2). Merging them
+[kernel] Parsing merge_bts938_1.c (with preprocessing)
+[kernel] merge_bts938_1.c:7: Warning:
+ found two contracts (old location: merge_bts938.h:2). Merging them
+[kernel] merge_bts938.c:8: Warning: found two contracts. Merging them
+[kernel] merge_bts938.c:8: Warning:
+ found two contracts (old location: merge_bts938.h:2). Merging them
+/* Generated by Frama-C */
+extern int tab[10];
+
+int main(void);
+
+/*@ ensures test: \true;
+ ensures tab ≡ {tab \with [0] = (int)0};
+ ensures test1: \true;
+ */
+int main(void)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/spec/oracle/merge_different_assigns.res.oracle b/tests/spec/oracle/merge_different_assigns.res.oracle
index 2aa0db7bf538327e0993794b8f1beea42a6f3504..fa14a61ed3e8c7e2dd68e1b48d3b82de1289ac7b 100644
--- a/tests/spec/oracle/merge_different_assigns.res.oracle
+++ b/tests/spec/oracle/merge_different_assigns.res.oracle
@@ -1,13 +1,14 @@
[kernel] Parsing merge_different_assigns.i (no preprocessing)
[kernel] Parsing merge_different_assigns_bis.i (no preprocessing)
-[kernel] merge_different_assigns.i:7: Warning: found two contracts. Merging them
+[kernel] merge_different_assigns.i:7: Warning:
+ found two contracts. Merging them
[kernel] merge_different_assigns.i:8: Warning:
location z is not present in all assigns clauses
[kernel] merge_different_assigns.i:10: Warning:
incompatible from
- clauses (merge_different_assigns.i:10:'assigns t \from \nothing;' and
- merge_different_assigns_bis.i:8:'assigns t \from t;'). Keeping only the first
- one.
+ clauses (merge_different_assigns.i:10:'assigns t \from \nothing;'
+ and merge_different_assigns_bis.i:8:'assigns t \from t;'). Keeping
+ only the first one.
[kernel] merge_different_assigns_bis.i:10: Warning:
location v is not present in all assigns clauses
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/merge_logic_globals_1.res.oracle b/tests/spec/oracle/merge_logic_globals_1.res.oracle
index fadcd8f53cb12503bfc45ed992581f9650b5555a..7aeea85777c69b82fdb825f0de0e9f5bbf4d365d 100644
--- a/tests/spec/oracle/merge_logic_globals_1.res.oracle
+++ b/tests/spec/oracle/merge_logic_globals_1.res.oracle
@@ -1,2 +1,59 @@
-[kernel] User Error: source file 'merge_logic_globals_2.c' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing merge_logic_globals_1.c (with preprocessing)
+[kernel] Parsing merge_logic_globals_2.c (with preprocessing)
+[kernel] merge_logic_globals.h:14: Warning:
+ dropping duplicate def'n of func test at merge_logic_globals.h:14 in favor of that at merge_logic_globals.h:14
+/* Generated by Frama-C */
+struct s_t {
+ int n ;
+};
+typedef struct s_t t;
+/*@ type invariant inv_t(t x) = x.n > 0;
+ */
+int i = 42;
+/*@ predicate p{Here}(int x) = x ≥ i;
+ */
+/*@ axiomatic Bar {
+ logic ℤ li;
+
+ }
+ */
+/*@ ensures i ≡ li; */
+void test(void)
+{
+ return;
+}
+
+/*@
+axiomatic Foo {
+ type foo;
+
+ logic foo ff(foo x, char *y) ;
+
+ predicate fp(foo x, foo y) ;
+
+ axiom fffp{L}: ∀ foo x, char *y; fp(x, ff(x, y)) ∧ *y ≡ 0;
+
+ }
+
+*/
+int main(void)
+{
+ int __retres;
+ test();
+ /*@ assert p((int)li); */ ;
+ __retres = 0;
+ return __retres;
+}
+
+int f(void)
+{
+ int __retres;
+ t x;
+ x.n = i;
+ i --;
+ /*@ assert p(x.n); */ ;
+ __retres = x.n;
+ return __retres;
+}
+
+
diff --git a/tests/spec/oracle/model1.res.oracle b/tests/spec/oracle/model1.res.oracle
index c0fa5fe152a68bd3ee883aaec54ce1dce80182fb..74fab1dd774e744591c8884d9037c91e2706a494 100644
--- a/tests/spec/oracle/model1.res.oracle
+++ b/tests/spec/oracle/model1.res.oracle
@@ -1,8 +1,83 @@
[kernel] Parsing model1.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/model1.c7f10d5.i' '/home/bobot/Sources/frama-c/_build/default/result/model1.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 "model1.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing model2.c (with preprocessing)
+/* Generated by Frama-C */
+struct S {
+ int bar ;
+};
+/*@
+model struct S { ℤ foo };
+*/
+void reset(struct S *s);
+
+void inc(struct S *s);
+
+void dec(struct S *s);
+
+int is_pos(struct S *s);
+
+void main(void)
+{
+ struct S s;
+ reset(& s);
+ inc(& s);
+ /*@ assert s.foo > 0; */ ;
+ /*@ loop variant s.foo; */
+ while (1) {
+ int tmp;
+ tmp = is_pos(& s);
+ if (! tmp) break;
+ dec(& s);
+ }
+ /*@ assert s.foo ≤ 0; */ ;
+ return;
+}
+
+/*@ type invariant foobar(struct S s) = s.bar ≡ s.foo;
+
+*/
+/*@ requires \valid(s);
+ ensures \old(s)->foo ≡ 0;
+ assigns *s; */
+void reset(struct S *s)
+{
+ int tmp = s->bar == 0;
+ return;
+}
+
+/*@ requires \valid(s);
+ ensures \old(s)->foo > \at(s->foo,Pre);
+ assigns *s; */
+void inc(struct S *s)
+{
+ s->bar += 5;
+ return;
+}
+
+/*@ requires \valid(s);
+ ensures \old(s)->foo < \at(s->foo,Pre);
+ assigns *s; */
+void dec(struct S *s)
+{
+ (s->bar) --;
+ return;
+}
+
+/*@ requires \valid(s);
+ assigns \nothing;
+
+ behavior is_true:
+ assumes s->foo > 0;
+ ensures \result ≡ 1;
+
+ behavior is_false:
+ assumes s->foo ≤ 0;
+ ensures \result ≡ 0;
+ */
+int is_pos(struct S *s)
+{
+ int tmp;
+ if (s->bar > 0) tmp = 1; else tmp = 0;
+ return tmp;
+}
+
+
diff --git a/tests/spec/oracle/multi_axiomatic_1.res.oracle b/tests/spec/oracle/multi_axiomatic_1.res.oracle
index 49242357a0761a6feaeb1fa1e857586a810d793e..99b62a0cf76418e63d83120e6d805c2d28986700 100644
--- a/tests/spec/oracle/multi_axiomatic_1.res.oracle
+++ b/tests/spec/oracle/multi_axiomatic_1.res.oracle
@@ -1,2 +1,20 @@
-[kernel] User Error: source file 'multi_axiomatic_2.i' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing multi_axiomatic_1.i (no preprocessing)
+[kernel] Parsing multi_axiomatic_2.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ axiomatic ax {
+ logic int Acc(int m) ;
+
+ }
+ */
+/*@ predicate Bnd(ℤ n, int m) = Acc(m) ≤ 9;
+ */
+/*@ predicate Bnd(ℤ n) = Bnd(n, (int)0);
+ */
+/*@ requires Bnd(1);
+ ensures \true; */
+void foo(void)
+{
+ return;
+}
+
+
diff --git a/tests/spec/oracle/multiple_file_1.res.oracle b/tests/spec/oracle/multiple_file_1.res.oracle
index dc8375fadf197c1dfd379d2fc448673dbf760574..15adefaeaf962caa432168842ac126127dbe763d 100644
--- a/tests/spec/oracle/multiple_file_1.res.oracle
+++ b/tests/spec/oracle/multiple_file_1.res.oracle
@@ -1,6 +1,7 @@
[kernel] Parsing multiple_file_1.c (with preprocessing)
[kernel] Parsing multiple_file_2.c (with preprocessing)
-[kernel] multiple_file_1.c:10: Warning: found two contracts. Merging them
+[kernel] multiple_file_1.c:10: Warning:
+ found two contracts. Merging them
/* Generated by Frama-C */
/*@ requires x ≥ 0; */
extern int f(int x);
diff --git a/tests/spec/oracle/multiple_include_2.res.oracle b/tests/spec/oracle/multiple_include_2.res.oracle
index 75db916ee96d8628f698d83540e740930d7f8d5c..e68a9ef8456c90f7bfa3ded84ac260685a13714c 100644
--- a/tests/spec/oracle/multiple_include_2.res.oracle
+++ b/tests/spec/oracle/multiple_include_2.res.oracle
@@ -1,8 +1,4 @@
[kernel] Parsing multiple_include_2.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/multiple_include_2.cd49d12.i' '/home/bobot/Sources/frama-c/_build/default/result/multiple_include_2.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 "multiple_include_2.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+[kernel] Parsing multiple_include_1.c (with preprocessing)
+[kernel] User Error: multiple inclusion of logic function p referring to a static variable
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/preprocess.res.oracle b/tests/spec/oracle/preprocess.res.oracle
index b44e027017997a0374384042467ae94eb539d30a..5fe944d4b4146f90bb3b409d625e983227315e18 100644
--- a/tests/spec/oracle/preprocess.res.oracle
+++ b/tests/spec/oracle/preprocess.res.oracle
@@ -1,8 +1,55 @@
[kernel] Parsing preprocess.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/preprocess.c8c0ddf.i' '/home/bobot/Sources/frama-c/_build/default/result/preprocess.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 "preprocess.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ x ∈ {1}
+ y ∈ {1}
+[eva] computing for function f <- main.
+ Called from preprocess.c:24.
+[eva] preprocess.c:24: function f: precondition got status valid.
+[eva] preprocess.c:18:
+ function f, behavior default: postcondition got status valid.
+[eva] Recording results for f
+[eva] Done for function f
+[eva] preprocess.c:25: assertion got status valid.
+[eva] preprocess.c:28:
+ cannot evaluate ACSL term, unsupported ACSL construct: constant strings
+[eva:alarm] preprocess.c:28: Warning:
+ assertion 'backslash_string' got status unknown.
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function f:
+ __retres ∈ {84}
+[eva:final-states] Values at end of function main:
+ y_0 ∈ {84}
+ __retres ∈ {0}
+/* Generated by Frama-C */
+int x = 1;
+/*@ predicate test(int x) = x ≥ 42;
+ */
+int y = 1;
+/*@ requires x_0 ≥ 42;
+
+ behavior default:
+ ensures test(\result) ∧ 2 ≡ 2;
+ */
+int f(int x_0)
+{
+ int __retres;
+ __retres = x_0 + 42;
+ return __retres;
+}
+
+int main(void)
+{
+ int __retres;
+ int y_0 = f(42);
+ /*@ assert x ≡ 1; */ ;
+ /*@ assert backslash_string: *("\\" + 0) ≡ '\\'; */ ;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/spec/oracle/purse.res.oracle b/tests/spec/oracle/purse.res.oracle
index 1c67580a40cae0e22adc71ffc159882f2f927fab..002f073dcb12c237a0e04ad38453d5fa063a34aa 100644
--- a/tests/spec/oracle/purse.res.oracle
+++ b/tests/spec/oracle/purse.res.oracle
@@ -1,8 +1,83 @@
[kernel] Parsing purse.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/purse.ce2f698.i' '/home/bobot/Sources/frama-c/_build/default/result/purse.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 "purse.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+/* Generated by Frama-C */
+#include "stdlib.h"
+struct purse {
+ int balance ;
+};
+typedef struct purse purse;
+/*@ predicate purse_inv{L}(purse *p) = \valid(p) ∧ p->balance ≥ 0;
+
+*/
+/*@ requires purse_inv(p) ∧ s ≥ 0;
+ ensures
+ purse_inv(\old(p)) ∧ \old(p)->balance ≡ \old(p->balance) + \old(s);
+ assigns p->balance;
+ */
+void credit(purse *p, int s)
+{
+ p->balance += s;
+ return;
+}
+
+/*@ requires purse_inv(p) ∧ s ≥ 0;
+ ensures
+ purse_inv(\old(p)) ∧ \old(p)->balance ≡ \old(p->balance) + \old(s);
+ assigns p->balance;
+ */
+void f(purse *p, int s)
+{
+ p->balance += s;
+ return;
+}
+
+/*@ requires purse_inv(p) ∧ 0 ≤ s ≤ p->balance;
+ ensures
+ purse_inv(\old(p)) ∧ \old(p)->balance ≡ \old(p->balance) - \old(s);
+ assigns p->balance;
+ */
+void withdraw(purse *p, int s)
+{
+ p->balance -= s;
+ return;
+}
+
+/*@ requires purse_inv(p1) ∧ purse_inv(p2);
+ ensures \result ≡ 0;
+ assigns p1->balance, p2->balance;
+ */
+int test1(purse *p1, purse *p2)
+{
+ int __retres;
+ p1->balance = 0;
+ credit(p2,100);
+ __retres = p1->balance;
+ return __retres;
+}
+
+/*@ ensures
+ \fresh{Old, Here}(\result,sizeof(purse)) ∧ purse_inv(\result) ∧
+ \result->balance ≡ 0;
+ assigns \empty;
+ */
+purse *new_purse(void)
+{
+ purse *p = malloc((unsigned int)1 * sizeof(purse));
+ p->balance = 0;
+ return p;
+}
+
+/*@ ensures \result ≡ 150; */
+int test2(void)
+{
+ int __retres;
+ purse *p1 = new_purse();
+ purse *p2 = new_purse();
+ credit(p1,100);
+ credit(p2,200);
+ withdraw(p1,50);
+ withdraw(p2,100);
+ __retres = p1->balance + p2->balance;
+ return __retres;
+}
+
+
diff --git a/tests/spec/oracle/rm_qualifiers.res.oracle b/tests/spec/oracle/rm_qualifiers.res.oracle
index 04e77de3d9d0fc52035a3cc55825d7b4b5a58cd8..04cc92b6caa444bb12ff2111b6b7aa2294b1e733 100644
--- a/tests/spec/oracle/rm_qualifiers.res.oracle
+++ b/tests/spec/oracle/rm_qualifiers.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing rm_qualifiers.i (no preprocessing)
-[kernel] Parsing rm_qualifiers_res.i (no preprocessing)
+[kernel] Parsing result/rm_qualifiers_res.i (no preprocessing)
/* Generated by Frama-C */
extern void G(void const *p);
diff --git a/tests/spec/oracle/shifts.res.oracle b/tests/spec/oracle/shifts.res.oracle
index ab0a299ade0b5cdc19ea16babd89813186c1ab88..921a576fb7ae4aaa89cd0251503dfce016dc787c 100644
--- a/tests/spec/oracle/shifts.res.oracle
+++ b/tests/spec/oracle/shifts.res.oracle
@@ -7,8 +7,10 @@
[eva] computing for function f <- main.
Called from shifts.c:19.
[eva] shifts.c:13: assertion got status valid.
-[eva] shifts.c:8: function f, behavior a: postcondition got status valid.
-[eva] shifts.c:9: function f, behavior b: postcondition got status valid.
+[eva] shifts.c:8:
+ function f, behavior a: postcondition got status valid.
+[eva] shifts.c:9:
+ function f, behavior b: postcondition got status valid.
[eva] Recording results for f
[eva] Done for function f
[eva] Recording results for main
diff --git a/tests/spec/oracle/statement_behavior.res.oracle b/tests/spec/oracle/statement_behavior.res.oracle
index 225540226e3a237d0208cc020eb78db127076b94..d866de33a68c65334b0d14c00491233a8cd87fbe 100644
--- a/tests/spec/oracle/statement_behavior.res.oracle
+++ b/tests/spec/oracle/statement_behavior.res.oracle
@@ -8,7 +8,8 @@
Called from statement_behavior.c:23.
[eva] statement_behavior.c:10: Warning:
no \from part for clause 'assigns five_times;'
-[eva:alarm] statement_behavior.c:17: Warning: assertion got status unknown.
+[eva:alarm] statement_behavior.c:17: Warning:
+ assertion got status unknown.
[eva:alarm] statement_behavior.c:4: Warning:
function pfsqopfc: postcondition got status unknown.
[eva:alarm] statement_behavior.c:18: Warning:
diff --git a/tests/spec/oracle/status_by_call_issue_890.res.oracle b/tests/spec/oracle/status_by_call_issue_890.res.oracle
index 33e76da4d07f848c16531e3c1fa56d9c8828261c..6b1e54789c6305e32d23ea9d3ab19f3228dd6f9e 100644
--- a/tests/spec/oracle/status_by_call_issue_890.res.oracle
+++ b/tests/spec/oracle/status_by_call_issue_890.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/spec/status_by_call_issue_890.i (no preprocessing)
+[kernel] Parsing status_by_call_issue_890.i (no preprocessing)
/* Generated by Frama-C */
struct list {
struct list *next ;
diff --git a/tests/spec/oracle/transitive_rel.res.oracle b/tests/spec/oracle/transitive_rel.res.oracle
index f9db4c2965897ef5cacb755bf56fa26a9eb5be10..15f180b46998b73200d96fe9295ad78146b7be90 100644
--- a/tests/spec/oracle/transitive_rel.res.oracle
+++ b/tests/spec/oracle/transitive_rel.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing transitive_rel.c (with preprocessing)
-[kernel:annot-error] transitive_rel.c:16: Warning: Inconsistent relation chain.
+[kernel:annot-error] transitive_rel.c:16: Warning:
+ Inconsistent relation chain.
/* Generated by Frama-C */
/*@ predicate bound(int x, int y, int z) = x ≤ y < z ∧ z ≥ y > x;
*/
diff --git a/tests/spec/oracle/use.res.oracle b/tests/spec/oracle/use.res.oracle
index 5cc8ff67c6b5f56f443b0e9b180dd0156d28a2d1..ca1b1e2e0af8aacce861af57fd5e388e2468515a 100644
--- a/tests/spec/oracle/use.res.oracle
+++ b/tests/spec/oracle/use.res.oracle
@@ -1,8 +1,25 @@
[kernel] Parsing use.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/use.c492245.i' '/home/bobot/Sources/frama-c/_build/default/result/use.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 "use.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing use2.c (with preprocessing)
+/* Generated by Frama-C */
+/*@ axiomatic S {
+ logic ℤ F(ℤ x) ;
+
+ }
+ */
+/*@ logic ℤ X= 42;
+ */
+/*@ ensures X > 0;
+ ensures F(1) > 0; */
+void f(void)
+{
+ return;
+}
+
+/*@ ensures X > 0;
+ ensures F(1) > 0; */
+void g(void)
+{
+ return;
+}
+
+
diff --git a/tests/spec/oracle/volatile.res.oracle b/tests/spec/oracle/volatile.res.oracle
index f89207566b04db797b3119b5cb40389009d53c5a..53ddb97bb63f8b8c385d46e693cfab9762a8d20e 100644
--- a/tests/spec/oracle/volatile.res.oracle
+++ b/tests/spec/oracle/volatile.res.oracle
@@ -1,8 +1,97 @@
[kernel] Parsing volatile.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/volatile.c35a951.i' '/home/bobot/Sources/frama-c/_build/default/result/volatile.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 "volatile.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing volatile_aux.c (with preprocessing)
+[kernel] volatile.c:8: Warning:
+ Overlapping volatile specification: volatile location y already associated to a writes function in annotation at loc volatile.c:7. Ignoring new binding.
+[kernel] volatile.c:9: Warning:
+ Overlapping volatile specification: volatile location x already associated to a writes function in annotation at loc volatile.c:7. Ignoring new binding.
+[kernel] volatile.c:10: Warning:
+ Overlapping volatile specification: volatile location y already associated to a reads function in annotation at loc volatile.c:8. Ignoring new binding.
+/* Generated by Frama-C */
+typedef int volatile VINT;
+struct st {
+ int a ;
+ int volatile v ;
+};
+typedef struct st ST;
+struct vst {
+ int b ;
+ ST v ;
+};
+int f(int x_0);
+
+__inline static int r__fc_inline(VINT *v_0)
+{
+ int __retres;
+ __retres = *v_0;
+ return __retres;
+}
+
+__inline static int w__fc_inline(int volatile *v_0, int new)
+{
+ *v_0 = new;
+ return new;
+}
+
+int volatile v;
+int volatile tab[10];
+VINT *pt;
+struct st s;
+/*@ volatile v, tab[..] reads r__fc_inline writes w__fc_inline; */
+/*@ volatile *pt writes w__fc_inline; */
+/*@ volatile s.v reads r__fc_inline;
+*/
+struct vst vs;
+struct vst rs(struct vst *p);
+
+struct vst ws(struct vst *p, struct vst v);
+
+/*@ volatile vs reads rs writes ws;
+*/
+int volatile x;
+int volatile y;
+int volatile z;
+/*@ volatile x, y writes w__fc_inline; */
+/*@ volatile y, z reads r__fc_inline writes w__fc_inline; */
+/*@ volatile x writes w__fc_inline; */
+/*@ volatile y reads r__fc_inline; */
+int const c = 1;
+int *p;
+/*@ lemma comp_const_addr{L}: p ≡ &c;
+ */
+/*@ lemma comp_volatile_addr{L}: p ≡ &v;
+ */
+/*@ lemma volatile_in_annot_is_illegal{L}: v ≡ 1 ⇒ v ≡ 1;
+
+*/
+int main(void)
+{
+ int __retres;
+ int x_0 = v;
+ v = f(x_0);
+ __retres = 0;
+ return __retres;
+}
+
+__inline static int r__fc_inline_0(VINT *v_0)
+{
+ int __retres;
+ __retres = *v_0;
+ return __retres;
+}
+
+__inline static int w__fc_inline_0(int volatile *v_0, int new)
+{
+ *v_0 = new;
+ return new;
+}
+
+int f(int x_0)
+{
+ int __retres;
+ x_0 ++;
+ v = x_0;
+ __retres = v + x_0;
+ return __retres;
+}
+
+