Skip to content
Snippets Groups Projects
Commit d13f593d authored by Julien Signoles's avatar Julien Signoles
Browse files

[typing] remove spurious warnings on real

parent a756e6d8
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/doc/Changelog
+ 1
− 0
View file @ d13f593d
...@@ -15,6 +15,7 @@ ...@@ -15,6 +15,7 @@
# E-ACSL: the Whole E-ACSL plug-in # E-ACSL: the Whole E-ACSL plug-in
############################################################################### ###############################################################################
- E-ACSL [2014/03/27] Remove spurious warnings when using type `real`.
-* E-ACSL [2014/03/26] Fix bug #1692 about wrong localisation of -* E-ACSL [2014/03/26] Fix bug #1692 about wrong localisation of
some messages. some messages.
- E-ACSL [2014/03/26] Remove a spurious warning when an annotated - E-ACSL [2014/03/26] Remove a spurious warning when an annotated
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+ 0
− 8
View file @ d13f593d
...@@ -6,16 +6,8 @@ ...@@ -6,16 +6,8 @@
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h" [kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation. [e-acsl] beginning translation.
tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
+ 0
− 4
View file @ d13f593d
...@@ -6,12 +6,8 @@ ...@@ -6,12 +6,8 @@
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h" [kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation. [e-acsl] beginning translation.
tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
......
src/plugins/e-acsl/typing.ml
+ 2
− 8
View file @ d13f593d
...@@ -76,10 +76,7 @@ let typ_of_eacsl_typ = function ...@@ -76,10 +76,7 @@ let typ_of_eacsl_typ = function
| No_integral (Ltype _) -> Error.not_yet "typing of user-defined logic type" | No_integral (Ltype _) -> Error.not_yet "typing of user-defined logic type"
| No_integral (Lvar _) -> Error.not_yet "type variable" | No_integral (Lvar _) -> Error.not_yet "type variable"
| No_integral Linteger -> Mpz.t () | No_integral Linteger -> Mpz.t ()
| No_integral Lreal -> | No_integral Lreal -> TFloat(FLongDouble, [])
Options.warning ~current:true ~once:true
"approximating type `real' by `long double'";
TFloat(FLongDouble, [])
| No_integral (Larrow _) -> Error.not_yet "functional type" | No_integral (Larrow _) -> Error.not_yet "functional type"
let eacsl_typ_of_typ ty = let eacsl_typ_of_typ ty =
...@@ -173,10 +170,7 @@ let generic_typ (which: < f: 'a. 'a * 'a -> 'a >) t = ...@@ -173,10 +170,7 @@ let generic_typ (which: < f: 'a. 'a * 'a -> 'a >) t =
| Ltype _ as ty when Logic_const.is_boolean_type ty -> Mpz.t () | Ltype _ as ty when Logic_const.is_boolean_type ty -> Mpz.t ()
| Ltype _ -> Error.not_yet "typing of user-defined logic type" | Ltype _ -> Error.not_yet "typing of user-defined logic type"
| Lvar _ -> Error.not_yet "type variable" | Lvar _ -> Error.not_yet "type variable"
| Lreal -> | Lreal -> TFloat(FLongDouble, [])
Options.warning ~current:true ~once:true
"approximating type `real' by `long double'";
TFloat(FLongDouble, [])
| Larrow _ -> Error.not_yet "functional type" | Larrow _ -> Error.not_yet "functional type"
in in
which#f (ty, ty) which#f (ty, ty)
......
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