Commit 85e816e8 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Fix proofs following removal of Bounded_int.{eq, ne}

parent 6ef5dada
......@@ -36,9 +36,7 @@ module mach.int.Int32
syntax val (*) "%1 * %2"
syntax val (/) "%1 / %2"
syntax val (%) "%1 % %2"
syntax val eq "%1 == %2"
syntax val (=) "%1 == %2"
syntax val ne "%1 != %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
......@@ -106,9 +104,7 @@ void lsld32(uint32_t * low, uint32_t * high, uint32_t x, uint32_t cnt)
syntax val (*) "%1 * %2"
syntax val (/) "%1 / %2"
syntax val (%) "%1 % %2"
syntax val eq "%1 == %2"
syntax val (=) "%1 == %2"
syntax val ne "%1 != %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
......@@ -232,9 +228,7 @@ uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
syntax val (*) "%1 * %2"
syntax val (/) "%1 / %2"
syntax val (%) "%1 % %2"
syntax val eq "%1 == %2"
syntax val (=) "%1 == %2"
syntax val ne "%1 != %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
......
......@@ -6,11 +6,11 @@ module Test
let a () : unit diverges =
let zero = Int32.of_int 0 in
let r = ref 0 in
let r = ref zero in
let rr = ref r in
let x = ref (ref 0) in
let x = ref (ref zero) in
x := !x;
!x := 42;
!x := Int32.of_int 42;
let p = malloc (UInt32.of_int 2) in
c_assert (is_not_null p);
let b = ref p in
......
......@@ -6,68 +6,63 @@
<prover id="1" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="2000"/>
<file name="../alias.mlw" expanded="true">
<theory name="Test" sum="60d2c661058fee260304cc03a8554cad" expanded="true">
<goal name="VC a" expl="VC for a">
<proof prover="0"><result status="valid" time="0.03" steps="88"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<file name="../alias.mlw" proved="true">
<theory name="Test" proved="true" sum="773ba2f1c5327babb485c13dcb1be597">
<goal name="VC a" expl="VC for a" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="93"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC t_alias" expl="VC for t_alias" expanded="true">
<goal name="VC t_alias" expl="VC for t_alias" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="72"/></proof>
</goal>
<goal name="VC test" expl="VC for test">
<transf name="split_goal_wp">
<goal name="VC test.1" expl="1. assertion">
<goal name="VC test" expl="VC for test" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC test.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="73"/></proof>
<proof prover="1" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC test.2" expl="2. assertion">
<goal name="VC test.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="74"/></proof>
<proof prover="1" obsolete="true"><result status="valid" time="0.00"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Refptr" sum="28e6ccc93811975085d494b96cfc79ef" expanded="true">
<goal name="VC refp" expl="VC for refp" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="1"/></proof>
<transf name="split_goal_wp" expanded="true">
<goal name="VC refp.1" expl="1. integer overflow">
<theory name="Refptr" proved="true" sum="e0c18f7f9852ffa63bd288fd26538a90">
<goal name="VC refp" expl="VC for refp" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
<transf name="split_goal_wp" proved="true" >
<goal name="VC refp.0" expl="integer overflow" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="78"/></proof>
</goal>
<goal name="VC refp.2" expl="2. precondition">
<goal name="VC refp.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="75"/></proof>
</goal>
<goal name="VC refp.3" expl="3. postcondition">
<goal name="VC refp.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="76"/></proof>
</goal>
<goal name="VC refp.4" expl="4. postcondition">
<goal name="VC refp.3" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="76"/></proof>
</goal>
</transf>
</goal>
<goal name="VC infix ::=" expl="VC for infix ::=" expanded="true">
<goal name="VC infix ::=">
<proof prover="0" timelimit="55" obsolete="true"><result status="outofmemory" time="29.53"/></proof>
<transf name="split_goal_wp" expanded="true">
<goal name="VC infix ::=.1" expl="1. integer overflow">
<proof prover="0"><result status="valid" time="0.02" steps="78"/></proof>
<transf name="split_goal_wp" >
<goal name="VC infix ::=.1">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="78"/></proof>
</goal>
<goal name="VC infix ::=.2" expl="2. precondition" expanded="true">
<proof prover="0" obsolete="true"><undone/></proof>
<proof prover="3"><undone/></proof>
<goal name="VC infix ::=.2">
<proof prover="0" obsolete="true"><result status="failure" time="0.00"/></proof>
<proof prover="3" obsolete="true"><result status="failure" time="0.00"/></proof>
</goal>
<goal name="VC infix ::=.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
<goal name="VC infix ::=.3">
<proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="82"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="A" sum="01e2c7b0173f54ae866bc2d6700edd1a" expanded="true">
<goal name="VC test" expl="VC for test" expanded="true">
<proof prover="0" obsolete="true"><result status="valid" time="0.29" steps="475"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -298,7 +298,7 @@ module N
assert { 0 <= !i < sz };
let lx = get_ofs x !i in
let ly = get_ofs y !i in
if (Limb.ne lx ly)
if (not (Limb.(=) lx ly))
then begin
value_sub_concat (pelts x) x.offset (x.offset+k) (x.offset+p2i sz);
value_sub_concat (pelts y) y.offset (y.offset+k) (y.offset+p2i sz);
......@@ -361,7 +361,7 @@ module N
i := Int32.(-) !i (Int32.of_int 1);
assert { 0 <= !i < sz };
lx := get_ofs x !i;
if (Limb.ne !lx uzero)
if not (Limb.(=) !lx uzero)
then begin
value_sub_concat (pelts x) x.offset (x.offset+k) (x.offset + p2i sz);
value_sub_lower_bound_tight (pelts x) x.offset (x.offset+k);
......@@ -411,7 +411,7 @@ module N
let c = ref y in
let lx = ref limb_zero in
let i = ref (Int32.of_int 0) in
while Int32.(<) !i sz && Limb.ne !c limb_zero do
while Int32.(<) !i sz && (not (Limb.(=) !c limb_zero)) do
invariant { 0 <= !i <= sz }
invariant { !i > 0 -> 0 <= !c <= 1 }
invariant { value r !i + (power radix !i) * !c =
......@@ -444,7 +444,7 @@ module N
= value x k + y + (power radix k) * !lx
= value x !i + y }
done;
if Int32.eq !i sz then !c
if Int32.(=) !i sz then !c
else begin
while Int32.(<) !i sz do
invariant { !c = 0 }
......@@ -811,7 +811,7 @@ module N
let b = ref y in
let lx = ref limb_zero in
let i = ref (Int32.of_int 0) in
while Int32.(<) !i sz && Limb.ne !b limb_zero do
while Int32.(<) !i sz && (not (Limb.(=) !b limb_zero)) do
invariant { 0 <= !i <= sz }
invariant { !i > 0 -> 0 <= !b <= 1 }
invariant { value r !i - power radix !i * !b
......@@ -845,7 +845,7 @@ module N
= value x !i - y
};
done;
if Int32.eq !i sz then !b
if Int32.(=) !i sz then !b
else begin
while Int32.(<) !i sz do
invariant { !b = 0 }
......@@ -3621,7 +3621,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
>= (pelts x)[(!xp).offset] + radix * !x1 }
let ghost ox = pelts x in
begin "vc:sp"
if Limb.ne qh limb_zero
if (not (Limb.(=) qh limb_zero))
then begin
assert { qh = 1 };
let b = sub_in_place xd y sy sy in
......@@ -4574,7 +4574,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
- power radix sy * cy2
};
end;
if "ex:unlikely" Limb.ne cy2 limb_zero
if "ex:unlikely" (not (Limb.(=) cy2 limb_zero))
then begin
label Adjust in
assert { cy2 = 1 };
......
......@@ -360,6 +360,7 @@ type info = Pdriver.printer_args = private {
blacklist : Printer.blacklist;
syntax : Printer.syntax_map;
converter : Printer.syntax_map;
literal : Printer.syntax_map; (*TODO handle literals*)
}
let debug = false
......
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