diff options
| author | Christopher Pulte | 2016-09-19 16:12:24 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-09-19 16:12:24 +0100 |
| commit | ea2d92c84d879719f44b3f4bf3c9dfabd8d8ea29 (patch) | |
| tree | 87fb42cd892e65b6d5c6279f910849afebf25af6 /src | |
| parent | 4d823e649a4070fbc2ce90bf0980378ffd96a0f9 (diff) | |
| parent | 034f5baee23523f6bbf451bc0e4a5fe05cfd0e2a (diff) | |
Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 452971ae..fa3bcbaa 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1706,7 +1706,7 @@ and check_lexp envs imp_param ret_t is_top (LEXP_aux(lexp,(l,annot))) | _ -> typ_error l ("Cannot assign to " ^ i ^" with type " ^ t_to_string t ^ ". Assignment must be to registers or non-parameter, non-let-bound local variables.")) - | _,_ -> + | _,_ -> if is_top then typ_error l ("Cannot assign to " ^ i ^" with type " ^ t_to_string t ^ @@ -1813,9 +1813,10 @@ and check_lexp envs imp_param ret_t is_top (LEXP_aux(lexp,(l,annot))) ty,false,Envmap.empty,Emp_set,[],bs,ef,ef) | (Tfn _ ,_) -> (match tag with - | External _ | Spec | Emp_global -> - let tannot = (Base(([],ty),Emp_intro,[],pure_e,pure_e,new_bounds)) in - (LEXP_aux(lexp,(l,tannot)),ty, + | External _ | Spec | Emp_global -> + let u' = {t=Tapp("reg",[TA_typ ty])} in + let tannot = (Base(([],u'),Emp_intro,[],pure_e,pure_e,new_bounds)) in + (LEXP_aux(lexp,(l,tannot)),u', false,Envmap.from_list [i,tannot],Emp_intro,[],new_bounds,pure_e,pure_e) | _ -> typ_error l ("Cannot assign to " ^ i ^ " with type " ^ t_to_string t)) |