Update tests

Author: arnaudgolfouse

tests/creusot-contracts/creusot-contracts.coma

@@ -20,7 +20,7 @@ module M_01_resolve_unsoundness__make_vec_of_size [#"01_resolve_unsoundness.rs"
   let%span sord'9 = "../../../creusot-contracts/src/logic/ord.rs" 167 40 167 73
   let%span sord'10 = "../../../creusot-contracts/src/logic/ord.rs" 168 39 168 69
   let%span sord'11 = "../../../creusot-contracts/src/logic/ord.rs" 173 39 173 84
-  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 230 16 236 17
+  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 260 16 266 17
   let%span smodel = "../../../creusot-contracts/src/model.rs" 62 8 62 22
 
   use creusot.prelude.Opaque

tests/creusot-contracts/creusot-contracts/why3session.xml

@@ -2,9 +2,13 @@ module M_1204__evil [#"1204.rs" 8 0 8 22]
   let%span s1204 = "1204.rs" 6 11 6 16
   let%span s1204'0 = "1204.rs" 7 10 7 11
   let%span s1204'1 = "1204.rs" 9 4 9 16
+  let%span swell_founded = "../../../creusot-contracts/src/well_founded.rs" 44 8 44 33
 
   use mach.int.Int
 
+  predicate well_founded_relation (self: int) (other: int) =
+    [%#swell_founded] self >= 0 /\ self > other
+  
   meta "compute_max_steps" 1000000
 
   meta "select_lsinst" "all"
@@ -14,7 +18,7 @@ module M_1204__evil [#"1204.rs" 8 0 8 22]
   function evil [#"1204.rs" 8 0 8 22] (x'0: int) : int
 
   goal vc_evil: ([%#s1204] false)
-   -> ([@expl:evil requires] [%#s1204] false) /\ 0 <= ([%#s1204'0] x) /\ ([%#s1204'0] - x) < ([%#s1204'0] x)
+   -> ([@expl:evil requires] [%#s1204] false) /\ well_founded_relation ([%#s1204'0] x) ([%#s1204'0] - x)
 end
 module M_1204__wrong [#"1204.rs" 14 0 14 10]
   let%span s1204 = "1204.rs" 13 10 13 15

tests/should_fail/bug/01_resolve_unsoundness.coma

@@ -130,7 +130,7 @@ module M_692__valid_normal [#"692.rs" 12 0 12 34]
   let%span sord'9 = "../../../creusot-contracts/src/logic/ord.rs" 167 40 167 73
   let%span sord'10 = "../../../creusot-contracts/src/logic/ord.rs" 168 39 168 69
   let%span sord'11 = "../../../creusot-contracts/src/logic/ord.rs" 173 39 173 84
-  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 230 16 236 17
+  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 260 16 266 17
   let%span sresolve = "../../../creusot-contracts/src/resolve.rs" 49 20 49 34
 
   use creusot.int.UInt32

tests/should_fail/bug/1204.coma

@@ -172,7 +172,7 @@ module M_695__valid [#"695.rs" 12 0 12 27]
   let%span sord'9 = "../../../creusot-contracts/src/logic/ord.rs" 167 40 167 73
   let%span sord'10 = "../../../creusot-contracts/src/logic/ord.rs" 168 39 168 69
   let%span sord'11 = "../../../creusot-contracts/src/logic/ord.rs" 173 39 173 84
-  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 230 16 236 17
+  let%span sord'12 = "../../../creusot-contracts/src/logic/ord.rs" 260 16 266 17
   let%span sresolve = "../../../creusot-contracts/src/resolve.rs" 49 20 49 34
 
   use creusot.int.UInt32

tests/should_fail/bug/1204/why3shapes.gz

@@ -18,10 +18,10 @@ module M_generic_deref_ghost__deref_wrap [#"generic_deref_ghost.rs" 8 0 8 48]
 
   use creusot.prelude.Any
 
-  type t_Target
-  
   type t_T
 
+  type t_Target
+  
   predicate precondition (self: ()) (args: t_T)
 
   axiom precondition_fndef: [%#sgeneric_deref_ghost'3] forall args: t_T [precondition () args]. (let self_ = args in false)

tests/should_fail/bug/692.coma

@@ -18,10 +18,10 @@ module M_generic_deref_snap__deref_wrap [#"generic_deref_snap.rs" 8 0 8 48]
 
   use creusot.prelude.Any
 
-  type t_Target
-  
   type t_T
 
+  type t_Target
+  
   predicate precondition (self: ()) (args: t_T)
 
   axiom precondition_fndef: [%#sgeneric_deref_snap'3] forall args: t_T [precondition () args]. (let self_ = args in false)

tests/should_fail/bug/695.coma

@@ -14,15 +14,15 @@ error: cannot use `return` in ghost code
    |
    = note: control flow cannot escape the `ghost!` block
 
-error: cannot use `break` in ghost code
+error: cannot `break` to an outer loop in ghost code
   --> control_flow.rs:21:13
    |
 21 |             break;
    |             ^^^^^
    |
    = note: control flow cannot escape the `ghost!` block
 
-error: cannot use `continue` in ghost code
+error: cannot `continue` to an outer loop in ghost code
   --> control_flow.rs:29:13
    |
 29 |             continue;