From 1aac6f7be4db813c4607086ddca7d93166bf9bdd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Fri, 7 Oct 2011 11:55:29 +0200 Subject: [PATCH] Fixed bug in unicity check in linear typing Test case included --- compiler/heptagon/analysis/linear_typing.ml | 5 +++-- test/bad/linear_fun.ept | 20 ++++++++++++++++++++ 2 files changed, 23 insertions(+), 2 deletions(-) create mode 100644 test/bad/linear_fun.ept diff --git a/compiler/heptagon/analysis/linear_typing.ml b/compiler/heptagon/analysis/linear_typing.ml index 1cd6fab..125c427 100644 --- a/compiler/heptagon/analysis/linear_typing.ml +++ b/compiler/heptagon/analysis/linear_typing.ml @@ -774,8 +774,9 @@ and expect env lin e = let l, env = match e.e_desc with | Evar x -> let actual_lin = lin_of_ident x env in - let env = check_linearity_exp env e lin in - unify_lin lin actual_lin, env + let found_lin = unify_lin lin actual_lin in + let env = check_linearity_exp env e found_lin in + found_lin, env | Emerge (_, c_e_list) -> let env = List.fold_left (fun env (_, e) -> safe_expect env lin e) env c_e_list in diff --git a/test/bad/linear_fun.ept b/test/bad/linear_fun.ept new file mode 100644 index 0000000..c926a68 --- /dev/null +++ b/test/bad/linear_fun.ept @@ -0,0 +1,20 @@ +const n:int = 100 + +type tab = float^n + +node f(x : tab at r) returns (o : tab at r) +let + o = x; +tel + +node main() returns (o:float) +var u : tab at r; + z1 : tab; z2 : tab at r; +let + init<> u = (0.0)^n; + + z1 = f(u); + z2 = f(u); + + o = 0.0; +tel \ No newline at end of file