Commit 33f16ba1 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Ensure radix-2 and radix-8 constants are properly sent to Gappa.

parent cde5c55a
......@@ -95,3 +95,12 @@ theory GappaEq2
value ("lab2" q) - value q1 * value q2 <= 0x1.p-52
end
theory GappaNumbers
use import int.Int
goal G1 : 0x1f - 0o37 = 0
goal G2 : 0b1001 - 9 = 0
end
......@@ -14,7 +14,7 @@
locfile="../gappa.why"
loclnum="2" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
expanded="false">
<goal
name="Round_single_01"
locfile="../gappa.why"
......@@ -123,7 +123,7 @@
locfile="../gappa.why"
loclnum="41" loccnumb="7" loccnume="14"
verified="true"
expanded="true">
expanded="false">
<goal
name="Test1"
locfile="../gappa.why"
......@@ -181,14 +181,14 @@
locfile="../gappa.why"
loclnum="72" loccnumb="7" loccnume="15"
verified="true"
expanded="true">
expanded="false">
<goal
name="G1"
locfile="../gappa.why"
loclnum="89" loccnumb="7" loccnume="9"
sum="74b37efbbe6660f5ea36fd62cc900a56"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;=ainfix -avaluearesultainfix *avalueaq1avalueaq2c0x1.p-52">
<proof
prover="0"
......@@ -205,7 +205,7 @@
loclnum="91" loccnumb="7" loccnume="9"
sum="d3842095b63f0f1ab64946632f288173"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;=ainfix -avalueV0ainfix *avalueaq1avalueaq2c0x1.p-52Iainfix =V0aresultF">
<proof
prover="0"
......@@ -222,7 +222,7 @@
loclnum="94" loccnumb="7" loccnume="9"
sum="6ca1af78b2d507b13a5914296f9bef9e"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &lt;=ainfix -avalueV0ainfix *avalueaq1avalueaq2c0x1.p-52Iainfix =V0aresultF">
<proof
prover="0"
......@@ -234,5 +234,46 @@
</proof>
</goal>
</theory>
<theory
name="GappaNumbers"
locfile="../gappa.why"
loclnum="99" loccnumb="7" loccnume="19"
verified="true"
expanded="false">
<goal
name="G1"
locfile="../gappa.why"
loclnum="103" loccnumb="7" loccnume="9"
sum="a11eaea1a9b7aecdd63d32e24ca320a7"
proved="true"
expanded="false"
shape="ainfix =ainfix -c0x1fc0o37c0">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G2"
locfile="../gappa.why"
loclnum="104" loccnumb="7" loccnume="9"
sum="a9d369101091c10180e385534508fd97"
proved="true"
expanded="false"
shape="ainfix =ainfix -c0b1001c9c0">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
</file>
</why3session>
......@@ -143,20 +143,21 @@ let ident_printer =
let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
let constant_value =
let number_format = {
Number.long_int_support = true;
Number.dec_int_support = Number.Number_default;
Number.hex_int_support = Number.Number_default;
Number.oct_int_support = Number.Number_unsupported;
Number.bin_int_support = Number.Number_unsupported;
Number.def_int_support = Number.Number_unsupported;
Number.dec_real_support = Number.Number_default;
Number.hex_real_support = Number.Number_default;
Number.frac_real_support = Number.Number_unsupported;
Number.def_real_support = Number.Number_unsupported;
} in
fun t -> match t.t_node with
let number_format = {
Number.long_int_support = true;
Number.dec_int_support = Number.Number_default;
Number.hex_int_support = Number.Number_default;
Number.oct_int_support = Number.Number_unsupported;
Number.bin_int_support = Number.Number_unsupported;
Number.def_int_support = Number.Number_unsupported;
Number.dec_real_support = Number.Number_default;
Number.hex_real_support = Number.Number_default;
Number.frac_real_support = Number.Number_unsupported;
Number.def_real_support = Number.Number_unsupported;
}
let constant_value t =
match t.t_node with
| Tconst c ->
fprintf str_formatter "%a" (Number.print number_format) c;
flush_str_formatter ()
......@@ -172,7 +173,7 @@ let rec print_term info fmt t =
let term = print_term info in
match t.t_node with
| Tconst c ->
Pretty.print_const fmt c
fprintf fmt "%a" (Number.print number_format) c
| Tvar { vs_name = id } ->
print_ident fmt id
| Tapp ( { ls_name = id } ,[] ) ->
......
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