Skip to content

Improve the code coverage #182

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 10 additions & 4 deletions src/coqOfOCaml.ml
Original file line number Diff line number Diff line change
Expand Up @@ -101,13 +101,13 @@ let of_ocaml
success_message;
}

let exit (context : MonadEval.Context.t) (output : Output.t) : unit =
let get_exit_code (context : MonadEval.Context.t) (output : Output.t) : int =
let is_blacklist =
Configuration.is_filename_in_error_blacklist context.configuration in
if output.has_errors && not is_blacklist then
exit 1
1
else
exit 0
0

(** The main function. *)
let main () =
Expand Down Expand Up @@ -163,6 +163,7 @@ let main () =
let pipeline = Mpipeline.make merlin_config file_source in

Mpipeline.with_pipeline pipeline (fun _ ->
try
let comments = Mpipeline.reader_comments pipeline in
let typing = Mpipeline.typer_result pipeline in
let typedtree = Mtyper.get_typedtree typing in
Expand All @@ -183,6 +184,11 @@ let main () =
!output_file_name
!json_mode in
Output.write !json_mode output;
exit context output)
let exit_code = get_exit_code context output in
exit exit_code
with Failure message ->
prerr_endline message;
exit 1
)

;;main ()
3 changes: 2 additions & 1 deletion src/error.ml
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
(** Error messages. *)
(** Error messages. We handle the errors with a monad, and allopw multiple
errors per file. *)
open SmartPrint

module Category = struct
Expand Down
13 changes: 13 additions & 0 deletions tests/constants.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
let c_int : int = 0

let c_char : char = 'c'

let c_string : string = "c"

let c_float : float = 1.0

let c_int32 : int32 = 0l

let c_int64 : int64 = 0L

let c_nativeint : nativeint = 0n
24 changes: 24 additions & 0 deletions tests/constants.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Definition c_int : int := 0.

Definition c_char : ascii := "c" % char.

Definition c_string : string := "c".

Definition c_float : float :=
(* ❌ Float constant 1.0 is approximated by the integer 1 *)
1.

Definition c_int32 : int32 :=
(* ❌ Constant of type int32 is converted to int *)
0.

Definition c_int64 : int64 :=
(* ❌ Constant of type int64 is converted to int *)
0.

Definition c_nativeint : nativeint :=
(* ❌ Constant of type nativeint is converted to int *)
0.