Summary: Make it possible to run infer code from within `ocaml`/`utop`. Integration is really basic, but we can extend it if we find it useful. Reviewed By: jberdine Differential Revision: D3736029 fbshipit-source-id: 4cebb7cmaster
parent
c2ca6a23d5
commit
a31c5416b1
@ -0,0 +1,22 @@
|
|||||||
|
(*
|
||||||
|
* Copyright (c) 2016 - present Facebook, Inc.
|
||||||
|
* All rights reserved.
|
||||||
|
*
|
||||||
|
* This source code is licensed under the BSD style license found in the
|
||||||
|
* LICENSE file in the root directory of this source tree. An additional grant
|
||||||
|
* of patent rights can be found in the PATENTS file in the same directory.
|
||||||
|
*)
|
||||||
|
|
||||||
|
(* Example of ocaml script starting with infer code. To execute a scipt run:
|
||||||
|
./scripts/infer_repl <path/to/this/script.ml>
|
||||||
|
It's used as a basic integration test *)
|
||||||
|
|
||||||
|
(* "import" infer code *)
|
||||||
|
#use "toplevel_init";;
|
||||||
|
|
||||||
|
let _ = Ident.create_fresh Ident.knormal in
|
||||||
|
let ident = Ident.create_fresh Ident.knormal in
|
||||||
|
let e = Exp.Var ident in
|
||||||
|
print_endline (Sil.exp_to_string e);
|
||||||
|
(* pass --flavors flag to change the value *)
|
||||||
|
print_endline (string_of_bool Config.flavors)
|
@ -0,0 +1,20 @@
|
|||||||
|
#!/bin/bash
|
||||||
|
|
||||||
|
SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
|
||||||
|
|
||||||
|
BUILD_DIR=$SCRIPT_DIR/../infer/_build/infer
|
||||||
|
# to build new toplevel, run `make toplevel`
|
||||||
|
# -init option is used only in interactive mode
|
||||||
|
# in batch mode, scripts need to import toplevel_init themselves
|
||||||
|
# It can be done by adding #use "toplevel_init";; to the beginning
|
||||||
|
# of a script.
|
||||||
|
# NOTE: $SCRIPT_DIR is added search path for batch scripts
|
||||||
|
# so they can be located anywhere and still find toplevel_init
|
||||||
|
# file. In interactive mode $SCRIPT_DIR isn't needed
|
||||||
|
|
||||||
|
# by default utop is used, pass `INFER_UTOP_BINARY` to change the toplevel
|
||||||
|
# binary (to `ocaml` for example)
|
||||||
|
if [ -z "$INFER_UTOP_BINARY" ]; then
|
||||||
|
INFER_REPL_BINARY="utop"
|
||||||
|
fi
|
||||||
|
$INFER_REPL_BINARY -init $SCRIPT_DIR/toplevel_init -I $BUILD_DIR -I $SCRIPT_DIR $@
|
@ -0,0 +1,9 @@
|
|||||||
|
(* load dependencies *)
|
||||||
|
#use "topfind";;
|
||||||
|
#require "sawja";;
|
||||||
|
#require "atdgen";;
|
||||||
|
#require "extlib";;
|
||||||
|
|
||||||
|
(* load infer code *)
|
||||||
|
#load_rec "toplevel.cmo";;
|
||||||
|
open Toplevel;;
|
Loading…
Reference in new issue