From 7a31c2dd87e68ebf99a2d890684d5c22a3079bb5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 29 Sep 2020 17:01:47 +0200
Subject: [PATCH] recover good oracles for spec
---
ptests/ptests.ml | 9 +-
tests/saveload/deps.i | 12 +-
tests/sparecode/test_config | 1 +
tests/spec/anon_arg_2.i | 2 +-
tests/spec/axiom_included.c | 3 +-
tests/spec/bts0578.i | 4 +-
tests/spec/generalized_check.i | 1 +
tests/spec/lib.c | 2 +-
tests/spec/merge_1.i | 2 +-
tests/spec/merge_bts938.c | 2 +-
tests/spec/merge_different_assigns.i | 2 +-
tests/spec/multi_axiomatic_1.i | 2 +-
.../oracle/acsl_basic_allocator.res.oracle | 105 ++++++++++++++++--
.../spec/oracle/annot_decl_bts1009.res.oracle | 10 +-
tests/spec/oracle/anon_arg_2.res.oracle | 21 +++-
tests/spec/oracle/array_typedef.res.oracle | 3 +-
.../oracle/assignable_location.res.oracle | 3 +-
tests/spec/oracle/axiom_included.res.oracle | 15 +--
.../spec/oracle/behavior_assert.0.res.oracle | 9 +-
.../spec/oracle/behavior_assert.1.res.oracle | 3 +-
.../clash_double_file_bts1598.res.oracle | 2 +-
tests/spec/oracle/doxygen.res.oracle | 37 ------
tests/spec/oracle/error_msg.res.oracle | 3 +-
.../oracle/generalized_check.0.res.oracle | 6 +-
.../oracle/generalized_check.1.res.oracle | 18 +--
.../oracle/generalized_check.2.res.oracle | 2 +-
tests/spec/oracle/lib.res.oracle | 19 +++-
tests/spec/oracle/merge_bts938.res.oracle | 32 ++++--
.../oracle/merge_different_assigns.res.oracle | 9 +-
.../oracle/merge_logic_globals_1.res.oracle | 61 +++++++++-
tests/spec/oracle/model1.res.oracle | 89 +++++++++++++--
.../spec/oracle/multi_axiomatic_1.res.oracle | 22 +++-
tests/spec/oracle/multiple_file_1.res.oracle | 3 +-
.../spec/oracle/multiple_include_2.res.oracle | 8 +-
tests/spec/oracle/preprocess.res.oracle | 61 ++++++++--
tests/spec/oracle/purse.res.oracle | 89 +++++++++++++--
tests/spec/oracle/rm_qualifiers.res.oracle | 2 +-
tests/spec/oracle/shifts.res.oracle | 6 +-
.../spec/oracle/statement_behavior.res.oracle | 3 +-
.../status_by_call_issue_890.res.oracle | 2 +-
tests/spec/oracle/transitive_rel.res.oracle | 3 +-
tests/spec/oracle/use.res.oracle | 31 ++++--
tests/spec/oracle/volatile.res.oracle | 103 +++++++++++++++--
43 files changed, 650 insertions(+), 172 deletions(-)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 4ed528781c7..274977fc09e 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 a9290b7c510..fa94aacd688 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 a9330dd48d0..a8bbd0d9d8f 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 9e3ef0cb8d0..80197a9b0f7 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 4b30e4e5337..2b3bb5dece3 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 2e1bf64bb4c..4ecccedf4d0 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 66c93e7d3a8..8f06f2a0a58 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 8a1d566beaf..54cd5a85a14 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 ac6d0792236..409e6b7683f 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 8ee32add093..efd3962eb5d 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 63fea95aa5b..b9166ff75bc 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 cfe295495cc..8430c9c2bbf 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 cf8150d4acb..6d2b0811ba6 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 6c592eecabf..24b7d528817 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 d9ebdefad94..4dac36af6cc 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 585ed5bea14..f9f255b9bff 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 43aec8f2843..db7ee46c131 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 b79a2467ca2..a0b318d9f59 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 fe15f248e83..a909a19c510 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 13875b49281..e206e4995a9 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 19ba21bf7c8..93fcee65eeb 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 80866aac793..5a7807914f0 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 e973fed7c59..246a6346f75 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 391634ac903..f0d439c4204 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 f93e7228b40..4d035120bc0 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 dd870d5dc00..7e0503ac2ae 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 080c8c4cf13..831442a8fe0 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 1661ab65689..4970ba6c845 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 2aa0db7bf53..fa14a61ed3e 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 fadcd8f53cb..7aeea85777c 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 c0fa5fe152a..74fab1dd774 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 49242357a07..99b62a0cf76 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 dc8375fadf1..15adefaeaf9 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 75db916ee96..e68a9ef8456 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 b44e0270179..5fe944d4b41 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 1c67580a40c..002f073dcb1 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 04e77de3d9d..04cc92b6caa 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 ab0a299ade0..921a576fb7a 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 225540226e3..d866de33a68 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 33e76da4d07..6b1e54789c6 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 f9db4c29658..15f180b4699 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 5cc8ff67c6b..ca1b1e2e0af 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 f89207566b0..53ddb97bb63 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;
+}
+
+
--
GitLab