Commit 9e50156a authored by Michael Sammler's avatar Michael Sammler

updated t01_basic

parent 9a1d5386
......@@ -17,79 +17,79 @@ Section code.
Definition loc_14 : location_info := LocationInfo file_0 154 11 154 12.
Definition loc_15 : location_info := LocationInfo file_0 154 11 154 12.
Definition loc_16 : location_info := LocationInfo file_0 154 15 154 16.
Definition loc_19 : location_info := LocationInfo file_0 260 4 264 5.
Definition loc_20 : location_info := LocationInfo file_0 267 4 267 19.
Definition loc_21 : location_info := LocationInfo file_0 268 4 268 19.
Definition loc_22 : location_info := LocationInfo file_0 269 4 269 13.
Definition loc_23 : location_info := LocationInfo file_0 269 11 269 12.
Definition loc_24 : location_info := LocationInfo file_0 269 11 269 12.
Definition loc_25 : location_info := LocationInfo file_0 268 11 268 17.
Definition loc_26 : location_info := LocationInfo file_0 268 11 268 12.
Definition loc_27 : location_info := LocationInfo file_0 268 11 268 12.
Definition loc_28 : location_info := LocationInfo file_0 268 16 268 17.
Definition loc_29 : location_info := LocationInfo file_0 268 16 268 17.
Definition loc_30 : location_info := LocationInfo file_0 267 11 267 17.
Definition loc_31 : location_info := LocationInfo file_0 267 11 267 12.
Definition loc_32 : location_info := LocationInfo file_0 267 11 267 12.
Definition loc_33 : location_info := LocationInfo file_0 267 16 267 17.
Definition loc_34 : location_info := LocationInfo file_0 267 16 267 17.
Definition loc_35 : location_info := LocationInfo file_0 260 14 262 5.
Definition loc_36 : location_info := LocationInfo file_0 261 8 261 14.
Definition loc_37 : location_info := LocationInfo file_0 261 8 261 9.
Definition loc_38 : location_info := LocationInfo file_0 261 12 261 13.
Definition loc_39 : location_info := LocationInfo file_0 261 12 261 13.
Definition loc_40 : location_info := LocationInfo file_0 262 11 264 5.
Definition loc_41 : location_info := LocationInfo file_0 263 8 263 14.
Definition loc_42 : location_info := LocationInfo file_0 263 8 263 9.
Definition loc_43 : location_info := LocationInfo file_0 263 12 263 13.
Definition loc_44 : location_info := LocationInfo file_0 263 12 263 13.
Definition loc_45 : location_info := LocationInfo file_0 260 7 260 12.
Definition loc_46 : location_info := LocationInfo file_0 260 7 260 8.
Definition loc_47 : location_info := LocationInfo file_0 260 7 260 8.
Definition loc_48 : location_info := LocationInfo file_0 260 11 260 12.
Definition loc_49 : location_info := LocationInfo file_0 260 11 260 12.
Definition loc_52 : location_info := LocationInfo file_0 306 4 311 5.
Definition loc_53 : location_info := LocationInfo file_0 312 4 312 13.
Definition loc_54 : location_info := LocationInfo file_0 312 11 312 12.
Definition loc_55 : location_info := LocationInfo file_0 312 11 312 12.
Definition loc_56 : location_info := LocationInfo file_0 306 4 311 5.
Definition loc_57 : location_info := LocationInfo file_0 306 17 311 5.
Definition loc_58 : location_info := LocationInfo file_0 307 8 307 12.
Definition loc_59 : location_info := LocationInfo file_0 310 8 310 12.
Definition loc_60 : location_info := LocationInfo file_0 306 4 311 5.
Definition loc_61 : location_info := LocationInfo file_0 306 4 311 5.
Definition loc_62 : location_info := LocationInfo file_0 310 8 310 9.
Definition loc_63 : location_info := LocationInfo file_0 307 8 307 9.
Definition loc_64 : location_info := LocationInfo file_0 306 10 306 15.
Definition loc_65 : location_info := LocationInfo file_0 306 10 306 11.
Definition loc_66 : location_info := LocationInfo file_0 306 10 306 11.
Definition loc_67 : location_info := LocationInfo file_0 306 14 306 15.
Definition loc_70 : location_info := LocationInfo file_0 402 4 402 13.
Definition loc_71 : location_info := LocationInfo file_0 402 4 402 8.
Definition loc_72 : location_info := LocationInfo file_0 402 5 402 8.
Definition loc_73 : location_info := LocationInfo file_0 402 5 402 8.
Definition loc_74 : location_info := LocationInfo file_0 402 11 402 12.
Definition loc_77 : location_info := LocationInfo file_0 413 2 413 15.
Definition loc_78 : location_info := LocationInfo file_0 414 2 414 15.
Definition loc_79 : location_info := LocationInfo file_0 414 2 414 10.
Definition loc_80 : location_info := LocationInfo file_0 414 2 414 10.
Definition loc_81 : location_info := LocationInfo file_0 414 11 414 13.
Definition loc_82 : location_info := LocationInfo file_0 414 12 414 13.
Definition loc_83 : location_info := LocationInfo file_0 413 2 413 10.
Definition loc_84 : location_info := LocationInfo file_0 413 2 413 10.
Definition loc_85 : location_info := LocationInfo file_0 413 11 413 13.
Definition loc_86 : location_info := LocationInfo file_0 413 12 413 13.
Definition loc_89 : location_info := LocationInfo file_0 434 4 434 34.
Definition loc_90 : location_info := LocationInfo file_0 435 4 435 13.
Definition loc_91 : location_info := LocationInfo file_0 435 4 435 10.
Definition loc_92 : location_info := LocationInfo file_0 435 4 435 7.
Definition loc_93 : location_info := LocationInfo file_0 435 4 435 7.
Definition loc_94 : location_info := LocationInfo file_0 434 4 434 8.
Definition loc_95 : location_info := LocationInfo file_0 434 5 434 8.
Definition loc_96 : location_info := LocationInfo file_0 434 5 434 8.
Definition loc_97 : location_info := LocationInfo file_0 434 11 434 33.
Definition loc_98 : location_info := LocationInfo file_0 434 11 434 33.
Definition loc_101 : location_info := LocationInfo file_0 434 31 434 32.
Definition loc_19 : location_info := LocationInfo file_0 256 4 260 5.
Definition loc_20 : location_info := LocationInfo file_0 263 4 263 19.
Definition loc_21 : location_info := LocationInfo file_0 264 4 264 19.
Definition loc_22 : location_info := LocationInfo file_0 265 4 265 13.
Definition loc_23 : location_info := LocationInfo file_0 265 11 265 12.
Definition loc_24 : location_info := LocationInfo file_0 265 11 265 12.
Definition loc_25 : location_info := LocationInfo file_0 264 11 264 17.
Definition loc_26 : location_info := LocationInfo file_0 264 11 264 12.
Definition loc_27 : location_info := LocationInfo file_0 264 11 264 12.
Definition loc_28 : location_info := LocationInfo file_0 264 16 264 17.
Definition loc_29 : location_info := LocationInfo file_0 264 16 264 17.
Definition loc_30 : location_info := LocationInfo file_0 263 11 263 17.
Definition loc_31 : location_info := LocationInfo file_0 263 11 263 12.
Definition loc_32 : location_info := LocationInfo file_0 263 11 263 12.
Definition loc_33 : location_info := LocationInfo file_0 263 16 263 17.
Definition loc_34 : location_info := LocationInfo file_0 263 16 263 17.
Definition loc_35 : location_info := LocationInfo file_0 256 14 258 5.
Definition loc_36 : location_info := LocationInfo file_0 257 8 257 14.
Definition loc_37 : location_info := LocationInfo file_0 257 8 257 9.
Definition loc_38 : location_info := LocationInfo file_0 257 12 257 13.
Definition loc_39 : location_info := LocationInfo file_0 257 12 257 13.
Definition loc_40 : location_info := LocationInfo file_0 258 11 260 5.
Definition loc_41 : location_info := LocationInfo file_0 259 8 259 14.
Definition loc_42 : location_info := LocationInfo file_0 259 8 259 9.
Definition loc_43 : location_info := LocationInfo file_0 259 12 259 13.
Definition loc_44 : location_info := LocationInfo file_0 259 12 259 13.
Definition loc_45 : location_info := LocationInfo file_0 256 7 256 12.
Definition loc_46 : location_info := LocationInfo file_0 256 7 256 8.
Definition loc_47 : location_info := LocationInfo file_0 256 7 256 8.
Definition loc_48 : location_info := LocationInfo file_0 256 11 256 12.
Definition loc_49 : location_info := LocationInfo file_0 256 11 256 12.
Definition loc_52 : location_info := LocationInfo file_0 302 4 307 5.
Definition loc_53 : location_info := LocationInfo file_0 308 4 308 13.
Definition loc_54 : location_info := LocationInfo file_0 308 11 308 12.
Definition loc_55 : location_info := LocationInfo file_0 308 11 308 12.
Definition loc_56 : location_info := LocationInfo file_0 302 4 307 5.
Definition loc_57 : location_info := LocationInfo file_0 302 17 307 5.
Definition loc_58 : location_info := LocationInfo file_0 303 8 303 12.
Definition loc_59 : location_info := LocationInfo file_0 306 8 306 12.
Definition loc_60 : location_info := LocationInfo file_0 302 4 307 5.
Definition loc_61 : location_info := LocationInfo file_0 302 4 307 5.
Definition loc_62 : location_info := LocationInfo file_0 306 8 306 9.
Definition loc_63 : location_info := LocationInfo file_0 303 8 303 9.
Definition loc_64 : location_info := LocationInfo file_0 302 10 302 15.
Definition loc_65 : location_info := LocationInfo file_0 302 10 302 11.
Definition loc_66 : location_info := LocationInfo file_0 302 10 302 11.
Definition loc_67 : location_info := LocationInfo file_0 302 14 302 15.
Definition loc_70 : location_info := LocationInfo file_0 398 4 398 13.
Definition loc_71 : location_info := LocationInfo file_0 398 4 398 8.
Definition loc_72 : location_info := LocationInfo file_0 398 5 398 8.
Definition loc_73 : location_info := LocationInfo file_0 398 5 398 8.
Definition loc_74 : location_info := LocationInfo file_0 398 11 398 12.
Definition loc_77 : location_info := LocationInfo file_0 409 2 409 15.
Definition loc_78 : location_info := LocationInfo file_0 410 2 410 15.
Definition loc_79 : location_info := LocationInfo file_0 410 2 410 10.
Definition loc_80 : location_info := LocationInfo file_0 410 2 410 10.
Definition loc_81 : location_info := LocationInfo file_0 410 11 410 13.
Definition loc_82 : location_info := LocationInfo file_0 410 12 410 13.
Definition loc_83 : location_info := LocationInfo file_0 409 2 409 10.
Definition loc_84 : location_info := LocationInfo file_0 409 2 409 10.
Definition loc_85 : location_info := LocationInfo file_0 409 11 409 13.
Definition loc_86 : location_info := LocationInfo file_0 409 12 409 13.
Definition loc_89 : location_info := LocationInfo file_0 430 4 430 34.
Definition loc_90 : location_info := LocationInfo file_0 431 4 431 13.
Definition loc_91 : location_info := LocationInfo file_0 431 4 431 10.
Definition loc_92 : location_info := LocationInfo file_0 431 4 431 7.
Definition loc_93 : location_info := LocationInfo file_0 431 4 431 7.
Definition loc_94 : location_info := LocationInfo file_0 430 4 430 8.
Definition loc_95 : location_info := LocationInfo file_0 430 5 430 8.
Definition loc_96 : location_info := LocationInfo file_0 430 5 430 8.
Definition loc_97 : location_info := LocationInfo file_0 430 11 430 33.
Definition loc_98 : location_info := LocationInfo file_0 430 11 430 33.
Definition loc_101 : location_info := LocationInfo file_0 430 31 430 32.
(* Definition of struct [basic]. *)
Program Definition struct_basic := {|
......
......@@ -17,12 +17,12 @@
something like
...
theories/examples/tutorial/t1_basic_proof_int_id (...)
coqc tutorial/proofs/t01_basic/.generated_proof_int_id.aux,...
...
This means that this function was verified successfully. If you only see
make[2]: Nothing to be done for 'real-all'.
Entering directory '/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc'
This means that the proof is already up-to-date. The simplest way
to force a rechecking is to add an empty line at the top of this
......@@ -160,21 +160,17 @@ int add1(int a) {
something like:
Cannot solve sidecondition in function "add1" !
Location: "theories/examples/tutorial/t1_basic.c" [ 149 : 11 - 149 : 16 ]
Location: "theories/examples/tutorial/t1_basic.c" [ 149 : 4 - 149 : 17 ]
Location: "tutorial/t01_basic.c" [ 154 : 11 - 154 : 16 ]
Location: "tutorial/t01_basic.c" [ 154 : 4 - 154 : 17 ]
up to date: true
Goal:
Σ : gFunctors
typeG0 : (typeG Σ)
globalG0 : (globalG Σ)
n : Z
arg_a : loc
x : val
_Hyp_ : (min_int i32 ≤ n)
_Hyp1_ : (n ≤ max_int i32)
_Hyp2_ : (min_int i32 ≤ 1)
H : (min_int i32 ≤ n)
H0 : (n ≤ max_int i32)
H1 : (min_int i32 ≤ 1)
---------------------------------------
((n + 1) ∈ i32)
(n + 1 ≤ max_int i32)
This is one of the possible failure modes of RefinedC. If you look
at the first line, you can see that RefinedC could not prove a side
......@@ -237,7 +233,7 @@ int add1(int a) {
Case distinction (DHintDestruct bool (bool_decide (a < b))) -
(false, DestructHintIfBool (bool_decide (a < b)))
at "theories/examples/tutorial/t1_basic.c" [ 260 : 7 - 260 : 12 ]
at "tutorial/t01_basic.c" [ 256 : 7 - 256 : 12 ]
This kind of output gives us some information which case
distinctions took place before this sidecondition was generated,
......@@ -276,7 +272,7 @@ int min(int a, int b) {
As you can see, loops must have an annotated loop invariant.
ATTENTION: If you forget annotating a loop invariant, the
typechecker will happily go around the loop forever and never
typechecker might happily go around the loop forever and never
terminate!
The main part of the loop invariant annotation is the [rc::inv_vars]
......@@ -334,17 +330,17 @@ int looping_add(int a, int b) {
gets stuck. For this example, it should look something like
_ : block{ "#1" }
_ : i2v (a + b - x + 1) i32 ◁ᵥ (a + b - x + 1) @ int i32
_ : arg_b ◁ₗ (a + b - x + 1) @ int i32
_ : arg_a ◁ₗ x @ int i32
_ : i2v (va + vb - acc + 1) i32 ◁ᵥ (va + vb - acc + 1) @ int i32
_ : arg_b ◁ₗ (va + vb - acc + 1) @ int i32
_ : arg_a ◁ₗ acc @ int i32
--------------------------------------∗
The first line only tells us that there is a precondtion for block
"#1", but the other ones are more interesting:
arg_a ◁ₗ x @ int i32
arg_a ◁ₗ acc @ int i32
Tells us that the /location/ where [a] is stored has type [x @ int
Tells us that the /location/ where [a] is stored has type [acc @ int
i32]. In general, RefinedC has two kinds of type assignments:
- The main type assignment of RefinedC is based on locations in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment