You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

Josh Berdine 12bab4b16b [sledge] Add formal parameters to functions for return values ... Summary: This diff adds a formal parameter to each non-void-returning function to name the return value, and similarly a formal parameter for the thrown exception value. These are interpreted as call-by-reference parameters, so that they can be constrained in formulas to e.g. be equal to the return value, and are still in scope when the function returns, and so can be passed to the return block. Prior to summarizing functions, this means that these formals need to be tracked on the analyzer's control stack. This will be needed to express function specs/summaries in terms of formals, and fixes a bug where in some cases return values were not tracked correctly. Reviewed By: kren1 Differential Revision: D15738026 fbshipit-source-id: fff2d107c		6 years ago
..
config	[sledge] Put all the entry points in the config	6 years ago
import	[sledge] Add formal parameters to functions for return values	6 years ago
llair	[sledge] Add formal parameters to functions for return values	6 years ago
ppx_trace	[sledge] Add Trace.{printf,fprintf,kprintf}	6 years ago
symbheap	[sledge] Add formal parameters to functions for return values	6 years ago
trace	[sledge] Use more standard interface for Trace.parse	6 years ago
control.ml	[sledge] Add formal parameters to functions for return values	6 years ago
control.mli	[sledge] Add CL option to disable exceptions	6 years ago
dune.in	[sledge] Put all the entry points in the config	6 years ago
report.ml	[sledge] Skeleton for symbolic execution of unsafe intrinsics	6 years ago
report.mli	[sledge] Skeleton for symbolic execution of unsafe intrinsics	6 years ago
sledge.ml	[sledge] Add CL option to disable exceptions	6 years ago
sledge.mli	[ocamlformat] upgrade to ocamlformat 0.7	6 years ago
sledge_buck.ml	[sledge] Put all the entry points in the config	6 years ago
sledge_buck.mli	[sledge] Rework command line interface	6 years ago
version.ml.in	[sledge] Rework command line interface	6 years ago
version.mli	[sledge] Update entry point and command line interface	6 years ago