AllanBlanchard · AllanBlanchard · May 21, 2026 · Feb 16, 2026 · Mar 22, 2026 · Mar 22, 2026
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,4 @@
+# latex
 */_minted-main*
 *.aux
 *.glg
@@ -11,10 +12,15 @@
 *.thm
 *.toc
 *.html
+*.fls
+*.fdb_latexmk
+# temps
 *~
 \#*\#
+# Frama-C tests
+**/.frama-c
+**/.frama-c-gui.local
 code/_build
-code/*/*/.frama-c
 code/**/oracle/dune
 code/**/result
 code/tests

diff --git a/code/acsl-logic-definitions/axiomatic/oracle/all-zeroes-bad.0.res.oracle b/code/acsl-logic-definitions/axiomatic/oracle/all-zeroes-bad.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing all-zeroes-bad.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function bad_function
 [wp] [Valid] Goal bad_function_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal bad_function_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/axiomatic/oracle/ex-1-occurrences_of-answer.0.res.oracle b/code/acsl-logic-definitions/axiomatic/oracle/ex-1-occurrences_of-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-1-occurrences_of-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function occurrences_of
 [wp] [Valid] Goal occurrences_of_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal occurrences_of_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/axiomatic/oracle/ex-2-gcd-answer.0.res.oracle b/code/acsl-logic-definitions/axiomatic/oracle/ex-2-gcd-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-2-gcd-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function gcd
 [wp] [Valid] Goal gcd_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal gcd_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/axiomatic/oracle/ex-3-sum-N-first-ints-answer.0.res.oracle b/code/acsl-logic-definitions/axiomatic/oracle/ex-3-sum-N-first-ints-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-3-sum-N-first-ints-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function sum_n
 [wp] [Valid] Goal sum_n_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal sum_n_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/axiomatic/oracle/ex-4-sort-answer.0.res.oracle b/code/acsl-logic-definitions/axiomatic/oracle/ex-4-sort-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-4-sort-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function min_idx_in
 [rte:annot] annotating function sort
 [rte:annot] annotating function swap

diff --git a/code/acsl-logic-definitions/axiomatic/oracle/false.0.res.oracle b/code/acsl-logic-definitions/axiomatic/oracle/false.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing false.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function main
 [wp] [Valid] Goal main_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal main_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/axiomatic/oracle/occurrences_of.0.res.oracle b/code/acsl-logic-definitions/axiomatic/oracle/occurrences_of.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing occurrences_of.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function occurrences_of
 [wp] [Valid] Goal occurrences_of_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal occurrences_of_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/axiomatic/oracle/reset-1.0.res.oracle b/code/acsl-logic-definitions/axiomatic/oracle/reset-1.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing reset-1.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function reset
 [wp] [Valid] Goal reset_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal reset_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/axiomatic/oracle/strlen-fails.0.res.oracle b/code/acsl-logic-definitions/axiomatic/oracle/strlen-fails.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing strlen-fails.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function strlen
 [wp] [Valid] Goal strlen_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal strlen_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/axiomatic/oracle/strlen-proved.0.res.oracle b/code/acsl-logic-definitions/axiomatic/oracle/strlen-proved.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing strlen-proved.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function strlen
 [wp] [Valid] Goal strlen_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal strlen_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/axiomatic/oracle/wrong-facto.0.res.oracle b/code/acsl-logic-definitions/axiomatic/oracle/wrong-facto.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing wrong-facto.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function example
 [wp] [Valid] Goal example_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal example_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/ghost-code/oracle/assigns-clause-2.0.res.oracle b/code/acsl-logic-definitions/ghost-code/oracle/assigns-clause-2.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing assigns-clause-2.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function foo
 [wp] [Valid] Goal foo_exits (Cfg) (Unreachable)
 [wp] 5 goals scheduled

diff --git a/code/acsl-logic-definitions/ghost-code/oracle/ex-2-times-2-answer.0.res.oracle b/code/acsl-logic-definitions/ghost-code/oracle/ex-2-times-2-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-2-times-2-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function times_2
 [wp] [Valid] Goal times_2_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal times_2_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/ghost-code/oracle/ex-3-array-answer-1.0.res.oracle b/code/acsl-logic-definitions/ghost-code/oracle/ex-3-array-answer-1.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-3-array-answer-1.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function foo
 [wp] [Valid] Goal foo_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal foo_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/ghost-code/oracle/ex-3-array-answer-2.0.res.oracle b/code/acsl-logic-definitions/ghost-code/oracle/ex-3-array-answer-2.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-3-array-answer-2.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function copy
 [rte:annot] annotating function foo
 [wp] [Valid] Goal copy_exits (Cfg) (Unreachable)

diff --git a/code/acsl-logic-definitions/ghost-code/oracle/ex-4-replace-answer.0.res.oracle b/code/acsl-logic-definitions/ghost-code/oracle/ex-4-replace-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-4-replace-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function caller
 [kernel:annot:missing-spec] ex-4-replace-answer.c:40: Warning: 
   Neither code nor explicit exits and terminates for function initialize,

diff --git a/code/acsl-logic-definitions/ghost-code/oracle/ghost-array-1.0.res.oracle b/code/acsl-logic-definitions/ghost-code/oracle/ghost-array-1.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ghost-array-1.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function function
 [wp] [Valid] Goal function_exits (Cfg) (Unreachable)
 [wp] ghost-array-1.c:4: Warning: 

diff --git a/code/acsl-logic-definitions/ghost-code/oracle/ghost-array-3.0.res.oracle b/code/acsl-logic-definitions/ghost-code/oracle/ghost-array-3.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ghost-array-3.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function function
 [wp] [Valid] Goal function_exits (Cfg) (Unreachable)
 [wp] ghost-array-3.c:5: Warning: 

diff --git a/code/acsl-logic-definitions/inductive/even-bad-2.c b/code/acsl-logic-definitions/inductive/even-bad-2.c
@@ -0,0 +1,20 @@
+/* run.config
+   OPT:
+*/
+
+/*@
+  inductive P(int*p) {
+  case c:
+    \forall int* p ; \valid(p) && p == (void*)0 ==> P(p) ;
+  }
+*/
+
+int n;
+
+/*@
+  requires P(&n) ;
+  ensures  \false ;
+*/
+void function(void){
+
+}
diff --git a/code/acsl-logic-definitions/inductive/even-bad-3.c b/code/acsl-logic-definitions/inductive/even-bad-3.c
@@ -0,0 +1,22 @@
+/* run.config
+   OPT:
+*/
+
+/*@
+  predicate hide_valid(int* p) = \valid(p);
+
+  inductive P(int*p) {
+  case c:
+    \forall int* p ; hide_valid(p) && p == (void*)0 ==> P(p) ;
+  }
+*/
+
+int n ;
+
+/*@
+  requires P(&n) ;
+  ensures  \false ;
+*/
+void function(int n){
+
+}
diff --git a/code/acsl-logic-definitions/inductive/even-bad.c b/code/acsl-logic-definitions/inductive/even-bad.c
@@ -14,10 +14,3 @@
       even_natural(n) ;
   }
 */
-
-/*@
-  requires even_natural(n) ;
-  ensures  \false ;
-*/ void function(int n){
-
-}
diff --git a/code/acsl-logic-definitions/inductive/oracle/even-0.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/even-0.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte -wp-timeout 5 [...]
 [kernel] Parsing even-0.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function bar
 [rte:annot] annotating function foo
 [wp] [Valid] Goal bar_exits (Cfg) (Unreachable)

diff --git a/code/acsl-logic-definitions/inductive/oracle/even-1.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/even-1.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing even-1.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function bar
 [wp] [Valid] Goal bar_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal bar_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/inductive/oracle/even-bad-2.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/even-bad-2.0.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing even-bad-2.c (with preprocessing)
diff --git a/code/acsl-logic-definitions/inductive/oracle/even-bad-3.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/even-bad-3.0.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing even-bad-3.c (with preprocessing)
diff --git a/code/acsl-logic-definitions/inductive/oracle/ex-1-sum-N-first-ints-answer.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/ex-1-sum-N-first-ints-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-1-sum-N-first-ints-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function sum_n
 [wp] [Valid] Goal sum_n_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal sum_n_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/inductive/oracle/ex-2-gcd-answer.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/ex-2-gcd-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-2-gcd-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function gcd
 [wp] [Valid] Goal gcd_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal gcd_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/inductive/oracle/ex-4-rotate-permutation-answer.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/ex-4-rotate-permutation-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-4-rotate-permutation-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function rotate
 [rte:annot] annotating function two_rotates
 [wp] [Valid] Goal rotate_exits (Cfg) (Unreachable)

diff --git a/code/acsl-logic-definitions/inductive/oracle/other-bad.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/other-bad.0.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing other-bad.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
+[rte:annot] annotating function foo
+[wp] [Valid] Goal foo_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal foo_terminates (Cfg) (Trivial)
+[wp] 1 goal scheduled
+[wp] User Error: After simplification inductive P appear ill-formed (hint: check cases premises)
+[wp] Warning: Goal Property: running prover Alt-Ergo:2.6.2 failed ([User Error])
+[wp] [Failure] typed_foo_ensures (Alt-Ergo) (No Cache)
+[wp] Proved goals:    2 / 3
+  Terminating:     1
+  Unreachable:     1
+  Failed:          1
+[wp:pedantic-assigns] other-bad.c:8: Warning: 
+  No 'assigns' specification for function 'foo'.
+  Callers assumptions might be imprecise.
diff --git a/code/acsl-logic-definitions/inductive/oracle/reset-0.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/reset-0.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing reset-0.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function reset
 [wp] [Valid] Goal reset_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal reset_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/inductive/oracle/reset-1.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/reset-1.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing reset-1.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function reset
 [wp] [Valid] Goal reset_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal reset_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/inductive/oracle/sort-1.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/sort-1.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing sort-1.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function min_idx_in
 [rte:annot] annotating function sort
 [rte:annot] annotating function swap

diff --git a/code/acsl-logic-definitions/inductive/oracle/sort-false.0.res.oracle b/code/acsl-logic-definitions/inductive/oracle/sort-false.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing sort-false.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function fail_sort
 [wp] [Valid] Goal fail_sort_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal fail_sort_terminates (Cfg) (Trivial)

diff --git a/code/acsl-logic-definitions/inductive/other-bad.c b/code/acsl-logic-definitions/inductive/other-bad.c
@@ -0,0 +1,8 @@
+/*@ inductive P(int* p){
+      case c: \forall int* p ; \valid(p) && p == (void*)0 ==> P(p);
+    }
+*/
+
+/*@ requires P(p);
+    ensures \false ; */
+void foo(int *p){}
diff --git a/code/acsl-properties/functions/oracle/ex-1-distance-answer.0.res.oracle b/code/acsl-properties/functions/oracle/ex-1-distance-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-1-distance-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function distance
 [wp] [Valid] Goal distance_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal distance_terminates (Cfg) (Trivial)

diff --git a/code/acsl-properties/functions/oracle/ex-2-square-answer.0.res.oracle b/code/acsl-properties/functions/oracle/ex-2-square-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte -warn-unsigned-overflow -warn-unsigned-downcast [...]
 [kernel] Parsing ex-2-square-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function abs
 [rte:annot] annotating function square
 [wp] [Valid] Goal abs_exits (Cfg) (Unreachable)

diff --git a/code/acsl-properties/functions/oracle/ex-3-iota-answer.0.res.oracle b/code/acsl-properties/functions/oracle/ex-3-iota-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-3-iota-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function iota
 [wp] [Valid] Goal iota_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal iota_terminates (Cfg) (Trivial)

diff --git a/code/acsl-properties/functions/oracle/ex-4-vec-inc-answer.0.res.oracle b/code/acsl-properties/functions/oracle/ex-4-vec-inc-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-4-vec-inc-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function show_the_difference
 [rte:annot] annotating function vec_add
 [wp] [Valid] Goal vec_add_exits (Cfg) (Unreachable)

diff --git a/code/acsl-properties/functions/oracle/ex-5-n-first-ints-answer.0.res.oracle b/code/acsl-properties/functions/oracle/ex-5-n-first-ints-answer.0.res.oracle
@@ -1,6 +1,8 @@
 # frama-c -wp -wp-rte [...]
 [kernel] Parsing ex-5-n-first-ints-answer.c (with preprocessing)
 [wp] Running WP plugin...
+[wp] Warning: Skipped RTE guards: unaligned pointers (\aligned not supported)
+[wp] Warning: Skipped RTE guards: invalid function pointer calls (\valid_function not supported)
 [rte:annot] annotating function sum_n
 [wp] [Valid] Goal sum_n_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal sum_n_terminates (Cfg) (Trivial)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		[kernel] Parsing even-bad-2.c (with preprocessing)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		[kernel] Parsing even-bad-3.c (with preprocessing)