Update section about loops wrt terminates

code/statements/function-calls/oracle/terminates.0.res.oracle

@@ -1,53 +1,55 @@
 # frama-c -wp [...]
 [kernel] Parsing terminates.c (with preprocessing)
 [wp] Running WP plugin...
-[kernel:annot:missing-spec] terminates.c:57: Warning: 
-  Neither code nor specification for function call, generating default assigns from the prototype
-[kernel:annot:missing-spec] terminates.c:57: Warning: 
-  Neither code nor implicit assigns clause for function callee, generating default assigns from the prototype
+[kernel:annot:missing-spec] terminates.c:11: Warning: 
+  Neither code nor specification for function call,
+   generating default exits, assigns and terminates. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] terminates.c:28: Warning: 
+  Neither code nor explicit exits and assigns for function callee,
+   generating default clauses. See -generated-spec-* options for more info
+[wp] [Valid] Goal cond_may_not_terminate_exits (Cfg) (Unreachable)
 [wp] Warning: Missing RTE guards
-[wp] [CFG] Goal may_not_terminate_terminates : Valid (Trivial)
-[wp] terminates.c:16: Warning: 
-  Missing terminates clause on call to call, defaults to \false
+[wp] [Valid] Goal may_not_terminate_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal may_not_terminate_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal with_loop_exits (Cfg) (Unreachable)
 [wp] terminates.c:23: Warning: 
   Missing assigns clause (assigns 'everything' instead)
 [wp] terminates.c:50: Warning: 
   Missing decreases clause on recursive function missing_decreases, call must be unreachable
-[wp] 15 goals scheduled
-[wp] [Unsuccess] typed_simple_terminates (Alt-Ergo) (Cached)
+[wp] 19 goals scheduled
+[wp] [Valid] typed_simple_terminates (Qed)
+[wp] [Valid] typed_simple_exits (Qed)
 [wp] [Valid] typed_cond_may_not_terminate_terminates (Qed)
 [wp] [Valid] typed_with_calls_terminates_part1 (Qed)
 [wp] [Unsuccess] typed_with_calls_terminates_part2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_with_calls_exits (Qed)
 [wp] [Valid] typed_with_loop_terminates (Qed)
 [wp] [Valid] typed_with_loop_loop_assigns (Qed)
 [wp] [Valid] typed_missing_decreases_terminates_part1 (Qed)
 [wp] [Unsuccess] typed_missing_decreases_terminates_part2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_missing_decreases_exits (Qed)
 [wp] [Valid] typed_recursive_terminates_part1 (Qed)
 [wp] [Valid] typed_recursive_terminates_part2 (Qed)
 [wp] [Valid] typed_recursive_terminates_part3 (Qed)
+[wp] [Valid] typed_recursive_exits (Qed)
 [wp] [Unsuccess] typed_recursive_variant_part1 (Alt-Ergo) (Cached)
 [wp] [Valid] typed_recursive_variant_part2 (Qed)
 [wp] [Valid] typed_recursive_call_recursive_requires (Qed)
 [wp] [Valid] typed_recursive_call_recursive_2_requires (Qed)
-[wp] Proved goals:   12 / 16
+[wp] Proved goals:   20 / 23
   Terminating:     1
-  Qed:            11
-  Unsuccess:       4
+  Unreachable:     3
+  Qed:            16
+  Unsuccess:       3
 [wp:pedantic-assigns] terminates.c:7: Warning: 
   No 'assigns' specification for function 'may_not_terminate'.
   Callers assumptions might be imprecise.
-[wp:pedantic-assigns] terminates.c:11: Warning: 
-  No 'assigns' specification for function 'call'.
-  Callers assumptions might be imprecise.
 [wp:pedantic-assigns] terminates.c:14: Warning: 
   No 'assigns' specification for function 'simple'.
   Callers assumptions might be imprecise.
 [wp:pedantic-assigns] terminates.c:20: Warning: 
   No 'assigns' specification for function 'cond_may_not_terminate'.
   Callers assumptions might be imprecise.
-[wp:pedantic-assigns] terminates.c:28: Warning: 
-  No 'assigns' specification for function 'callee'.
-  Callers assumptions might be imprecise.
 [wp:pedantic-assigns] terminates.c:31: Warning: 
   No 'assigns' specification for function 'with_calls'.
   Callers assumptions might be imprecise.

code/statements/function-calls/oracle/terminates.1.res.oracle

@@ -1,53 +1,55 @@
 # frama-c -wp [...]
 [kernel] Parsing terminates.c (with preprocessing)
 [wp] Running WP plugin...
-[kernel:annot:missing-spec] terminates.c:57: Warning: 
-  Neither code nor specification for function call, generating default assigns from the prototype
-[kernel:annot:missing-spec] terminates.c:57: Warning: 
-  Neither code nor implicit assigns clause for function callee, generating default assigns from the prototype
+[kernel:annot:missing-spec] terminates.c:11: Warning: 
+  Neither code nor specification for function call,
+   generating default exits, assigns and terminates. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] terminates.c:28: Warning: 
+  Neither code nor explicit exits and assigns for function callee,
+   generating default clauses. See -generated-spec-* options for more info
+[wp] [Valid] Goal cond_may_not_terminate_exits (Cfg) (Unreachable)
 [wp] Warning: Missing RTE guards
-[wp] [CFG] Goal may_not_terminate_terminates : Valid (Trivial)
-[wp] terminates.c:16: Warning: 
-  Missing terminates clause on call to call, defaults to \false
+[wp] [Valid] Goal may_not_terminate_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal may_not_terminate_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal with_loop_exits (Cfg) (Unreachable)
 [wp] terminates.c:23: Warning: 
   Missing assigns clause (assigns 'everything' instead)
 [wp] terminates.c:50: Warning: 
   Missing decreases clause on recursive function missing_decreases, call must be unreachable
-[wp] 15 goals scheduled
-[wp] [Unsuccess] typed_simple_terminates (Alt-Ergo) (Cached)
+[wp] 19 goals scheduled
+[wp] [Valid] typed_simple_terminates (Qed)
+[wp] [Valid] typed_simple_exits (Qed)
 [wp] [Valid] typed_cond_may_not_terminate_terminates (Qed)
 [wp] [Valid] typed_with_calls_terminates_part1 (Qed)
 [wp] [Unsuccess] typed_with_calls_terminates_part2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_with_calls_exits (Qed)
 [wp] [Valid] typed_with_loop_terminates (Qed)
 [wp] [Valid] typed_with_loop_loop_assigns (Qed)
 [wp] [Valid] typed_missing_decreases_terminates_part1 (Qed)
 [wp] [Unsuccess] typed_missing_decreases_terminates_part2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_missing_decreases_exits (Qed)
 [wp] [Valid] typed_recursive_terminates_part1 (Qed)
 [wp] [Valid] typed_recursive_terminates_part2 (Qed)
 [wp] [Valid] typed_recursive_terminates_part3 (Qed)
+[wp] [Valid] typed_recursive_exits (Qed)
 [wp] [Valid] typed_recursive_variant_part1 (Qed)
 [wp] [Valid] typed_recursive_variant_part2 (Qed)
 [wp] [Valid] typed_recursive_call_recursive_requires (Qed)
 [wp] [Valid] typed_recursive_call_recursive_2_requires (Qed)
-[wp] Proved goals:   13 / 16
+[wp] Proved goals:   21 / 23
   Terminating:     1
-  Qed:            12
-  Unsuccess:       3
+  Unreachable:     3
+  Qed:            17
+  Unsuccess:       2
 [wp:pedantic-assigns] terminates.c:7: Warning: 
   No 'assigns' specification for function 'may_not_terminate'.
   Callers assumptions might be imprecise.
-[wp:pedantic-assigns] terminates.c:11: Warning: 
-  No 'assigns' specification for function 'call'.
-  Callers assumptions might be imprecise.
 [wp:pedantic-assigns] terminates.c:14: Warning: 
   No 'assigns' specification for function 'simple'.
   Callers assumptions might be imprecise.
 [wp:pedantic-assigns] terminates.c:20: Warning: 
   No 'assigns' specification for function 'cond_may_not_terminate'.
   Callers assumptions might be imprecise.
-[wp:pedantic-assigns] terminates.c:28: Warning: 
-  No 'assigns' specification for function 'callee'.
-  Callers assumptions might be imprecise.
 [wp:pedantic-assigns] terminates.c:31: Warning: 
   No 'assigns' specification for function 'with_calls'.
   Callers assumptions might be imprecise.

code/statements/loops/first_loop-5.c

@@ -0,0 +1,15 @@
+int main(){
+  int i = 0;
+  int h = 42;
+
+  /*@
+    loop invariant 0 <= i <= 30;
+    loop assigns i;
+    loop variant 30 - i;
+  */
+  while(i < 30){
+    //++i;
+  }
+  //@assert i == 30;
+  //@assert h == 42;
+}

code/statements/loops/oracle/first_loop-1.0.res.oracle

@@ -2,15 +2,19 @@
 [kernel] Parsing first_loop-1.c (with preprocessing)
 [wp] Running WP plugin...
 [rte:annot] annotating function main
+[wp] [Valid] Goal main_exits (Cfg) (Unreachable)
 [wp] first_loop-1.c:12: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] 4 goals scheduled
+[wp] 5 goals scheduled
+[wp] [Unsuccess] typed_main_terminates (Alt-Ergo) (Cached)
 [wp] [Valid] typed_main_loop_invariant_preserved (Qed)
 [wp] [Valid] typed_main_loop_invariant_established (Qed)
 [wp] [Valid] typed_main_assert_rte_signed_overflow (Qed)
 [wp] [Valid] typed_main_assert (Qed)
-[wp] Proved goals:    4 / 4
+[wp] Proved goals:    5 / 6
+  Unreachable:     1
   Qed:             4
+  Unsuccess:       1
 [wp:pedantic-assigns] first_loop-1.c:6: Warning: 
   No 'assigns' specification for function 'main'.
   Callers assumptions might be imprecise.

code/statements/loops/oracle/first_loop-1.1.res.oracle

@@ -7,6 +7,12 @@
   Function main
 ------------------------------------------------------------
 
+Goal Termination-condition (generated) in 'main':
+Loop termination at line 12
+Prove: false.
+
+------------------------------------------------------------
+
 Goal Preservation of Invariant (file first_loop-1.c, line 10):
 Prove: true.
 

code/statements/loops/oracle/first_loop-2.res.oracle

@@ -2,17 +2,20 @@
 [kernel] Parsing first_loop-2.c (with preprocessing)
 [wp] Running WP plugin...
 [rte:annot] annotating function main
+[wp] [Valid] Goal main_exits (Cfg) (Unreachable)
 [wp] first_loop-2.c:8: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] 5 goals scheduled
+[wp] 6 goals scheduled
+[wp] [Unsuccess] typed_main_terminates (Alt-Ergo) (Cached)
 [wp] [Valid] typed_main_loop_invariant_preserved (Qed)
 [wp] [Valid] typed_main_loop_invariant_established (Qed)
 [wp] [Valid] typed_main_assert_rte_signed_overflow (Qed)
 [wp] [Valid] typed_main_assert (Qed)
 [wp] [Unsuccess] typed_main_assert_2 (Alt-Ergo) (Cached)
-[wp] Proved goals:    4 / 5
+[wp] Proved goals:    5 / 7
+  Unreachable:     1
   Qed:             4
-  Unsuccess:       1
+  Unsuccess:       2
 [wp:pedantic-assigns] first_loop-2.c:1: Warning: 
   No 'assigns' specification for function 'main'.
   Callers assumptions might be imprecise.

code/statements/loops/oracle/first_loop-3.res.oracle

@@ -2,15 +2,19 @@
 [kernel] Parsing first_loop-3.c (with preprocessing)
 [wp] Running WP plugin...
 [rte:annot] annotating function main
-[wp] 6 goals scheduled
+[wp] [Valid] Goal main_exits (Cfg) (Unreachable)
+[wp] 7 goals scheduled
+[wp] [Unsuccess] typed_main_terminates (Alt-Ergo) (Cached)
 [wp] [Valid] typed_main_loop_invariant_preserved (Qed)
 [wp] [Valid] typed_main_loop_invariant_established (Qed)
 [wp] [Valid] typed_main_assert_rte_signed_overflow (Qed)
 [wp] [Valid] typed_main_assert (Qed)
 [wp] [Valid] typed_main_assert_2 (Qed)
 [wp] [Valid] typed_main_loop_assigns (Qed)
-[wp] Proved goals:    6 / 6
+[wp] Proved goals:    7 / 8
+  Unreachable:     1
   Qed:             6
+  Unsuccess:       1
 [wp:pedantic-assigns] first_loop-3.c:1: Warning: 
   No 'assigns' specification for function 'main'.
   Callers assumptions might be imprecise.

code/statements/loops/oracle/infinite.res.oracle

@@ -2,10 +2,15 @@
 [kernel] Parsing infinite.c (with preprocessing)
 [wp] Running WP plugin...
 [rte:annot] annotating function foo
-[wp] [CFG] Goal foo_assert : Valid (Unreachable)
-[wp] Warning: No goal generated
-[wp] Proved goals:    1 / 1
-  Unreachable:     1
+[wp] [Valid] Goal foo_assert (Cfg) (Unreachable)
+[wp] [Valid] Goal foo_exits (Cfg) (Unreachable)
+[wp] infinite.c:2: Warning: 
+  Missing assigns clause (assigns 'everything' instead)
+[wp] 1 goal scheduled
+[wp] [Unsuccess] typed_foo_terminates (Alt-Ergo) (Cached)
+[wp] Proved goals:    2 / 3
+  Unreachable:     2
+  Unsuccess:       1
 [wp:pedantic-assigns] infinite.c:1: Warning: 
   No 'assigns' specification for function 'foo'.
   Callers assumptions might be imprecise.

english/statements/function-calls.tex

@@ -362,7 +362,8 @@
 We can see that the function and the assertion are proved. And indeed the
 proof is correct: we consider partial correctness, and we face a function
 that does not terminate: anything that follows a call to this function would
-be true.
+be true. But again, we have a watchdog: the \CodeInline{terminates} clause is
+not proved.
 
 
 Thus, the question is: what could we do in such a case? Again, we could use
@@ -471,6 +472,7 @@
 
 
 \levelThreeTitle{Specifying and proving function termination}
+\label{l3:statements-function-calls-terminates}
 
 
 A desirable property for a function is often that it should terminate. Indeed,
@@ -532,16 +534,13 @@
 \begin{Information}
   In ACSL, it is specified that when a function does not have a
   \CodeInline{terminates} clause, the default is
-  \CodeInline{terminates \textbackslash{}true}, however it is still not
-  implemented by the Frama-C kernel. This behavior can be enabled in WP
-  by using the options:
+  \CodeInline{terminates \textbackslash{}true}. This behavior is automatically
+  enabled by WP at the kernel level. Thus, when WP starts the verification of
+  a function, it asks the kernel to generate these annotations. This behavior
+  can be disabled \textbf{for user defined functions} using the kernel option:
   \begin{itemize}
-  \item \CodeInline{-wp-definitions-terminate} (for functions with definition),
-  \item \CodeInline{-wp-declarations-terminate} (for functions without definition),
-  \item \CodeInline{-wp-frama-c-stdlib-terminate} (for functions of the Frama-C stdlib),
+    \item \CodeInline{-generated-spec-custom terminates:skip}
   \end{itemize}
-  to claim that, unless a clause is provided, they must terminate (and thus
-  for functions with a definition, the verification must be performed).
 \end{Information}
 
 
@@ -625,23 +624,6 @@
 Where the first call termination is indeed verified while the second is not.
 
 
-When the called function does not have a \CodeInline{terminates} clause, it
-is considered to be \CodeInline{\textbackslash{}false}, that is: unless a
-\CodeInline{terminates} clause is provided, the function may not terminate.
-
-
-For example with our previous \CodeInline{simple} function, we get the message
-``Missing terminates clause on call to call, defaults to \textbackslash{}false''
-and we fail to prove termination:
-
-
-\image{simple_terminates_fails}
-
-
-Note that the formula $\mathtt{r} > 0 \Rightarrow false$ is translated into
-$\mathtt{r} <= 0$.
-
-
 \paragraph{Loop variant}
 
 
@@ -710,16 +692,6 @@
 \CodeBlockInput[53][60]{c}{terminates.c}
 
 
-\begin{Information}
-  When a function under proof does not have \CodeInline{terminates}
-  specification, whenever a verification condition needs it, the clause is
-  considered to be \CodeInline{\textbackslash{}true} since it makes sure that
-  we have more things to prove. For example, when the option
-  \CodeInline{-wp-variant-with-terminates} is used and a function contains a
-  \CodeInline{loop variant}, it guarantees that WP tries to prove it.
-\end{Information}
-
-
 \levelThreeTitle{Exercises}