Commit 6a2a53ea authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Improve extraction of arrays and mutable structs

parent 0aa5c166
......@@ -10,11 +10,20 @@ else
endif
endif
clean:
rm -rf build
dir:
mkdir -p build
why3:
make -C ../..
extract: why3
$(WHY3) extract -D cursor.drv -D c -L . -o ptrcursor.c ccursor.PtrCursor
extract: why3 dir
$(WHY3) extract -D cursor.drv -D c -L . -o build/ptrcursor.c ccursor.PtrCursor
cfiles: extract
gcc -Wall -g -pedantic -Wno-unused-function -std=c11 build/ptrcursor.c -Ibuild -o build/tests
main: extract
gcc -Wall -g -pedantic -Wno-unused-function -c -std=c11 ptrcursor.c
tests: cfiles
./build/tests
......@@ -46,6 +46,7 @@ module PtrCursor
ensures { result.len = l }
ensures { not result.freed }
ensures { forall i. 0 <= i < l -> (data result.current)[i] = 0 }
ensures { bound result = b }
= let a = malloc (UInt32.of_int32 l) in
c_assert (is_not_null a);
for i = 0 to l-1 do
......@@ -108,7 +109,17 @@ module PtrCursor
a[i] <- 0
done;
c.new <- true;
(* assert { forall i. 0 <= i < n -> Map.get (pelts c.current) i = a[i] };*)
end
let main () : int32
= let c = create_cursor 4 4 in
for i = 0:int32 to 255 do
invariant { not c.freed }
invariant { forall i. 0 <= i < c.len -> (data c.current)[i] < c.bound }
c_assert c.new;
next c;
done;
c_assert (not c.new);
0
end
\ No newline at end of file
......@@ -68,7 +68,10 @@
<goal name="VC create_cursor.10" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC create_cursor.11" expl="out of loop bounds" proved="true">
<goal name="VC create_cursor.11" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC create_cursor.12" expl="out of loop bounds" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
......@@ -271,7 +274,6 @@
<transf name="case" proved="true" arg1="(i &gt;= r)">
<goal name="VC next.26.6.0" expl="true case (type invariant)" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="290"/></proof>
<proof prover="3"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC next.26.6.1" expl="false case (type invariant)" proved="true">
<proof prover="2"><result status="valid" time="0.15" steps="422"/></proof>
......@@ -285,6 +287,40 @@
</goal>
</transf>
</goal>
<goal name="VC main" expl="VC for main" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.1" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC main.2" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.3" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC main.4" expl="type invariant" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC main.5" expl="type invariant" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC main.6" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.7" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC main.8" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC main.9" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -2,6 +2,6 @@ module ccursor.PtrCursor
syntax val ([]) "%1[%2]"
syntax val ([]<-) "%1[%2] = %3"
syntax val get_current "%1.current"
syntax val get_current "%1->current"
end
\ No newline at end of file
This diff is collapsed.
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