Commit ef0b5271 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

added a ghost uint function

parent bde133d5
......@@ -581,6 +581,14 @@ let rec ghost uint_bound (reg: address_space) (lo w: int): unit
assert { 256*pow2 (8*(w-1)) = pow2 (8*w) };
end
let rec ghost uint (w: int) (reg: address_space) (lo: register): int
ensures { result = uint w reg lo }
variant { w }
= if w <= 0 then 0 else begin
uint_recursion reg lo w;
Map.get reg.data lo + 256*uint (w-1) reg (lo+1)
end
let rec ghost uint_eq (w: int) (m1 m2: address_space) (ofs: int)
requires { w >= 0 }
requires { B.sum (m1,ofs) 0 w = B.sum (m2,ofs) 0 w }
......
......@@ -6,9 +6,9 @@
<prover id="2" name="CVC4" version="1.4" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="13" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="13" steplimit="1" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="13" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="13" steplimit="0" memlimit="2000"/>
<file name="../avrmodel.mlw">
<theory name="AVRint" sum="514a40cb0665f64f0dce0e88744d4d50">
<theory name="AVRint" sum="3d15a03dce7a3b39f896db106f6dc27b">
<goal name="WP_parameter prefix ?" expl="VC for prefix ?">
<proof prover="4"><result status="valid" time="0.02" steps="70"/></proof>
</goal>
......@@ -187,22 +187,22 @@
<goal name="WP_parameter adiw" expl="VC for adiw">
<transf name="split_goal_wp">
<goal name="WP_parameter adiw.1" expl="type invariant">
<proof prover="5" steplimit="-1"><result status="valid" time="0.28"/></proof>
<proof prover="5" steplimit="-1" memlimit="1000"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="WP_parameter adiw.2" expl="postcondition">
<proof prover="5" steplimit="-1"><result status="valid" time="0.30"/></proof>
<proof prover="5" steplimit="-1" memlimit="1000"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="WP_parameter adiw.3" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter adiw.3.1" expl="postcondition">
<proof prover="5" steplimit="1"><result status="valid" time="0.22"/></proof>
<proof prover="5" steplimit="1" memlimit="1000"><result status="valid" time="0.22"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter adiw.4" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter adiw.4.1" expl="postcondition">
<proof prover="5" steplimit="1"><result status="valid" time="0.23"/></proof>
<proof prover="5" steplimit="1" memlimit="1000"><result status="valid" time="0.23"/></proof>
</goal>
</transf>
</goal>
......@@ -217,19 +217,19 @@
<proof prover="4" steplimit="0"><result status="valid" time="0.06" steps="71"/></proof>
</goal>
<goal name="WP_parameter sbiw.3" expl="postcondition">
<proof prover="5" steplimit="1"><result status="valid" time="0.15"/></proof>
<proof prover="5" steplimit="1" memlimit="1000"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter sbiw.4" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter sbiw.4.1" expl="postcondition">
<proof prover="5" steplimit="1"><result status="valid" time="0.26"/></proof>
<proof prover="5" steplimit="1" memlimit="1000"><result status="valid" time="0.26"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sbiw.5" expl="postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter sbiw.5.1" expl="postcondition">
<proof prover="5" steplimit="1"><result status="valid" time="0.26"/></proof>
<proof prover="5" steplimit="1" memlimit="1000"><result status="valid" time="0.26"/></proof>
</goal>
</transf>
</goal>
......@@ -297,13 +297,13 @@
<proof prover="0"><result status="valid" time="1.56"/></proof>
</goal>
<goal name="bitset_correct2" expl="">
<proof prover="5" steplimit="1"><result status="valid" time="0.30"/></proof>
<proof prover="5" steplimit="1" memlimit="1000"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="bitset_equiv_def" expl="">
<proof prover="0"><result status="valid" time="1.42"/></proof>
</goal>
<goal name="bitsetx_equiv_def" expl="">
<proof prover="5" steplimit="1"><result status="valid" time="0.22"/></proof>
<proof prover="5" steplimit="1" memlimit="1000"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter bld" expl="VC for bld">
<proof prover="4"><result status="valid" time="0.87" steps="786"/></proof>
......@@ -324,7 +324,7 @@
<proof prover="4" steplimit="-1"><result status="valid" time="0.14" steps="73"/></proof>
</goal>
<goal name="WP_parameter uint_recursion.4" expl="postcondition">
<proof prover="5" steplimit="1"><result status="valid" time="2.66"/></proof>
<proof prover="5" steplimit="1" memlimit="1000"><result status="valid" time="2.66"/></proof>
</goal>
<goal name="WP_parameter uint_recursion.5" expl="postcondition">
<proof prover="0"><result status="valid" time="0.30"/></proof>
......@@ -337,7 +337,7 @@
<proof prover="4" steplimit="-1"><result status="valid" time="0.10" steps="73"/></proof>
</goal>
<goal name="WP_parameter uint_bound.2" expl="assertion">
<proof prover="5" steplimit="1"><result status="valid" time="2.40"/></proof>
<proof prover="5" steplimit="1" memlimit="1000"><result status="valid" time="2.40"/></proof>
</goal>
<goal name="WP_parameter uint_bound.3" expl="variant decrease">
<proof prover="4" steplimit="-1"><result status="valid" time="0.06" steps="75"/></proof>
......@@ -349,26 +349,42 @@
<proof prover="4" steplimit="0"><result status="valid" time="0.08" steps="82"/></proof>
</goal>
<goal name="WP_parameter uint_bound.6" expl="postcondition">
<proof prover="5"><result status="valid" time="0.34"/></proof>
<proof prover="5" memlimit="1000"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="WP_parameter uint_bound.7" expl="postcondition">
<proof prover="0" steplimit="-1"><result status="valid" time="0.21"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter uint" expl="VC for uint">
<transf name="split_goal_wp">
<goal name="WP_parameter uint.1" expl="postcondition">
<proof prover="5" timelimit="30"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="WP_parameter uint.2" expl="precondition">
<proof prover="5" timelimit="30"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="WP_parameter uint.3" expl="variant decrease">
<proof prover="5" timelimit="30"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="WP_parameter uint.4" expl="postcondition">
<proof prover="5" timelimit="30"><result status="valid" time="2.30"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter uint_eq" expl="VC for uint_eq">
<transf name="split_goal_wp">
<goal name="WP_parameter uint_eq.1" expl="precondition">
<proof prover="5" memlimit="2000"><result status="valid" time="0.22"/></proof>
<proof prover="5"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter uint_eq.2" expl="assertion">
<proof prover="5" memlimit="2000"><result status="valid" time="4.02"/></proof>
<proof prover="5"><result status="valid" time="4.02"/></proof>
</goal>
<goal name="WP_parameter uint_eq.3" expl="precondition">
<proof prover="5" memlimit="2000"><result status="valid" time="0.15"/></proof>
<proof prover="5"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter uint_eq.4" expl="assertion">
<proof prover="5" memlimit="2000"><result status="valid" time="4.38"/></proof>
<proof prover="5"><result status="valid" time="4.38"/></proof>
</goal>
<goal name="WP_parameter uint_eq.5" expl="assertion">
<transf name="split_goal_wp">
......@@ -376,7 +392,7 @@
<proof prover="0" timelimit="30" steplimit="0" memlimit="2000"><result status="valid" time="12.87"/></proof>
</goal>
<goal name="WP_parameter uint_eq.5.2" expl="VC for uint_eq">
<proof prover="5" memlimit="2000"><result status="valid" time="0.16"/></proof>
<proof prover="5"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter uint_eq.5.3" expl="VC for uint_eq">
<proof prover="0" steplimit="0" memlimit="2000"><result status="valid" time="11.25"/></proof>
......@@ -384,22 +400,22 @@
</transf>
</goal>
<goal name="WP_parameter uint_eq.6" expl="variant decrease">
<proof prover="5" memlimit="2000"><result status="valid" time="0.14"/></proof>
<proof prover="5"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter uint_eq.7" expl="precondition">
<proof prover="5" memlimit="2000"><result status="valid" time="0.13"/></proof>
<proof prover="5"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter uint_eq.8" expl="precondition">
<proof prover="5" memlimit="2000"><result status="valid" time="0.12"/></proof>
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter uint_eq.9" expl="assertion">
<proof prover="5" memlimit="2000"><result status="valid" time="0.13"/></proof>
<proof prover="5"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter uint_eq.10" expl="postcondition">
<proof prover="5" memlimit="2000"><result status="valid" time="5.44"/></proof>
<proof prover="5"><result status="valid" time="5.44"/></proof>
</goal>
<goal name="WP_parameter uint_eq.11" expl="postcondition">
<proof prover="5" memlimit="2000"><result status="valid" time="0.23"/></proof>
<proof prover="5"><result status="valid" time="0.23"/></proof>
</goal>
</transf>
</goal>
......
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