Skip to content
GitLab
Commit d7201cfe authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Make axiom only apply to 8 bit uints to avoid inconsistencies

parent 927e6350
Hide whitespace changes
Inline Side-by-side
avrmodel.mlw
View file @ d7201cfe
......@@ -429,8 +429,9 @@ use bv.BV8
val bv8_to_int (x: BV8.t): int
ensures { result = BV8.t'int x }
axiom bv8_nth_def: forall x y. BV8.nth (BV8.of_int x) y <-> mod (div x (pow2 y)) 2 = 1
axiom bv8_nth_def: forall x y. (256 > x >= 0 /\ 8 > y >= 0) -> (BV8.nth (BV8.of_int x) y <-> mod (div x (pow2 y)) 2 = 1)
(*
let add_ (dst src: register): unit
writes { reg, cf }
ensures { reg = old (reg[dst <- mod (reg[dst] + reg[src]) 256]) }
......@@ -450,6 +451,7 @@ let sub_ (dst src: register): unit
let rd' = BV8.sub rd rr in
reg.data <- data_set reg.data dst (bv8_to_int rd');
cf.value <- (not BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rr 7 && BV8.nth rd' 7 || BV8.nth rd' 7 && not BV8.nth rd 7)
*)
let inc_ (dst: register): unit
writes { reg }
......
avrmodel/why3session.xml
View file @ d7201cfe
......@@ -96,10 +96,10 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC ld_inc.1" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC ld_inc.2" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC ld_inc.3" expl="type invariant" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.14" steps="134"/></proof>
......@@ -295,88 +295,6 @@
</goal>
</transf>
</goal>
<goal name="VC add_" expl="VC for add_" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="VC add_.0" expl="VC for add_" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC add_.0.0" expl="type invariant" proved="true">
<proof prover="4" timelimit="60" memlimit="12000"><result status="valid" time="0.09" steps="163"/></proof>
</goal>
<goal name="VC add_.0.1" expl="postcondition" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.36" steps="200"/></proof>
</goal>
<goal name="VC add_.0.2" expl="postcondition" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.29" steps="126"/></proof>
</goal>
<goal name="VC add_.0.3" expl="type invariant" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.11" steps="170"/></proof>
</goal>
<goal name="VC add_.0.4" expl="postcondition" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.29" steps="215"/></proof>
</goal>
<goal name="VC add_.0.5" expl="postcondition" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC add_.0.5.0" expl="postcondition" proved="true">
<proof prover="3" timelimit="30" memlimit="4000"><result status="valid" time="10.41"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add_.0.6" expl="type invariant" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.10" steps="175"/></proof>
</goal>
<goal name="VC add_.0.7" expl="postcondition" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.36" steps="215"/></proof>
</goal>
<goal name="VC add_.0.8" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.71"/></proof>
</goal>
<goal name="VC add_.0.9" expl="type invariant" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC add_.0.10" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC add_.0.11" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC add_.0.12" expl="type invariant" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.10" steps="171"/></proof>
</goal>
<goal name="VC add_.0.13" expl="postcondition" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.19" steps="201"/></proof>
</goal>
<goal name="VC add_.0.14" expl="postcondition" proved="true">
<proof prover="4" timelimit="5" memlimit="2000"><result status="valid" time="4.30" steps="1805"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC sub_" expl="VC for sub_" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="VC sub_.0" expl="VC for sub_" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC sub_.0.0" expl="type invariant" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.11" steps="172"/></proof>
</goal>
<goal name="VC sub_.0.1" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC sub_.0.1.0" expl="postcondition" proved="true">
<proof prover="4" timelimit="30" memlimit="4000"><result status="valid" time="19.73" steps="724"/></proof>
</goal>
</transf>
</goal>
<goal name="VC sub_.0.2" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC sub_.0.2.0" expl="postcondition" proved="true">
<proof prover="4" timelimit="5" memlimit="2000"><result status="valid" time="3.30" steps="570"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC inc_" expl="VC for inc_" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC inc_.0" expl="type invariant" proved="true">
......@@ -413,13 +331,13 @@
<proof prover="4" timelimit="60" memlimit="12000"><result status="valid" time="0.07" steps="123"/></proof>
</goal>
<goal name="VC asr.1" expl="postcondition" proved="true">
<proof prover="4" timelimit="60" memlimit="12000"><result status="valid" time="0.12" steps="219"/></proof>
<proof prover="4" timelimit="60" memlimit="12000"><result status="valid" time="0.12" steps="220"/></proof>
</goal>
<goal name="VC asr.2" expl="postcondition" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.22" steps="175"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.22" steps="153"/></proof>
</goal>
<goal name="VC asr.3" expl="postcondition" proved="true">
<proof prover="4" timelimit="60" memlimit="12000"><result status="valid" time="0.06" steps="121"/></proof>
<proof prover="4" timelimit="60" memlimit="12000"><result status="valid" time="0.06" steps="118"/></proof>
</goal>
</transf>
</goal>
......@@ -432,7 +350,7 @@
<proof prover="3"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC lsr.2" expl="postcondition" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.21" steps="175"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.21" steps="153"/></proof>
</goal>
<goal name="VC lsr.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
......@@ -469,7 +387,7 @@
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="bitset_correct1" proved="true">
<proof prover="0"><result status="valid" time="1.20"/></proof>
<proof prover="0"><result status="valid" time="1.83"/></proof>
</goal>
<goal name="bitset_correct2" proved="true">
<proof prover="5"><result status="valid" time="0.10"/></proof>
......@@ -502,7 +420,7 @@
<goal name="VC uint_recursion.0.0" expl="assertion" proved="true">
<transf name="inline_all" proved="true" >
<goal name="VC uint_recursion.0.0.0" expl="assertion" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.24" steps="196"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.24" steps="198"/></proof>
</goal>
</transf>
</goal>
......
avrmodel/why3shapes.gz
View file @ d7201cfe
No preview for this file type
Supports Markdown
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