diff --git a/creusot/tests/should_succeed/bug/vcgen.coma b/creusot/tests/should_succeed/bug/vcgen.coma index c03e4dbec..377e96183 100644 --- a/creusot/tests/should_succeed/bug/vcgen.coma +++ b/creusot/tests/should_succeed/bug/vcgen.coma @@ -4,8 +4,8 @@ module M_vcgen__set_max [#"vcgen.rs" 10 0 10 42] let%span svcgen2 = "vcgen.rs" 9 10 9 53 let%span svcgen3 = "vcgen.rs" 7 10 7 17 let%span svcgen4 = "vcgen.rs" 4 0 4 8 - let%span sfset5 = "../../../../creusot-contracts/src/logic/fset.rs" 46 8 46 26 - let%span sfset6 = "../../../../creusot-contracts/src/logic/fset.rs" 92 8 92 26 + let%span sfset5 = "../../../../creusot-contracts/src/logic/fset.rs" 47 8 47 26 + let%span sfset6 = "../../../../creusot-contracts/src/logic/fset.rs" 93 8 93 26 use set.Fset diff --git a/creusot/tests/should_succeed/cc/collections.coma b/creusot/tests/should_succeed/cc/collections.coma index cca6c0ba8..625db4bd2 100644 --- a/creusot/tests/should_succeed/cc/collections.coma +++ b/creusot/tests/should_succeed/cc/collections.coma @@ -7,9 +7,9 @@ module M_collections__roundtrip_hashmap_into_iter [#"collections.rs" 15 0 17 18] let%span siter5 = "../../../../creusot-contracts/src/std/iter.rs" 166 26 167 120 let%span shash_map6 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 73 20 73 54 let%span shash_map7 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 56 12 66 29 - let%span sfmap8 = "../../../../creusot-contracts/src/logic/fmap.rs" 92 8 95 9 + let%span sfmap8 = "../../../../creusot-contracts/src/logic/fmap.rs" 93 8 96 9 let%span sseq9 = "../../../../creusot-contracts/src/logic/seq.rs" 355 20 355 77 - let%span sfmap10 = "../../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35 + let%span sfmap10 = "../../../../creusot-contracts/src/logic/fmap.rs" 133 8 133 35 let%span shash_map11 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 199 20 199 24 let%span shash_map12 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 205 20 205 33 let%span shash_map13 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 245 20 247 86 @@ -21,15 +21,15 @@ module M_collections__roundtrip_hashmap_into_iter [#"collections.rs" 15 0 17 18] let%span shash_map19 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 87 8 87 104 let%span sresolve20 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span smodel21 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 - let%span sfmap22 = "../../../../creusot-contracts/src/logic/fmap.rs" 139 8 139 34 - let%span sfmap23 = "../../../../creusot-contracts/src/logic/fmap.rs" 48 14 48 25 - let%span sfmap24 = "../../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 - let%span sfmap25 = "../../../../creusot-contracts/src/logic/fmap.rs" 39 14 39 31 - let%span sfmap26 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 49 - let%span sfmap27 = "../../../../creusot-contracts/src/logic/fmap.rs" 214 14 214 38 - let%span sfmap28 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 83 - let%span sfmap29 = "../../../../creusot-contracts/src/logic/fmap.rs" 217 8 217 35 - let%span sfmap30 = "../../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86 + let%span sfmap22 = "../../../../creusot-contracts/src/logic/fmap.rs" 140 8 140 34 + let%span sfmap23 = "../../../../creusot-contracts/src/logic/fmap.rs" 49 14 49 25 + let%span sfmap24 = "../../../../creusot-contracts/src/logic/fmap.rs" 104 8 104 26 + let%span sfmap25 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 31 + let%span sfmap26 = "../../../../creusot-contracts/src/logic/fmap.rs" 41 14 41 49 + let%span sfmap27 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 38 + let%span sfmap28 = "../../../../creusot-contracts/src/logic/fmap.rs" 216 14 216 83 + let%span sfmap29 = "../../../../creusot-contracts/src/logic/fmap.rs" 218 8 218 35 + let%span sfmap30 = "../../../../creusot-contracts/src/logic/fmap.rs" 59 14 59 86 use prelude.prelude.UInt64 @@ -374,7 +374,7 @@ module M_collections__roundtrip_hashmap_iter [#"collections.rs" 32 0 32 97] let%span siter4 = "../../../../creusot-contracts/src/std/iter.rs" 166 26 167 120 let%span shash_map5 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 125 20 125 54 let%span shash_map6 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 108 12 118 29 - let%span sfmap7 = "../../../../creusot-contracts/src/logic/fmap.rs" 92 8 95 9 + let%span sfmap7 = "../../../../creusot-contracts/src/logic/fmap.rs" 93 8 96 9 let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sseq9 = "../../../../creusot-contracts/src/logic/seq.rs" 355 20 355 77 let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 @@ -387,15 +387,15 @@ module M_collections__roundtrip_hashmap_iter [#"collections.rs" 32 0 32 97] let%span shash_map17 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 139 8 139 104 let%span sresolve18 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span smodel19 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 - let%span sfmap20 = "../../../../creusot-contracts/src/logic/fmap.rs" 139 8 139 34 - let%span sfmap21 = "../../../../creusot-contracts/src/logic/fmap.rs" 48 14 48 25 - let%span sfmap22 = "../../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 - let%span sfmap23 = "../../../../creusot-contracts/src/logic/fmap.rs" 39 14 39 31 - let%span sfmap24 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 49 - let%span sfmap25 = "../../../../creusot-contracts/src/logic/fmap.rs" 214 14 214 38 - let%span sfmap26 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 83 - let%span sfmap27 = "../../../../creusot-contracts/src/logic/fmap.rs" 217 8 217 35 - let%span sfmap28 = "../../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86 + let%span sfmap20 = "../../../../creusot-contracts/src/logic/fmap.rs" 140 8 140 34 + let%span sfmap21 = "../../../../creusot-contracts/src/logic/fmap.rs" 49 14 49 25 + let%span sfmap22 = "../../../../creusot-contracts/src/logic/fmap.rs" 104 8 104 26 + let%span sfmap23 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 31 + let%span sfmap24 = "../../../../creusot-contracts/src/logic/fmap.rs" 41 14 41 49 + let%span sfmap25 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 38 + let%span sfmap26 = "../../../../creusot-contracts/src/logic/fmap.rs" 216 14 216 83 + let%span sfmap27 = "../../../../creusot-contracts/src/logic/fmap.rs" 218 8 218 35 + let%span sfmap28 = "../../../../creusot-contracts/src/logic/fmap.rs" 59 14 59 86 use prelude.prelude.Borrow @@ -694,12 +694,12 @@ module M_collections__roundtrip_hashmap_iter_mut [#"collections.rs" 48 0 50 24] let%span siter6 = "../../../../creusot-contracts/src/std/iter.rs" 166 26 167 120 let%span shash_map7 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 177 20 177 54 let%span shash_map8 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 160 12 170 29 - let%span sfmap9 = "../../../../creusot-contracts/src/logic/fmap.rs" 92 8 95 9 + let%span sfmap9 = "../../../../creusot-contracts/src/logic/fmap.rs" 93 8 96 9 let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sseq11 = "../../../../creusot-contracts/src/logic/seq.rs" 355 20 355 77 let%span smodel12 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 - let%span sfmap13 = "../../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35 - let%span sfmap14 = "../../../../creusot-contracts/src/logic/fmap.rs" 228 8 228 24 + let%span sfmap13 = "../../../../creusot-contracts/src/logic/fmap.rs" 133 8 133 35 + let%span sfmap14 = "../../../../creusot-contracts/src/logic/fmap.rs" 229 8 229 24 let%span shash_map15 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 233 20 235 112 let%span shash_map16 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 245 20 247 86 let%span shash_map17 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 182 14 182 45 @@ -709,17 +709,17 @@ module M_collections__roundtrip_hashmap_iter_mut [#"collections.rs" 48 0 50 24] let%span shash_map21 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 189 14 189 42 let%span shash_map22 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 191 8 191 104 let%span sresolve23 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span sfmap24 = "../../../../creusot-contracts/src/logic/fmap.rs" 139 8 139 34 - let%span sfmap25 = "../../../../creusot-contracts/src/logic/fmap.rs" 48 14 48 25 - let%span sfmap26 = "../../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 - let%span sfmap27 = "../../../../creusot-contracts/src/logic/fmap.rs" 116 9 116 31 - let%span sfmap28 = "../../../../creusot-contracts/src/logic/fmap.rs" 39 14 39 31 - let%span sfmap29 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 49 - let%span sfmap30 = "../../../../creusot-contracts/src/logic/fmap.rs" 214 14 214 38 - let%span sfmap31 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 83 - let%span sfmap32 = "../../../../creusot-contracts/src/logic/fmap.rs" 217 8 217 35 - let%span sfmap33 = "../../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86 - let%span sfmap34 = "../../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35 + let%span sfmap24 = "../../../../creusot-contracts/src/logic/fmap.rs" 140 8 140 34 + let%span sfmap25 = "../../../../creusot-contracts/src/logic/fmap.rs" 49 14 49 25 + let%span sfmap26 = "../../../../creusot-contracts/src/logic/fmap.rs" 104 8 104 26 + let%span sfmap27 = "../../../../creusot-contracts/src/logic/fmap.rs" 117 9 117 31 + let%span sfmap28 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 31 + let%span sfmap29 = "../../../../creusot-contracts/src/logic/fmap.rs" 41 14 41 49 + let%span sfmap30 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 38 + let%span sfmap31 = "../../../../creusot-contracts/src/logic/fmap.rs" 216 14 216 83 + let%span sfmap32 = "../../../../creusot-contracts/src/logic/fmap.rs" 218 8 218 35 + let%span sfmap33 = "../../../../creusot-contracts/src/logic/fmap.rs" 59 14 59 86 + let%span sfmap34 = "../../../../creusot-contracts/src/logic/fmap.rs" 125 8 125 35 let%span sutil35 = "../../../../creusot-contracts/src/util.rs" 55 11 55 21 let%span sutil36 = "../../../../creusot-contracts/src/util.rs" 56 10 56 28 @@ -1083,7 +1083,7 @@ module M_collections__roundtrip_hashset_into_iter [#"collections.rs" 64 0 64 90] let%span shash_set13 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 110 8 110 43 let%span smodel14 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span shash_set15 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 58 16 65 23 - let%span sfset16 = "../../../../creusot-contracts/src/logic/fset.rs" 46 8 46 26 + let%span sfset16 = "../../../../creusot-contracts/src/logic/fset.rs" 47 8 47 26 let%span sseq17 = "../../../../creusot-contracts/src/logic/seq.rs" 355 20 355 77 let%span shash_set18 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 71 11 71 33 let%span shash_set19 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 72 11 72 33 @@ -1386,7 +1386,7 @@ module M_collections__roundtrip_hashset_iter [#"collections.rs" 69 0 69 87] let%span shash_set12 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 149 8 149 43 let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span shash_set14 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 58 16 65 23 - let%span sfset15 = "../../../../creusot-contracts/src/logic/fset.rs" 46 8 46 26 + let%span sfset15 = "../../../../creusot-contracts/src/logic/fset.rs" 47 8 47 26 let%span smodel16 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sseq17 = "../../../../creusot-contracts/src/logic/seq.rs" 355 20 355 77 let%span shash_set18 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 71 11 71 33 @@ -1629,7 +1629,7 @@ module M_collections__hashset_intersection [#"collections.rs" 74 0 77 15] let%span scopied13 = "../../../../creusot-contracts/src/std/iter/copied.rs" 64 14 64 42 let%span shash_set14 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 210 20 210 56 let%span shash_set15 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 204 8 204 38 - let%span sfset16 = "../../../../creusot-contracts/src/logic/fset.rs" 46 8 46 26 + let%span sfset16 = "../../../../creusot-contracts/src/logic/fset.rs" 47 8 47 26 let%span sseq17 = "../../../../creusot-contracts/src/logic/seq.rs" 355 20 355 77 let%span shash_set18 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 215 14 215 45 let%span shash_set19 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 213 4 213 10 diff --git a/creusot/tests/should_succeed/fmap_indexing.coma b/creusot/tests/should_succeed/fmap_indexing.coma index a16cb2939..fa1a80f18 100644 --- a/creusot/tests/should_succeed/fmap_indexing.coma +++ b/creusot/tests/should_succeed/fmap_indexing.coma @@ -6,19 +6,19 @@ module M_fmap_indexing__foo [#"fmap_indexing.rs" 4 0 4 12] let%span sfmap_indexing4 = "fmap_indexing.rs" 9 18 9 45 let%span sfmap_indexing5 = "fmap_indexing.rs" 10 10 10 37 let%span sfmap_indexing6 = "fmap_indexing.rs" 11 18 11 45 - let%span sfmap7 = "../../../creusot-contracts/src/logic/fmap.rs" 39 14 39 31 - let%span sfmap8 = "../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 49 - let%span sfmap9 = "../../../creusot-contracts/src/logic/fmap.rs" 66 14 66 71 - let%span sfmap10 = "../../../creusot-contracts/src/logic/fmap.rs" 67 14 67 61 - let%span sfmap11 = "../../../creusot-contracts/src/logic/fmap.rs" 68 14 68 66 - let%span sfmap12 = "../../../creusot-contracts/src/logic/fmap.rs" 228 8 228 24 - let%span sfmap13 = "../../../creusot-contracts/src/logic/fmap.rs" 48 14 48 25 - let%span sfmap14 = "../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86 + let%span sfmap7 = "../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 31 + let%span sfmap8 = "../../../creusot-contracts/src/logic/fmap.rs" 41 14 41 49 + let%span sfmap9 = "../../../creusot-contracts/src/logic/fmap.rs" 67 14 67 71 + let%span sfmap10 = "../../../creusot-contracts/src/logic/fmap.rs" 68 14 68 61 + let%span sfmap11 = "../../../creusot-contracts/src/logic/fmap.rs" 69 14 69 66 + let%span sfmap12 = "../../../creusot-contracts/src/logic/fmap.rs" 229 8 229 24 + let%span sfmap13 = "../../../creusot-contracts/src/logic/fmap.rs" 49 14 49 25 + let%span sfmap14 = "../../../creusot-contracts/src/logic/fmap.rs" 59 14 59 86 let%span sutil15 = "../../../creusot-contracts/src/util.rs" 21 14 21 30 - let%span sfmap16 = "../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35 - let%span sfmap17 = "../../../creusot-contracts/src/logic/fmap.rs" 116 9 116 31 - let%span sfmap18 = "../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 - let%span sfmap19 = "../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35 + let%span sfmap16 = "../../../creusot-contracts/src/logic/fmap.rs" 133 8 133 35 + let%span sfmap17 = "../../../creusot-contracts/src/logic/fmap.rs" 117 9 117 31 + let%span sfmap18 = "../../../creusot-contracts/src/logic/fmap.rs" 104 8 104 26 + let%span sfmap19 = "../../../creusot-contracts/src/logic/fmap.rs" 125 8 125 35 let%span sutil20 = "../../../creusot-contracts/src/util.rs" 55 11 55 21 let%span sutil21 = "../../../creusot-contracts/src/util.rs" 56 10 56 28 diff --git a/creusot/tests/should_succeed/ghost/ghost_map.coma b/creusot/tests/should_succeed/ghost/ghost_map.coma index 90e4d6a56..ee4671809 100644 --- a/creusot/tests/should_succeed/ghost/ghost_map.coma +++ b/creusot/tests/should_succeed/ghost/ghost_map.coma @@ -1,7 +1,7 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] let%span sghost_map0 = "ghost_map.rs" 5 18 5 41 - let%span sfmap1 = "../../../../creusot-contracts/src/logic/fmap.rs" 239 4 239 34 - let%span sfmap2 = "../../../../creusot-contracts/src/logic/fmap.rs" 237 14 237 31 + let%span sfmap1 = "../../../../creusot-contracts/src/logic/fmap.rs" 240 4 240 34 + let%span sfmap2 = "../../../../creusot-contracts/src/logic/fmap.rs" 238 14 238 31 let%span sghost_map3 = "ghost_map.rs" 7 22 7 53 let%span sghost_map4 = "ghost_map.rs" 8 25 8 26 let%span sghost_map5 = "ghost_map.rs" 8 28 8 30 @@ -32,60 +32,60 @@ module M_ghost_map__ghost_map [#"ghost_map.rs" 4 0 4 18] let%span sghost_map30 = "ghost_map.rs" 46 22 46 34 let%span sghost_map31 = "ghost_map.rs" 47 22 47 34 let%span sghost32 = "../../../../creusot-contracts/src/ghost.rs" 217 9 217 15 - let%span sfmap33 = "../../../../creusot-contracts/src/logic/fmap.rs" 139 8 139 34 - let%span sfmap34 = "../../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35 + let%span sfmap33 = "../../../../creusot-contracts/src/logic/fmap.rs" 140 8 140 34 + let%span sfmap34 = "../../../../creusot-contracts/src/logic/fmap.rs" 133 8 133 35 let%span sghost35 = "../../../../creusot-contracts/src/ghost.rs" 85 22 85 26 let%span sghost36 = "../../../../creusot-contracts/src/ghost.rs" 85 4 85 48 let%span sghost37 = "../../../../creusot-contracts/src/ghost.rs" 84 14 84 36 - let%span sfmap38 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 29 376 33 - let%span sfmap39 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 35 376 38 - let%span sfmap40 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 43 376 48 - let%span sfmap41 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 4 378 17 - let%span sfmap42 = "../../../../creusot-contracts/src/logic/fmap.rs" 374 14 374 49 - let%span sfmap43 = "../../../../creusot-contracts/src/logic/fmap.rs" 375 14 375 40 + let%span sfmap38 = "../../../../creusot-contracts/src/logic/fmap.rs" 377 29 377 33 + let%span sfmap39 = "../../../../creusot-contracts/src/logic/fmap.rs" 377 35 377 38 + let%span sfmap40 = "../../../../creusot-contracts/src/logic/fmap.rs" 377 43 377 48 + let%span sfmap41 = "../../../../creusot-contracts/src/logic/fmap.rs" 377 4 379 17 + let%span sfmap42 = "../../../../creusot-contracts/src/logic/fmap.rs" 375 14 375 49 + let%span sfmap43 = "../../../../creusot-contracts/src/logic/fmap.rs" 376 14 376 40 let%span sghost44 = "../../../../creusot-contracts/src/ghost.rs" 69 14 69 18 let%span sghost45 = "../../../../creusot-contracts/src/ghost.rs" 69 4 69 36 let%span sghost46 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35 - let%span sfmap47 = "../../../../creusot-contracts/src/logic/fmap.rs" 265 22 265 26 - let%span sfmap48 = "../../../../creusot-contracts/src/logic/fmap.rs" 264 14 264 34 - let%span sfmap49 = "../../../../creusot-contracts/src/logic/fmap.rs" 116 9 116 31 - let%span sfmap50 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 30 348 34 - let%span sfmap51 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 36 348 39 - let%span sfmap52 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 4 348 62 - let%span sfmap53 = "../../../../creusot-contracts/src/logic/fmap.rs" 336 4 345 11 - let%span sfmap54 = "../../../../creusot-contracts/src/logic/fmap.rs" 346 14 346 89 - let%span sfmap55 = "../../../../creusot-contracts/src/logic/fmap.rs" 347 14 347 44 - let%span sfmap56 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 29 415 33 - let%span sfmap57 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 35 415 38 - let%span sfmap58 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 4 417 17 - let%span sfmap59 = "../../../../creusot-contracts/src/logic/fmap.rs" 413 14 413 43 - let%span sfmap60 = "../../../../creusot-contracts/src/logic/fmap.rs" 414 14 414 41 - let%span sfmap61 = "../../../../creusot-contracts/src/logic/fmap.rs" 92 8 95 9 - let%span sfmap62 = "../../../../creusot-contracts/src/logic/fmap.rs" 285 27 285 31 - let%span sfmap63 = "../../../../creusot-contracts/src/logic/fmap.rs" 285 33 285 36 - let%span sfmap64 = "../../../../creusot-contracts/src/logic/fmap.rs" 284 14 284 43 - let%span sfmap65 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 22 314 26 - let%span sfmap66 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 28 314 31 - let%span sfmap67 = "../../../../creusot-contracts/src/logic/fmap.rs" 314 4 314 50 - let%span sfmap68 = "../../../../creusot-contracts/src/logic/fmap.rs" 306 4 313 11 + let%span sfmap47 = "../../../../creusot-contracts/src/logic/fmap.rs" 266 22 266 26 + let%span sfmap48 = "../../../../creusot-contracts/src/logic/fmap.rs" 265 14 265 34 + let%span sfmap49 = "../../../../creusot-contracts/src/logic/fmap.rs" 117 9 117 31 + let%span sfmap50 = "../../../../creusot-contracts/src/logic/fmap.rs" 349 30 349 34 + let%span sfmap51 = "../../../../creusot-contracts/src/logic/fmap.rs" 349 36 349 39 + let%span sfmap52 = "../../../../creusot-contracts/src/logic/fmap.rs" 349 4 349 62 + let%span sfmap53 = "../../../../creusot-contracts/src/logic/fmap.rs" 337 4 346 11 + let%span sfmap54 = "../../../../creusot-contracts/src/logic/fmap.rs" 347 14 347 89 + let%span sfmap55 = "../../../../creusot-contracts/src/logic/fmap.rs" 348 14 348 44 + let%span sfmap56 = "../../../../creusot-contracts/src/logic/fmap.rs" 416 29 416 33 + let%span sfmap57 = "../../../../creusot-contracts/src/logic/fmap.rs" 416 35 416 38 + let%span sfmap58 = "../../../../creusot-contracts/src/logic/fmap.rs" 416 4 418 17 + let%span sfmap59 = "../../../../creusot-contracts/src/logic/fmap.rs" 414 14 414 43 + let%span sfmap60 = "../../../../creusot-contracts/src/logic/fmap.rs" 415 14 415 41 + let%span sfmap61 = "../../../../creusot-contracts/src/logic/fmap.rs" 93 8 96 9 + let%span sfmap62 = "../../../../creusot-contracts/src/logic/fmap.rs" 286 27 286 31 + let%span sfmap63 = "../../../../creusot-contracts/src/logic/fmap.rs" 286 33 286 36 + let%span sfmap64 = "../../../../creusot-contracts/src/logic/fmap.rs" 285 14 285 43 + let%span sfmap65 = "../../../../creusot-contracts/src/logic/fmap.rs" 315 22 315 26 + let%span sfmap66 = "../../../../creusot-contracts/src/logic/fmap.rs" 315 28 315 31 + let%span sfmap67 = "../../../../creusot-contracts/src/logic/fmap.rs" 315 4 315 50 + let%span sfmap68 = "../../../../creusot-contracts/src/logic/fmap.rs" 307 4 314 11 let%span sghost69 = "../../../../creusot-contracts/src/ghost.rs" 181 15 181 16 let%span sghost70 = "../../../../creusot-contracts/src/ghost.rs" 181 4 181 28 let%span sghost71 = "../../../../creusot-contracts/src/ghost.rs" 179 14 179 28 - let%span sfmap72 = "../../../../creusot-contracts/src/logic/fmap.rs" 39 14 39 31 - let%span sfmap73 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 49 - let%span sfmap74 = "../../../../creusot-contracts/src/logic/fmap.rs" 214 14 214 38 - let%span sfmap75 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 83 - let%span sfmap76 = "../../../../creusot-contracts/src/logic/fmap.rs" 217 8 217 35 - let%span sfmap77 = "../../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 - let%span sfmap78 = "../../../../creusot-contracts/src/logic/fmap.rs" 66 14 66 71 - let%span sfmap79 = "../../../../creusot-contracts/src/logic/fmap.rs" 67 14 67 61 - let%span sfmap80 = "../../../../creusot-contracts/src/logic/fmap.rs" 68 14 68 66 + let%span sfmap72 = "../../../../creusot-contracts/src/logic/fmap.rs" 40 14 40 31 + let%span sfmap73 = "../../../../creusot-contracts/src/logic/fmap.rs" 41 14 41 49 + let%span sfmap74 = "../../../../creusot-contracts/src/logic/fmap.rs" 215 14 215 38 + let%span sfmap75 = "../../../../creusot-contracts/src/logic/fmap.rs" 216 14 216 83 + let%span sfmap76 = "../../../../creusot-contracts/src/logic/fmap.rs" 218 8 218 35 + let%span sfmap77 = "../../../../creusot-contracts/src/logic/fmap.rs" 104 8 104 26 + let%span sfmap78 = "../../../../creusot-contracts/src/logic/fmap.rs" 67 14 67 71 + let%span sfmap79 = "../../../../creusot-contracts/src/logic/fmap.rs" 68 14 68 61 + let%span sfmap80 = "../../../../creusot-contracts/src/logic/fmap.rs" 69 14 69 66 let%span sresolve81 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span sfmap82 = "../../../../creusot-contracts/src/logic/fmap.rs" 48 14 48 25 - let%span sfmap83 = "../../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35 - let%span sfmap84 = "../../../../creusot-contracts/src/logic/fmap.rs" 76 14 76 55 - let%span sfmap85 = "../../../../creusot-contracts/src/logic/fmap.rs" 77 14 77 84 - let%span sfmap86 = "../../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86 + let%span sfmap82 = "../../../../creusot-contracts/src/logic/fmap.rs" 49 14 49 25 + let%span sfmap83 = "../../../../creusot-contracts/src/logic/fmap.rs" 125 8 125 35 + let%span sfmap84 = "../../../../creusot-contracts/src/logic/fmap.rs" 77 14 77 55 + let%span sfmap85 = "../../../../creusot-contracts/src/logic/fmap.rs" 78 14 78 84 + let%span sfmap86 = "../../../../creusot-contracts/src/logic/fmap.rs" 59 14 59 86 let%span sutil87 = "../../../../creusot-contracts/src/util.rs" 21 14 21 30 let%span sutil88 = "../../../../creusot-contracts/src/util.rs" 55 11 55 21 let%span sutil89 = "../../../../creusot-contracts/src/util.rs" 56 10 56 28 diff --git a/creusot/tests/should_succeed/ghost/ghost_set.coma b/creusot/tests/should_succeed/ghost/ghost_set.coma index 715ebc53b..52fc0b1e0 100644 --- a/creusot/tests/should_succeed/ghost/ghost_set.coma +++ b/creusot/tests/should_succeed/ghost/ghost_set.coma @@ -1,7 +1,7 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] let%span sghost_set0 = "ghost_set.rs" 5 18 5 36 - let%span sfset1 = "../../../../creusot-contracts/src/logic/fset.rs" 196 4 196 34 - let%span sfset2 = "../../../../creusot-contracts/src/logic/fset.rs" 194 14 194 31 + let%span sfset1 = "../../../../creusot-contracts/src/logic/fset.rs" 197 4 197 34 + let%span sfset2 = "../../../../creusot-contracts/src/logic/fset.rs" 195 14 195 31 let%span sghost_set3 = "ghost_set.rs" 7 22 7 53 let%span sghost_set4 = "ghost_set.rs" 8 25 8 26 let%span sghost_set5 = "ghost_set.rs" 10 22 10 63 @@ -21,32 +21,32 @@ module M_ghost_set__ghost_map [#"ghost_set.rs" 4 0 4 18] let%span sghost_set19 = "ghost_set.rs" 32 22 32 32 let%span sghost_set20 = "ghost_set.rs" 33 22 33 32 let%span sghost21 = "../../../../creusot-contracts/src/ghost.rs" 217 9 217 15 - let%span sfset22 = "../../../../creusot-contracts/src/logic/fset.rs" 46 8 46 26 + let%span sfset22 = "../../../../creusot-contracts/src/logic/fset.rs" 47 8 47 26 let%span sghost23 = "../../../../creusot-contracts/src/ghost.rs" 85 22 85 26 let%span sghost24 = "../../../../creusot-contracts/src/ghost.rs" 85 4 85 48 let%span sghost25 = "../../../../creusot-contracts/src/ghost.rs" 84 14 84 36 - let%span sfset26 = "../../../../creusot-contracts/src/logic/fset.rs" 277 29 277 33 - let%span sfset27 = "../../../../creusot-contracts/src/logic/fset.rs" 277 35 277 40 - let%span sfset28 = "../../../../creusot-contracts/src/logic/fset.rs" 275 14 275 44 - let%span sfset29 = "../../../../creusot-contracts/src/logic/fset.rs" 276 14 276 48 + let%span sfset26 = "../../../../creusot-contracts/src/logic/fset.rs" 278 29 278 33 + let%span sfset27 = "../../../../creusot-contracts/src/logic/fset.rs" 278 35 278 40 + let%span sfset28 = "../../../../creusot-contracts/src/logic/fset.rs" 276 14 276 44 + let%span sfset29 = "../../../../creusot-contracts/src/logic/fset.rs" 277 14 277 48 let%span sghost30 = "../../../../creusot-contracts/src/ghost.rs" 69 14 69 18 let%span sghost31 = "../../../../creusot-contracts/src/ghost.rs" 69 4 69 36 let%span sghost32 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35 - let%span sfset33 = "../../../../creusot-contracts/src/logic/fset.rs" 222 22 222 26 - let%span sfset34 = "../../../../creusot-contracts/src/logic/fset.rs" 221 14 221 34 - let%span sfset35 = "../../../../creusot-contracts/src/logic/fset.rs" 313 29 313 33 - let%span sfset36 = "../../../../creusot-contracts/src/logic/fset.rs" 313 35 313 40 - let%span sfset37 = "../../../../creusot-contracts/src/logic/fset.rs" 311 14 311 45 - let%span sfset38 = "../../../../creusot-contracts/src/logic/fset.rs" 312 14 312 48 - let%span sfset39 = "../../../../creusot-contracts/src/logic/fset.rs" 243 27 243 31 - let%span sfset40 = "../../../../creusot-contracts/src/logic/fset.rs" 243 33 243 38 - let%span sfset41 = "../../../../creusot-contracts/src/logic/fset.rs" 242 14 242 45 + let%span sfset33 = "../../../../creusot-contracts/src/logic/fset.rs" 223 22 223 26 + let%span sfset34 = "../../../../creusot-contracts/src/logic/fset.rs" 222 14 222 34 + let%span sfset35 = "../../../../creusot-contracts/src/logic/fset.rs" 314 29 314 33 + let%span sfset36 = "../../../../creusot-contracts/src/logic/fset.rs" 314 35 314 40 + let%span sfset37 = "../../../../creusot-contracts/src/logic/fset.rs" 312 14 312 45 + let%span sfset38 = "../../../../creusot-contracts/src/logic/fset.rs" 313 14 313 48 + let%span sfset39 = "../../../../creusot-contracts/src/logic/fset.rs" 244 27 244 31 + let%span sfset40 = "../../../../creusot-contracts/src/logic/fset.rs" 244 33 244 38 + let%span sfset41 = "../../../../creusot-contracts/src/logic/fset.rs" 243 14 243 45 let%span sghost42 = "../../../../creusot-contracts/src/ghost.rs" 181 15 181 16 let%span sghost43 = "../../../../creusot-contracts/src/ghost.rs" 181 4 181 28 let%span sghost44 = "../../../../creusot-contracts/src/ghost.rs" 179 14 179 28 - let%span sfset45 = "../../../../creusot-contracts/src/logic/fset.rs" 65 8 65 26 + let%span sfset45 = "../../../../creusot-contracts/src/logic/fset.rs" 66 8 66 26 let%span sresolve46 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span sfset47 = "../../../../creusot-contracts/src/logic/fset.rs" 92 8 92 26 + let%span sfset47 = "../../../../creusot-contracts/src/logic/fset.rs" 93 8 93 26 use prelude.prelude.Int32