diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/sail.ml | 25 | ||||
| -rw-r--r-- | src/type_check.ml | 6 |
2 files changed, 7 insertions, 24 deletions
diff --git a/src/sail.ml b/src/sail.ml index 286141ab..2903e802 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -294,12 +294,8 @@ let version = let default = Printf.sprintf "Sail %s @ %s" branch commit in (* version is parsed from the output of git describe *) match String.split_on_char '-' version with - | [vnum; _; _] -> - (try - let vnum = float_of_string vnum +. 2.0 in - Printf.sprintf "Sail %.1f (%s @ %s)" vnum branch commit - with - | Failure _ -> default) + | (vnum :: _) -> + Printf.sprintf "Sail %s (%s @ %s)" vnum branch commit | _ -> default let usage_msg = @@ -340,22 +336,9 @@ let load_files ?generate:(generate=true) type_envs files = (out_name, ast, type_envs) -let print_version () = - let open Manifest in - let default = Printf.sprintf "Sail %s @ %s" branch commit in - (* version is the output of git describe *) - match String.split_on_char '-' version with - | [vnum; _; _] -> - (try - let vnum = float_of_string vnum +. 2.0 in - Printf.printf "Sail %.1f (%s @ %s)\n" vnum branch commit - with - | Failure _ -> print_endline default) - | _ -> print_endline default - let main() = - if !opt_print_version - then print_version () + if !opt_print_version then + print_endline version else let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in Util.opt_warnings := false; (* Don't show warnings during re-writing for now *) diff --git a/src/type_check.ml b/src/type_check.ml index 82286491..8fca2c7a 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2032,7 +2032,7 @@ let rec rewrite_sizeof' env (Nexp_aux (aux, l) as nexp) = | Nexp_app _ | Nexp_id _ -> typ_error env l ("Cannot re-write sizeof(" ^ string_of_nexp nexp ^ ")") -let rewrite_sizeof env nexp = +let rewrite_sizeof l env nexp = try rewrite_sizeof' env nexp with | No_simple_rewrite -> let locals = Env.get_locals env |> Bindings.bindings in @@ -2044,7 +2044,7 @@ let rewrite_sizeof env nexp = in begin match List.find_opt same_size locals with | Some (id, (_, typ)) -> mk_exp (E_app (mk_id "__size", [mk_exp (E_id id)])) - | None -> raise No_simple_rewrite + | None -> typ_error env l ("Cannot re-write sizeof(" ^ string_of_nexp nexp ^ ")") end let rec rewrite_nc env (NC_aux (nc_aux, l)) = mk_exp ~loc:l (rewrite_nc_aux l env nc_aux) @@ -3414,7 +3414,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = end | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit) | E_sizeof nexp -> - irule infer_exp env (rewrite_sizeof env nexp) + irule infer_exp env (rewrite_sizeof l env nexp) | E_constraint nc -> Env.wf_constraint env nc; crule check_exp env (rewrite_nc env nc) (atom_bool_typ nc) |