Skip to content
Snippets Groups Projects
Commit 60aa7368 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Do not exit with an internal error when a badly typed input val is provided to lus2lic -exec. 

Instead, print a warning and consider the input as unbound.
Is it really the right thing to do?
parent 6e55a6bb
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
src/lv6version.ml deleted 100644 → 0
+ 0
− 7
View file @ 6e55a6bb
(** Automatically generated from Makefile *)
let tool = "lus2lic"
let branch = "(no"
let commit = "436"
let sha_1 = "d4498a181c7a7a9aea786e534bad890bd4e1c11d"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "jahier@imag.fr"
src/socExecEvalPredef.ml
+ 38
− 2
View file @ 60aa7368
(* Time-stamp: <modified the 05/06/2013 (at 11:07) by Erwan Jahier> *) (* Time-stamp: <modified the 26/03/2014 (at 09:45) by Erwan Jahier> *)
open SocExecValue open SocExecValue
open Data open Data
...@@ -6,6 +6,21 @@ open Soc ...@@ -6,6 +6,21 @@ open Soc
(* A boring but simple module... *) (* A boring but simple module... *)
let type_error v1 v2 =
Printf.eprintf "Runtime error: '%s' and '%s' have different types.\n"
(Data.val_to_string string_of_float v1) (Data.val_to_string string_of_float v2);
flush stderr
let type_error1 v1 str =
Printf.eprintf "Runtime error: '%s' is not a '%s'\n"
(Data.val_to_string string_of_float v1) str;
flush stderr
let type_error2 v1 v2 str =
Printf.eprintf "Runtime error: '%s' and/or '%s' are/is not a %s\n"
(Data.val_to_string string_of_float v1) (Data.val_to_string string_of_float v2) str;
flush stderr
let (lustre_plus : ctx -> ctx) = let (lustre_plus : ctx -> ctx) =
fun ctx -> fun ctx ->
let l = [get_val "x" ctx; get_val "y" ctx] in let l = [get_val "x" ctx; get_val "y" ctx] in
...@@ -14,7 +29,8 @@ let (lustre_plus : ctx -> ctx) = ...@@ -14,7 +29,8 @@ let (lustre_plus : ctx -> ctx) =
| [I x1; I x2] -> "z"::ctx.cpath,I(x1+x2) | [I x1; I x2] -> "z"::ctx.cpath,I(x1+x2)
| [F i1; F i2] -> "z"::ctx.cpath,F(i1+.i2) | [F i1; F i2] -> "z"::ctx.cpath,F(i1+.i2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| e -> assert false | [v1;v2] -> type_error v1 v2; "z"::ctx.cpath,U
| _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -24,6 +40,7 @@ let lustre_times ctx = ...@@ -24,6 +40,7 @@ let lustre_times ctx =
| [I x1; I x2] -> "z"::ctx.cpath,I(x1 * x2) | [I x1; I x2] -> "z"::ctx.cpath,I(x1 * x2)
| [F x1; F x2] -> "z"::ctx.cpath,F(x1 *. x2) | [F x1; F x2] -> "z"::ctx.cpath,F(x1 *. x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2; "z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -35,6 +52,7 @@ let lustre_div ctx = ...@@ -35,6 +52,7 @@ let lustre_div ctx =
| [I x1; I x2] -> "z"::ctx.cpath,I(x1 / x2) | [I x1; I x2] -> "z"::ctx.cpath,I(x1 / x2)
| [F x1; F x2] -> "z"::ctx.cpath,F(x1 /. x2) | [F x1; F x2] -> "z"::ctx.cpath,F(x1 /. x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2;"z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -45,6 +63,7 @@ let lustre_slash ctx = ...@@ -45,6 +63,7 @@ let lustre_slash ctx =
| [I x1; I x2] -> "z"::ctx.cpath,I(x1 / x2) | [I x1; I x2] -> "z"::ctx.cpath,I(x1 / x2)
| [F x1; F x2] -> "z"::ctx.cpath,F(x1 /. x2) | [F x1; F x2] -> "z"::ctx.cpath,F(x1 /. x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2;"z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -56,6 +75,8 @@ let lustre_minus ctx = ...@@ -56,6 +75,8 @@ let lustre_minus ctx =
| [I x1; I x2] -> "z"::ctx.cpath,I(x1 - x2) | [I x1; I x2] -> "z"::ctx.cpath,I(x1 - x2)
| [F x1; F x2] -> "z"::ctx.cpath,F(x1 -. x2) | [F x1; F x2] -> "z"::ctx.cpath,F(x1 -. x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2; "z"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2; "z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -65,6 +86,7 @@ let lustre_mod ctx = ...@@ -65,6 +86,7 @@ let lustre_mod ctx =
match ([get_val "x" ctx; get_val "y" ctx]) with match ([get_val "x" ctx; get_val "y" ctx]) with
| [I x1; I x2] -> "z"::ctx.cpath,I(x1 mod x2) | [I x1; I x2] -> "z"::ctx.cpath,I(x1 mod x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2; "z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -75,6 +97,7 @@ let lustre_eq ctx = ...@@ -75,6 +97,7 @@ let lustre_eq ctx =
match ([get_val "x" ctx; get_val "y" ctx]) with match ([get_val "x" ctx; get_val "y" ctx]) with
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [x1; x2] -> "z"::ctx.cpath,B(x1 = x2) | [x1; x2] -> "z"::ctx.cpath,B(x1 = x2)
| [v1;v2] -> type_error v1 v2; "z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -85,6 +108,7 @@ let lustre_uminus ctx = ...@@ -85,6 +108,7 @@ let lustre_uminus ctx =
| [I x1] -> "z"::ctx.cpath,I(- x1) | [I x1] -> "z"::ctx.cpath,I(- x1)
| [F x1] -> "z"::ctx.cpath,F(-. x1) | [F x1] -> "z"::ctx.cpath,F(-. x1)
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [v1] -> type_error1 v1 "numeric";"z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -94,6 +118,7 @@ let lustre_real2int ctx = ...@@ -94,6 +118,7 @@ let lustre_real2int ctx =
match ([get_val "x" ctx]) with match ([get_val "x" ctx]) with
| [F x1] -> "z"::ctx.cpath,I(int_of_float x1) | [F x1] -> "z"::ctx.cpath,I(int_of_float x1)
| [U] -> "z"::ctx.cpath,U | [U] -> "z"::ctx.cpath,U
| [v1] -> type_error1 v1 "real";"z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -104,6 +129,7 @@ let lustre_int2real ctx = ...@@ -104,6 +129,7 @@ let lustre_int2real ctx =
match ([get_val "x" ctx]) with match ([get_val "x" ctx]) with
| [I x1] -> "z"::ctx.cpath,F(float_of_int x1) | [I x1] -> "z"::ctx.cpath,F(float_of_int x1)
| [U] -> "z"::ctx.cpath,U | [U] -> "z"::ctx.cpath,U
| [v1] -> type_error1 v1 "int";"z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -114,6 +140,7 @@ let lustre_not ctx = ...@@ -114,6 +140,7 @@ let lustre_not ctx =
match ([get_val "x" ctx]) with match ([get_val "x" ctx]) with
| [B x1] -> "z"::ctx.cpath,B(not x1) | [B x1] -> "z"::ctx.cpath,B(not x1)
| [U] -> "z"::ctx.cpath,U | [U] -> "z"::ctx.cpath,U
| [v1] -> type_error1 v1 "bool";"z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -124,6 +151,7 @@ let lustre_lt ctx = ...@@ -124,6 +151,7 @@ let lustre_lt ctx =
match ([get_val "x" ctx; get_val "y" ctx]) with match ([get_val "x" ctx; get_val "y" ctx]) with
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [x1; x2] -> "z"::ctx.cpath,B(x1 < x2) | [x1; x2] -> "z"::ctx.cpath,B(x1 < x2)
| [v1;v2] -> type_error v1 v2; "z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -133,6 +161,7 @@ let lustre_gt ctx = ...@@ -133,6 +161,7 @@ let lustre_gt ctx =
match ([get_val "x" ctx; get_val "y" ctx]) with match ([get_val "x" ctx; get_val "y" ctx]) with
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [x1; x2] -> "z"::ctx.cpath,B(x1 > x2) | [x1; x2] -> "z"::ctx.cpath,B(x1 > x2)
| [v1;v2] -> type_error v1 v2; "z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -142,6 +171,7 @@ let lustre_lte ctx = ...@@ -142,6 +171,7 @@ let lustre_lte ctx =
match ([get_val "x" ctx; get_val "y" ctx]) with match ([get_val "x" ctx; get_val "y" ctx]) with
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [x1; x2] -> "z"::ctx.cpath,B(x1 <= x2) | [x1; x2] -> "z"::ctx.cpath,B(x1 <= x2)
| [v1;v2] -> type_error v1 v2; "z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -151,6 +181,7 @@ let lustre_gte ctx = ...@@ -151,6 +181,7 @@ let lustre_gte ctx =
match ([get_val "x" ctx; get_val "y" ctx]) with match ([get_val "x" ctx; get_val "y" ctx]) with
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [x1; x2] -> "z"::ctx.cpath,B(x1 >= x2) | [x1; x2] -> "z"::ctx.cpath,B(x1 >= x2)
| [v1;v2] -> type_error v1 v2; "z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -160,6 +191,7 @@ let lustre_and ctx = ...@@ -160,6 +191,7 @@ let lustre_and ctx =
match ([get_val "x" ctx; get_val "y" ctx]) with match ([get_val "x" ctx; get_val "y" ctx]) with
| [B x1; B x2] -> "z"::ctx.cpath,B(x1 && x2) | [B x1; B x2] -> "z"::ctx.cpath,B(x1 && x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [v1;v2] -> type_error2 v1 v2 "bool";"z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -169,6 +201,7 @@ let lustre_xor ctx = ...@@ -169,6 +201,7 @@ let lustre_xor ctx =
match ([get_val "x" ctx; get_val "y" ctx]) with match ([get_val "x" ctx; get_val "y" ctx]) with
| [B x1; B x2] -> "z"::ctx.cpath,B(x1 <> x2) | [B x1; B x2] -> "z"::ctx.cpath,B(x1 <> x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [v1;v2] -> type_error2 v1 v2 "bool";"z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -189,6 +222,7 @@ let lustre_or ctx = ...@@ -189,6 +222,7 @@ let lustre_or ctx =
match ([get_val "x" ctx; get_val "y" ctx]) with match ([get_val "x" ctx; get_val "y" ctx]) with
| [B x1; B x2] -> "z"::ctx.cpath,B(x1 || x2) | [B x1; B x2] -> "z"::ctx.cpath,B(x1 || x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [v1;v2] -> type_error2 v1 v2 "bool";"z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -199,6 +233,7 @@ let lustre_impl ctx = ...@@ -199,6 +233,7 @@ let lustre_impl ctx =
match ([get_val "x" ctx; get_val "y" ctx]) with match ([get_val "x" ctx; get_val "y" ctx]) with
| [B x1; B x2] -> "z"::ctx.cpath,B(not x1 or x2) | [B x1; B x2] -> "z"::ctx.cpath,B(not x1 or x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U | [U; _] | [_;U] -> "z"::ctx.cpath,U
| [v1;v2] -> type_error2 v1 v2 "bool";"z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
...@@ -208,6 +243,7 @@ let lustre_if ctx = ...@@ -208,6 +243,7 @@ let lustre_if ctx =
match ([get_val "c" ctx; get_val "xt" ctx; get_val "xe" ctx]) with match ([get_val "c" ctx; get_val "xt" ctx; get_val "xe" ctx]) with
| [B c; v1; v2] -> "z"::ctx.cpath, if c then v1 else v2 | [B c; v1; v2] -> "z"::ctx.cpath, if c then v1 else v2
| [U;_; _] | [_;U;U] -> "z"::ctx.cpath,U | [U;_; _] | [_;U;U] -> "z"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2; "z"::ctx.cpath,U
| _ -> assert false | _ -> assert false
in in
{ ctx with s = sadd ctx.s vn vv } { ctx with s = sadd ctx.s vn vv }
......
test/lus2lic.log.ref
+ 303
− 301
View file @ 60aa7368
This diff is collapsed.
test/lus2lic.sum
+ 3
− 3
View file @ 60aa7368
Test Run By jahier on Tue Mar 25 14:28:07 2014 Test Run By jahier on Wed Mar 26 09:48:14 2014
Native configuration is i686-pc-linux-gnu Native configuration is i686-pc-linux-gnu
=== lus2lic tests === === lus2lic tests ===
...@@ -1028,7 +1028,7 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman ...@@ -1028,7 +1028,7 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
# of unexpected failures 74 # of unexpected failures 74
# of unexpected successes 21 # of unexpected successes 21
# of expected failures 37 # of expected failures 37
testcase ./lus2lic.tests/non-reg.exp completed in 103 seconds testcase ./lus2lic.tests/non-reg.exp completed in 106 seconds
testcase ./lus2lic.tests/progression.exp completed in 0 seconds testcase ./lus2lic.tests/progression.exp completed in 0 seconds
testcase ./lus2lic.tests/non-reg.exp completed in 103 seconds testcase ./lus2lic.tests/non-reg.exp completed in 106 seconds
testcase ./lus2lic.tests/progression.exp completed in 0 seconds testcase ./lus2lic.tests/progression.exp completed in 0 seconds
test/lus2lic.time
+ 1
− 1
View file @ 60aa7368
testcase ./lus2lic.tests/non-reg.exp completed in 103 seconds testcase ./lus2lic.tests/non-reg.exp completed in 106 seconds
testcase ./lus2lic.tests/progression.exp completed in 0 seconds testcase ./lus2lic.tests/progression.exp completed in 0 seconds
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